C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
⊢ GaloisConnection (functorPushforward F) (functorPullback F)
intro R S
case mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S → R ≤ functorPullback F S

case mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ R ≤ functorPullback F S → functorPushforward F R ≤ S
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S
constructor
case mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPullback F S).arrows f
case mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S → R ≤ functorPullback F S
intro hle X f hf
case mp.a
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPushforward F R).arrows (F.map f)
case mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPullback F S).arrows f
apply hle
case mp.a
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ F.map f = 𝟙 (F.obj X) ≫ F.map f
case mp.a
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPushforward F R).arrows (F.map f)
refine' ⟨X, f, 𝟙 _, hf, _⟩
no goals
case mp.a
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ F.map f = 𝟙 (F.obj X) ≫ F.map f
rw [id_comp]
case mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y✝ Z : C
f : Y✝ ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X✝
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (h ≫ F.map g)
case mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ R ≤ functorPullback F S → functorPushforward F R ≤ S
rintro hle Y f ⟨X, g, h, hg, rfl⟩
case mpr.intro.intro.intro.intro.x
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y✝ Z : C
f : Y✝ ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X✝
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (F.map g)
case mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y✝ Z : C
f : Y✝ ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X✝
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (h ≫ F.map g)
apply Sieve.downward_closed S
no goals
case mpr.intro.intro.intro.intro.x
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝¹ Y✝ Z : C
f : Y✝ ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category E
G : D ⥤ E
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X✝
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (F.map g)
exact hle g hg