[GOAL]
C : Type v₁
inst✝⁹ : SmallCategory C
D : Type v₁
inst✝⁸ : SmallCategory D
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesFilteredColimits (forget A)
inst✝¹ : ReflectsIsomorphisms (forget A)
G : C ⥤ D
inst✝ : RepresentablyFlat G
⊢ PreservesFiniteLimits (Sites.pushforward A J K G)
[PROOFSTEP]
have : PreservesFiniteLimits (lan (Functor.op G) ⋙ presheafToSheaf K A) := compPreservesFiniteLimits _ _
[GOAL]
C : Type v₁
inst✝⁹ : SmallCategory C
D : Type v₁
inst✝⁸ : SmallCategory D
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesFilteredColimits (forget A)
inst✝¹ : ReflectsIsomorphisms (forget A)
G : C ⥤ D
inst✝ : RepresentablyFlat G
this : PreservesFiniteLimits (lan G.op ⋙ presheafToSheaf K A)
⊢ PreservesFiniteLimits (Sites.pushforward A J K G)
[PROOFSTEP]
apply compPreservesFiniteLimits


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
⊢ CompleteLattice (Presieve X)
[PROOFSTEP]
dsimp [Presieve]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
⊢ CompleteLattice (⦃Y : C⦄ → Set (Y ⟶ X))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ singleton f g ↔ f = g
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ singleton f g → f = g
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case mp.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ f : Y✝ ⟶ X
Y : C
⊢ f = f
[PROOFSTEP]
rfl
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ f = g → singleton f g
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ f : Y ⟶ X
⊢ singleton f f
[PROOFSTEP]
apply singleton.mk
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
⊢ pullbackArrows f (singleton g) = singleton pullback.snd
[PROOFSTEP]
funext W
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
⊢ pullbackArrows f (singleton g) = singleton pullback.snd
[PROOFSTEP]
ext h
[GOAL]
case h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) ↔ h ∈ singleton pullback.snd
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) → h ∈ singleton pullback.snd
[PROOFSTEP]
rintro ⟨W, _, _, _⟩
[GOAL]
case h.h.mp.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y✝ Y : C
⊢ pullback.snd ∈ singleton pullback.snd
[PROOFSTEP]
exact singleton.mk
[GOAL]
case h.h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ singleton pullback.snd → h ∈ pullbackArrows f (singleton g)
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case h.h.mpr.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y : C
⊢ pullback.snd ∈ pullbackArrows f (singleton g)
[PROOFSTEP]
exact pullbackArrows.mk Z g singleton.mk
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
⊢ (ofArrows (fun x => Y) fun x => f) = singleton f
[PROOFSTEP]
funext Y
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
Y : C
⊢ (ofArrows (fun x => Y✝) fun x => f) = singleton f
[PROOFSTEP]
ext g
[GOAL]
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ (g ∈ ofArrows (fun x => Y✝) fun x => f) ↔ g ∈ singleton f
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ (g ∈ ofArrows (fun x => Y✝) fun x => f) → g ∈ singleton f
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case h.h.mp.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
Y : C
i✝ : PUnit
⊢ f ∈ singleton f
[PROOFSTEP]
apply singleton.mk
[GOAL]
case h.h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ g ∈ singleton f → g ∈ ofArrows (fun x => Y✝) fun x => f
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case h.h.mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
Y : C
⊢ f ∈ ofArrows (fun x => Y✝) fun x => f
[PROOFSTEP]
exact ofArrows.mk PUnit.unit
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
⊢ (ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) = pullbackArrows f (ofArrows Z g)
[PROOFSTEP]
funext T
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
⊢ (ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) = pullbackArrows f (ofArrows Z g)
[PROOFSTEP]
ext h
[GOAL]
case h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) ↔ h ∈ pullbackArrows f (ofArrows Z g)
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) → h ∈ pullbackArrows f (ofArrows Z g)
[PROOFSTEP]
rintro ⟨hk⟩
[GOAL]
case h.h.mp.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
hk : ι
⊢ pullback.snd ∈ pullbackArrows f (ofArrows Z g)
[PROOFSTEP]
exact pullbackArrows.mk _ _ (ofArrows.mk hk)
[GOAL]
case h.h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ h ∈ pullbackArrows f (ofArrows Z g) → h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
[PROOFSTEP]
rintro ⟨W, k, hk₁⟩
[GOAL]
case h.h.mpr.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y W : C
k : W ⟶ X
hk₁ : ofArrows Z g k
⊢ pullback.snd ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
[PROOFSTEP]
cases' hk₁ with i hi
[GOAL]
case h.h.mpr.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
i : ι
⊢ pullback.snd ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
[PROOFSTEP]
apply ofArrows.mk
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
⊢ (bind (ofArrows Z g) fun Y f H => ofArrows (W f H) (k f H)) =
    ofArrows (fun i => W (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd) fun ij =>
      k (g ij.fst) (_ : ofArrows Z g (g ij.fst)) ij.snd ≫ g ij.fst
[PROOFSTEP]
funext Y
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f : Y✝ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
⊢ (bind (ofArrows Z g) fun Y f H => ofArrows (W f H) (k f H)) =
    ofArrows (fun i => W (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd) fun ij =>
      k (g ij.fst) (_ : ofArrows Z g (g ij.fst)) ij.snd ≫ g ij.fst
[PROOFSTEP]
ext f
[GOAL]
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ bind (ofArrows Z g) fun Y f H => ofArrows (W f H) (k f H)) ↔
    f ∈
      ofArrows (fun i => W (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd) fun ij =>
        k (g ij.fst) (_ : ofArrows Z g (g ij.fst)) ij.snd ≫ g ij.fst
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ bind (ofArrows Z g) fun Y f H => ofArrows (W f H) (k f H)) →
    f ∈
      ofArrows (fun i => W (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd) fun ij =>
        k (g ij.fst) (_ : ofArrows Z g (g ij.fst)) ij.snd ≫ g ij.fst
[PROOFSTEP]
rintro ⟨_, _, _, ⟨i⟩, ⟨i'⟩, rfl⟩
[GOAL]
case h.h.mp.intro.intro.intro.intro.mk.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝¹ Z✝ : C
f : Y✝¹ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y✝ : C
i : ι
Y : C
i' : j (g i) (_ : ofArrows Z g (g i))
⊢ k (g i) (_ : ofArrows Z g (g i)) i' ≫ g i ∈
    ofArrows (fun i => W (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd) fun ij =>
      k (g ij.fst) (_ : ofArrows Z g (g ij.fst)) ij.snd ≫ g ij.fst
[PROOFSTEP]
exact ofArrows.mk (Sigma.mk _ _)
[GOAL]
case h.h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈
      ofArrows (fun i => W (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd) fun ij =>
        k (g ij.fst) (_ : ofArrows Z g (g ij.fst)) ij.snd ≫ g ij.fst) →
    f ∈ bind (ofArrows Z g) fun Y f H => ofArrows (W f H) (k f H)
[PROOFSTEP]
rintro ⟨i⟩
[GOAL]
case h.h.mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f : Y✝ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
i : (i : ι) × j (g i) (_ : ofArrows Z g (g i))
⊢ k (g i.fst) (_ : ofArrows Z g (g i.fst)) i.snd ≫ g i.fst ∈ bind (ofArrows Z g) fun Y f H => ofArrows (W f H) (k f H)
[PROOFSTEP]
exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
S : Presieve X
Y : D
f : Y ⟶ F.obj X
h : functorPushforward F S f
⊢ FunctorPushforwardStructure F S f
[PROOFSTEP]
choose Z f' g h₁ h using h
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
S : Presieve X
Y : D
f : Y ⟶ F.obj X
Z : C
f' : Z ⟶ X
g : Y ⟶ F.obj Z
h₁ : S f'
h : f = g ≫ F.map f'
⊢ FunctorPushforwardStructure F S f
[PROOFSTEP]
exact ⟨Z, f', g, h₁, h⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
[PROOFSTEP]
funext x
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
[PROOFSTEP]
ext f
[GOAL]
case h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward (F ⋙ G) R ↔ f ∈ functorPushforward G (functorPushforward F R)
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward (F ⋙ G) R → f ∈ functorPushforward G (functorPushforward F R)
[PROOFSTEP]
rintro ⟨X, f₁, g₁, h₁, rfl⟩
[GOAL]
case h.h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ g₁ ≫ (F ⋙ G).map f₁ ∈ functorPushforward G (functorPushforward F R)
[PROOFSTEP]
exact ⟨F.obj X, F.map f₁, g₁, ⟨X, f₁, 𝟙 _, h₁, by simp⟩, rfl⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ F.map f₁ = 𝟙 (F.obj X) ≫ F.map f₁
[PROOFSTEP]
simp
[GOAL]
case h.h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ f ∈ functorPushforward G (functorPushforward F R) → f ∈ functorPushforward (F ⋙ G) R
[PROOFSTEP]
rintro ⟨X, f₁, g₁, ⟨X', f₂, g₂, h₁, rfl⟩, rfl⟩
[GOAL]
case h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) ∈ functorPushforward (F ⋙ G) R
[PROOFSTEP]
exact ⟨X', f₂, g₁ ≫ G.map g₂, h₁, by simp⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) = (g₁ ≫ G.map g₂) ≫ (F ⋙ G).map f₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
f : Y ⟶ X
h : R f
⊢ F.map f = 𝟙 (F.obj Y) ≫ F.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
⊢ ∀ {R S : Sieve X}, R.arrows = S.arrows → R = S
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨_, _⟩ rfl
[GOAL]
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
𝒮 : Set (Sieve X)
x✝² x✝¹ : C
f : x✝² ⟶ X
hf : (fun Y => {f | ∃ S, S ∈ 𝒮 ∧ S.arrows f}) x✝² f
x✝ : x✝¹ ⟶ x✝²
⊢ (fun Y => {f | ∃ S, S ∈ 𝒮 ∧ S.arrows f}) x✝¹ (x✝ ≫ f)
[PROOFSTEP]
obtain ⟨S, hS, hf⟩ := hf
[GOAL]
case intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R : Sieve X
𝒮 : Set (Sieve X)
x✝² x✝¹ : C
f : x✝² ⟶ X
x✝ : x✝¹ ⟶ x✝²
S : Sieve X
hS : S ∈ 𝒮
hf : S.arrows f
⊢ setOf (fun f => ∃ S, S ∈ 𝒮 ∧ S.arrows f) (x✝ ≫ f)
[PROOFSTEP]
exact ⟨S, hS, S.downward_closed hf _⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X},
    (fun Y f => S.arrows f ∨ R.arrows f) Y f → ∀ (g : Z ⟶ Y), (fun Y f => S.arrows f ∨ R.arrows f) Z (g ≫ f)
[PROOFSTEP]
rintro _ _ _ (h | h) g
[GOAL]
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : S.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)
[PROOFSTEP]
simp [h]
[GOAL]
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : R.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X},
    (fun Y f => S.arrows f ∧ R.arrows f) Y f → ∀ (g : Z ⟶ Y), (fun Y f => S.arrows f ∧ R.arrows f) Z (g ≫ f)
[PROOFSTEP]
rintro _ _ _ ⟨h₁, h₂⟩ g
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h₁ : S.arrows f✝
h₂ : R.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∧ R.arrows (g ≫ f✝)
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : x✝³ ≤ x✝¹
h₂ : x✝² ≤ x✝¹
x✝ : C
f : x✝ ⟶ X
⊢ (x✝³ ⊔ x✝²).arrows f → x✝¹.arrows f
[PROOFSTEP]
rintro (hf | hf)
[GOAL]
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : x✝³ ≤ x✝¹
h₂ : x✝² ≤ x✝¹
x✝ : C
f : x✝ ⟶ X
hf : x✝³.arrows f
⊢ x✝¹.arrows f
[PROOFSTEP]
exact h₁ _ hf
[GOAL]
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : x✝³ ≤ x✝¹
h₂ : x✝² ≤ x✝¹
x✝ : C
f : x✝ ⟶ X
hf : x✝².arrows f
⊢ x✝¹.arrows f
[PROOFSTEP]
exact h₂ _ hf
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R : Sieve X
Ss : Set (Sieve X)
Y : C
f : Y ⟶ X
⊢ (sSup Ss).arrows f ↔ ∃ S x, S.arrows f
[PROOFSTEP]
simp [sSup, Sieve.sup, setOf]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
R : Presieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X},
    (fun Z f => ∃ Y h g, R g ∧ h ≫ g = f) Y f → ∀ (g : Z ⟶ Y), (fun Z f => ∃ Y h g, R g ∧ h ≫ g = f) Z (g ≫ f)
[PROOFSTEP]
rintro Y Z _ ⟨W, g, f, hf, rfl⟩ h
[GOAL]
case intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Presieve X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ ∃ Y_1 h_1 g_1, R g_1 ∧ h_1 ≫ g_1 = h ≫ g ≫ f
[PROOFSTEP]
exact ⟨_, h ≫ g, _, hf, by simp⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Presieve X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ (h ≫ g) ≫ f = h ≫ g ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
⊢ ∀ {Y Z : C} {f : Y ⟶ X},
    Presieve.bind S (fun Y f h => (R h).arrows) f → ∀ (g : Z ⟶ Y), Presieve.bind S (fun Y f h => (R h).arrows) (g ≫ f)
[PROOFSTEP]
rintro Y Z f ⟨W, f, h, hh, hf, rfl⟩ g
[GOAL]
case intro.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
Y Z W : C
f : Y ⟶ W
h : W ⟶ X
hh : S h
hf : (R hh).arrows f
g : Z ⟶ Y
⊢ Presieve.bind S (fun Y f h => (R h).arrows) (g ≫ f ≫ h)
[PROOFSTEP]
exact ⟨_, g ≫ f, _, hh, by simp [hf]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
Y Z W : C
f : Y ⟶ W
h : W ⟶ X
hh : S h
hf : (R hh).arrows f
g : Z ⟶ Y
⊢ (fun Y f h => (R h).arrows) W h hh (g ≫ f) ∧ (g ≫ f) ≫ h = g ≫ f ≫ h
[PROOFSTEP]
simp [hf]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S✝ R✝ : Sieve X
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ (generate R).arrows f → S.arrows f
[PROOFSTEP]
rintro ⟨Z, f, g, hg, rfl⟩
[GOAL]
case intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S✝ R✝ : Sieve X
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)
[PROOFSTEP]
exact S.downward_closed (ss Z hg) f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R : Sieve X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
x✝ : ⊤.arrows f
⊢ S.arrows f
[PROOFSTEP]
simpa using downward_closed _ h f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ generate R = ⊤
[PROOFSTEP]
rw [← id_mem_iff_eq_top]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)
[PROOFSTEP]
exact ⟨_, section_ f, f, hf, by simp⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ section_ f ≫ f = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R : Sieve X
h : Y ⟶ X
S : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ Y
g : (fun Y_1 sl => S.arrows (sl ≫ h)) Y✝ f✝
⊢ ∀ (g : Z✝ ⟶ Y✝), (fun Y_1 sl => S.arrows (sl ≫ h)) Z✝ (g ≫ f✝)
[PROOFSTEP]
simp [g]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
⊢ pullback (𝟙 X) S = S
[PROOFSTEP]
simp [Sieve.ext_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
g : Z ⟶ Y
S : Sieve X
⊢ pullback (g ≫ f) S = pullback g (pullback f S)
[PROOFSTEP]
simp [Sieve.ext_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R✝ : Sieve X
f : Y ⟶ X
S R : Sieve X
⊢ pullback f (S ⊓ R) = pullback f S ⊓ pullback f R
[PROOFSTEP]
simp [Sieve.ext_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
⊢ S.arrows f ↔ pullback f S = ⊤
[PROOFSTEP]
rw [← id_mem_iff_eq_top, pullback_apply, id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝¹ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
R : Sieve Y
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : (fun Z gf => ∃ g, g ≫ f = gf ∧ R.arrows g) Y✝ f✝
h : Z✝ ⟶ Y✝
j : Y✝ ⟶ Y
k : j ≫ f = f✝
z : R.arrows j
⊢ (h ≫ j) ≫ f = h ≫ f✝
[PROOFSTEP]
simp [k]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝¹ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
R : Sieve Y
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : (fun Z gf => ∃ g, g ≫ f = gf ∧ R.arrows g) Y✝ f✝
h : Z✝ ⟶ Y✝
j : Y✝ ⟶ Y
k : j ≫ f = f✝
z : R.arrows j
⊢ R.arrows (h ≫ j)
[PROOFSTEP]
simp [z]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward (g ≫ f) R).arrows h
f₁ : W ⟶ Z
hq : f₁ ≫ g ≫ f = h
hf₁ : R.arrows f₁
⊢ (f₁ ≫ g) ≫ f = h
[PROOFSTEP]
simpa
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ z ≫ g ≫ f = h ∧ R.arrows z
[PROOFSTEP]
rw [← Category.assoc, hR]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z
[PROOFSTEP]
tauto
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R
[PROOFSTEP]
rintro Z _ ⟨g, rfl, hg⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
Z : C
g : Z ⟶ Y
hg : (R h).arrows g
⊢ (bind S R).arrows (g ≫ f)
[PROOFSTEP]
exact ⟨_, g, f, h, hg, rfl⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ R h ≤ pullback f (bind S R)
[PROOFSTEP]
rw [← galoisConnection f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R
[PROOFSTEP]
apply pushforward_le_bind_of_mem
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
⊢ GaloisCoinsertion (pushforward f) (pullback f)
[PROOFSTEP]
apply (galoisConnection f).toGaloisCoinsertion
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
⊢ ∀ (a : Sieve Y), pullback f (pushforward f a) ≤ a
[PROOFSTEP]
rintro S Z g ⟨g₁, hf, hg₁⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ ≫ f = g ≫ f
hg₁ : S.arrows g₁
⊢ S.arrows g
[PROOFSTEP]
rw [cancel_mono f] at hf
[GOAL]
case intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g
[PROOFSTEP]
rwa [← hf]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
⊢ GaloisInsertion (pushforward f) (pullback f)
[PROOFSTEP]
apply (galoisConnection f).toGaloisInsertion
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
⊢ ∀ (b : Sieve X), b ≤ pushforward f (pullback f b)
[PROOFSTEP]
intro S Z g hg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
S : Sieve X
Z : C
g : Z ⟶ X
hg : S.arrows g
⊢ (pushforward f (pullback f S)).arrows g
[PROOFSTEP]
refine' ⟨g ≫ section_ f, by simpa⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
S : Sieve X
Z : C
g : Z ⟶ X
hg : S.arrows g
⊢ (g ≫ section_ f) ≫ f = g ∧ (pullback f S).arrows (g ≫ section_ f)
[PROOFSTEP]
simpa
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
⊢ generate (Presieve.pullbackArrows f R) = pullback f (generate R)
[PROOFSTEP]
ext W g
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
[PROOFSTEP]
constructor
[GOAL]
case h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g
[PROOFSTEP]
rintro ⟨_, h, k, hk, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W w✝ : C
h : W ⟶ w✝
k : w✝ ⟶ Y
hk : Presieve.pullbackArrows f R k
⊢ (pullback f (generate R)).arrows (h ≫ k)
[PROOFSTEP]
cases' hk with W g hg
[GOAL]
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd)
[PROOFSTEP]
change (Sieve.generate R).pullback f (h ≫ pullback.snd)
[GOAL]
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd)
[PROOFSTEP]
rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]
[GOAL]
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst) ≫ g)
[PROOFSTEP]
exact Sieve.downward_closed _ (by exact Sieve.le_generate R W hg) (h ≫ pullback.fst)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows g
[PROOFSTEP]
exact Sieve.le_generate R W hg
[GOAL]
case h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g
[PROOFSTEP]
rintro ⟨W, h, k, hk, comm⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g
[PROOFSTEP]
exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
⊢ ∀ {Y Z : C} {f : Y ⟶ X},
    Presieve.functorPullback F R.arrows f → ∀ (g : Z ⟶ Y), Presieve.functorPullback F R.arrows (g ≫ f)
[PROOFSTEP]
intro _ _ f hf g
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ Presieve.functorPullback F R.arrows (g ≫ f)
[PROOFSTEP]
unfold Presieve.functorPullback
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ R.arrows (F.map (g ≫ f))
[PROOFSTEP]
rw [F.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ R.arrows (F.map g ≫ F.map f)
[PROOFSTEP]
exact R.downward_closed hf (F.map g)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPullback (𝟭 C) R = R
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (𝟭 C) R).arrows f✝ ↔ R.arrows f✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
⊢ functorPullback (F ⋙ G) R = functorPullback F (functorPullback G R)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (F ⋙ G) R).arrows f✝ ↔ (functorPullback F (functorPullback G R)).arrows f✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
[PROOFSTEP]
funext Y
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
[PROOFSTEP]
ext f
[GOAL]
case h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows ↔ f ∈ Presieve.functorPushforward F R
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows → f ∈ Presieve.functorPushforward F R
[PROOFSTEP]
rintro ⟨X', g, f', ⟨X'', g', f'', h₁, rfl⟩, rfl⟩
[GOAL]
case h.h.mp.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') ∈ Presieve.functorPushforward F R
[PROOFSTEP]
exact ⟨X'', f'', f' ≫ F.map g', h₁, by simp⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') = (f' ≫ F.map g') ≫ F.map f''
[PROOFSTEP]
simp
[GOAL]
case h.h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ f ∈ Presieve.functorPushforward F R → f ∈ Presieve.functorPushforward F (generate R).arrows
[PROOFSTEP]
rintro ⟨X', g, f', h₁, h₂⟩
[GOAL]
case h.h.mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
Y : D
f : Y ⟶ F.obj X
X' : C
g : X' ⟶ X
f' : Y ⟶ F.obj X'
h₁ : R g
h₂ : f = f' ≫ F.map g
⊢ f ∈ Presieve.functorPushforward F (generate R).arrows
[PROOFSTEP]
exact ⟨X', g, f', le_generate R _ h₁, h₂⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ ∀ {Y Z : D} {f : Y ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z ⟶ Y), Presieve.functorPushforward F R.arrows (g ≫ f)
[PROOFSTEP]
intro _ _ f h g
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ Z✝ : D
f : Y✝ ⟶ F.obj X
h : Presieve.functorPushforward F R.arrows f
g : Z✝ ⟶ Y✝
⊢ Presieve.functorPushforward F R.arrows (g ≫ f)
[PROOFSTEP]
obtain ⟨X, α, β, hα, rfl⟩ := h
[GOAL]
case intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
Y✝ Z✝ : D
g : Z✝ ⟶ Y✝
X : C
α : X ⟶ X✝
β : Y✝ ⟶ F.obj X
hα : R.arrows α
⊢ Presieve.functorPushforward F R.arrows (g ≫ β ≫ F.map α)
[PROOFSTEP]
exact ⟨X, α, g ≫ β, hα, by simp⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
Y✝ Z✝ : D
g : Z✝ ⟶ Y✝
X : C
α : X ⟶ X✝
β : Y✝ ⟶ F.obj X
hα : R.arrows α
⊢ g ≫ β ≫ F.map α = (g ≫ β) ≫ F.map α
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPushforward (𝟭 C) R = R
[PROOFSTEP]
ext X f
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f✝ : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f ↔ R.arrows f
[PROOFSTEP]
constructor
[GOAL]
case h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f✝ : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f → R.arrows f
[PROOFSTEP]
intro hf
[GOAL]
case h.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f✝ : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : (functorPushforward (𝟭 C) R).arrows f
⊢ R.arrows f
[PROOFSTEP]
obtain ⟨X, g, h, hg, rfl⟩ := hf
[GOAL]
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝¹ Y Z : C
f : Y ⟶ X✝¹
S R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝¹
X✝ X : C
g : X ⟶ X✝¹
h : X✝ ⟶ (𝟭 C).obj X
hg : R.arrows g
⊢ R.arrows (h ≫ (𝟭 C).map g)
[PROOFSTEP]
exact R.downward_closed hg h
[GOAL]
case h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f✝ : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ R.arrows f → (functorPushforward (𝟭 C) R).arrows f
[PROOFSTEP]
intro hf
[GOAL]
case h.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f✝ : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ (functorPushforward (𝟭 C) R).arrows f
[PROOFSTEP]
exact ⟨X, f, 𝟙 _, hf, by simp⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f✝ : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ f = 𝟙 X ≫ (𝟭 C).map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ : E
f✝ : Y✝ ⟶ (F ⋙ G).obj X
⊢ (functorPushforward (F ⋙ G) R).arrows f✝ ↔ (functorPushforward G (functorPushforward F R)).arrows f✝
[PROOFSTEP]
simp [R.arrows.functorPushforward_comp F G]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
X : C
⊢ GaloisConnection (functorPushforward F) (functorPullback F)
[PROOFSTEP]
intro R S
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S → R ≤ functorPullback F S
[PROOFSTEP]
intro hle X f hf
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category.{v₃, u₃} 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
[PROOFSTEP]
apply hle
[GOAL]
case mp.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category.{v₃, u₃} 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)
[PROOFSTEP]
refine' ⟨X, f, 𝟙 _, hf, _⟩
[GOAL]
case mp.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝¹ Y Z : C
f✝ : Y ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category.{v₃, u₃} 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
[PROOFSTEP]
rw [id_comp]
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S✝ R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ R ≤ functorPullback F S → functorPushforward F R ≤ S
[PROOFSTEP]
rintro hle Y f ⟨X, g, h, hg, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝¹ Y✝ Z : C
f : Y✝ ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category.{v₃, u₃} 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)
[PROOFSTEP]
apply Sieve.downward_closed S
[GOAL]
case mpr.intro.intro.intro.intro.x
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝¹ Y✝ Z : C
f : Y✝ ⟶ X✝¹
S✝ R✝ : Sieve X✝¹
E : Type u₃
inst✝ : Category.{v₃, u₃} 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)
[PROOFSTEP]
exact hle g hg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ functorPushforward F ⊤ = ⊤
[PROOFSTEP]
refine' (generate_sieve _).symm.trans _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ generate (functorPushforward F ⊤).arrows = ⊤
[PROOFSTEP]
apply generate_of_contains_isSplitEpi (𝟙 (F.obj X))
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ (functorPushforward F ⊤).arrows (𝟙 (F.obj X))
[PROOFSTEP]
refine' ⟨X, 𝟙 _, 𝟙 _, trivial, by simp⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
V : C
f : V ⟶ X
h : R.arrows f
⊢ F.map f = 𝟙 (F.obj V) ≫ F.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : EssSurj F
inst✝ : Full F
X : C
⊢ GaloisInsertion (functorPushforward F) (functorPullback F)
[PROOFSTEP]
apply (functor_galoisConnection F X).toGaloisInsertion
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : EssSurj F
inst✝ : Full F
X : C
⊢ ∀ (b : Sieve (F.obj X)), b ≤ functorPushforward F (functorPullback F b)
[PROOFSTEP]
intro S Y f hf
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : EssSurj F
inst✝ : Full F
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPushforward F (functorPullback F S)).arrows f
[PROOFSTEP]
refine' ⟨_, F.preimage ((F.objObjPreimageIso Y).hom ≫ f), (F.objObjPreimageIso Y).inv, _⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : EssSurj F
inst✝ : Full F
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPullback F S).arrows (F.preimage ((Functor.objObjPreimageIso F Y).hom ≫ f)) ∧
    f = (Functor.objObjPreimageIso F Y).inv ≫ F.map (F.preimage ((Functor.objObjPreimageIso F Y).hom ≫ f))
[PROOFSTEP]
simpa using S.downward_closed hf _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : Full F
inst✝ : Faithful F
X : C
⊢ GaloisCoinsertion (functorPushforward F) (functorPullback F)
[PROOFSTEP]
apply (functor_galoisConnection F X).toGaloisCoinsertion
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : Full F
inst✝ : Faithful F
X : C
⊢ ∀ (a : Sieve X), functorPullback F (functorPushforward F a) ≤ a
[PROOFSTEP]
rintro S Y f ⟨Z, g, h, h₁, h₂⟩
[GOAL]
case intro.intro.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : Full F
inst✝ : Faithful F
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = h ≫ F.map g
⊢ S.arrows f
[PROOFSTEP]
rw [← F.image_preimage h, ← F.map_comp] at h₂
[GOAL]
case intro.intro.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : Full F
inst✝ : Faithful F
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows f
[PROOFSTEP]
rw [F.map_injective h₂]
[GOAL]
case intro.intro.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : Full F
inst✝ : Faithful F
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows (F.preimage h ≫ g)
[PROOFSTEP]
exact S.downward_closed h₁ _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ functor S
h : f ≫ functorInclusion S = g ≫ functorInclusion S
⊢ f = g
[PROOFSTEP]
ext Y y
[GOAL]
case w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R : Sieve X
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ functor S
h : f ≫ functorInclusion S = g ≫ functorInclusion S
Y : Cᵒᵖ
y : Z✝.obj Y
⊢ NatTrans.app f Y y = NatTrans.app g Y y
[PROOFSTEP]
simpa [Subtype.ext_iff_val] using congr_fun (NatTrans.congr_app h Y) y
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ X},
    (fun Y g => ∃ t, NatTrans.app f (Opposite.op Y) t = g) Y f_1 →
      ∀ (g : Z ⟶ Y), (fun Y g => ∃ t, NatTrans.app f (Opposite.op Y) t = g) Z (g ≫ f_1)
[PROOFSTEP]
rintro Y Z _ ⟨t, rfl⟩ g
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ ∃ t_1, NatTrans.app f (Opposite.op Z) t_1 = g ≫ NatTrans.app f (Opposite.op Y) t
[PROOFSTEP]
refine' ⟨R.map g.op t, _⟩
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ NatTrans.app f (Opposite.op Z) (R.map g.op t) = g ≫ NatTrans.app f (Opposite.op Y) t
[PROOFSTEP]
rw [FunctorToTypes.naturality _ _ f]
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ (yoneda.obj X).map g.op (NatTrans.app f (Opposite.op Y) t) = g ≫ NatTrans.app f (Opposite.op Y) t
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
⊢ sieveOfSubfunctor (functorInclusion S) = S
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (sieveOfSubfunctor (functorInclusion S)).arrows f✝ ↔ S.arrows f✝
[PROOFSTEP]
simp only [functorInclusion_app, sieveOfSubfunctor_apply]
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) ↔ S.arrows f✝
[PROOFSTEP]
constructor
[GOAL]
case h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) → S.arrows f✝
[PROOFSTEP]
rintro ⟨⟨f, hf⟩, rfl⟩
[GOAL]
case h.mp.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
Y✝ : C
f : (Opposite.op Y✝).unop ⟶ X
hf : S.arrows f
⊢ S.arrows ↑{ val := f, property := hf }
[PROOFSTEP]
exact hf
[GOAL]
case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, ↑t = f✝
[PROOFSTEP]
intro hf
[GOAL]
case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
hf : S.arrows f✝
⊢ ∃ t, ↑t = f✝
[PROOFSTEP]
exact ⟨⟨_, hf⟩, rfl⟩


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
⊢ S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X →
    Sieve.pullback g S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y
[PROOFSTEP]
rintro ⟨R, hR, RS⟩
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.pullback g S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y
[PROOFSTEP]
refine' ⟨_, K.pullbacks g _ hR, _⟩
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ pullbackArrows g R ≤ (Sieve.pullback g S).arrows
[PROOFSTEP]
rw [← Sieve.sets_iff_generate, Sieve.pullbackArrows_comm]
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.pullback g (Sieve.generate R) ≤ Sieve.pullback g S
[PROOFSTEP]
apply Sieve.pullback_monotone
[GOAL]
case intro.intro.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.generate R ≤ S
[PROOFSTEP]
rwa [Sieve.giGenerate.gc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
            S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y) →
          R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X
[PROOFSTEP]
rintro X S ⟨R', hR', RS⟩ R t
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y
⊢ R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X
[PROOFSTEP]
choose t₁ t₂ t₃ using t
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ coverings K Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
⊢ R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X
[PROOFSTEP]
refine' ⟨_, K.Transitive _ _ hR' fun _ f hf => t₂ (RS _ hf), _⟩
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ coverings K Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
⊢ (Presieve.bind R' fun x f hf => t₁ (_ : f ∈ S.arrows)) ≤ R.arrows
[PROOFSTEP]
rintro Y _ ⟨Z, g, f, hg, hf, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ coverings K Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hg : R' f
hf : t₁ (_ : f ∈ S.arrows) g
⊢ g ≫ f ∈ R.arrows
[PROOFSTEP]
apply t₃ (RS _ hg) _ hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
i : IsIso f
⊢ Sieve.generate (Presieve.singleton f) = ⊤
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
⊢ pullbackArrows f R ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
[PROOFSTEP]
simp only [Set.mem_def, Sieve.pullbackArrows_comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
⊢ GrothendieckTopology.sieves J Y (Sieve.pullback f (Sieve.generate R))
[PROOFSTEP]
apply J.pullback_stable f hR
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
⊢ Presieve.bind S Ti ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
[PROOFSTEP]
apply J.transitive hS
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    (Sieve.generate S).arrows f →
      Sieve.pullback f (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
intro Y f
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y : C
f : Y ⟶ X
⊢ (Sieve.generate S).arrows f → Sieve.pullback f (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
rintro ⟨Z, g, f, hf, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback (g ≫ f) (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
rw [Sieve.pullback_comp]
[GOAL]
case h.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback g (Sieve.pullback f (Sieve.generate (Presieve.bind S Ti))) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
apply J.pullback_stable g
[GOAL]
case h.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback f (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Z
[PROOFSTEP]
apply J.superset_covering _ (hTi _ hf)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.generate (Ti f hf) ≤ Sieve.pullback f (Sieve.generate (Presieve.bind S Ti))
[PROOFSTEP]
rintro Y g ⟨W, h, g, hg, rfl⟩
[GOAL]
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ (Sieve.pullback f (Sieve.generate (Presieve.bind S Ti))).arrows (h ≫ g)
[PROOFSTEP]
exact ⟨_, h, _, ⟨_, _, _, hf, hg, rfl⟩, by simp⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ h ≫ g ≫ f = (h ≫ g) ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ toGrothendieck C K ≤ J ↔ K ≤ ofGrothendieck C J
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ toGrothendieck C K ≤ J → K ≤ ofGrothendieck C J
[PROOFSTEP]
intro h X R hR
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : toGrothendieck C K ≤ J
X : C
R : Presieve X
hR : R ∈ coverings K X
⊢ R ∈ coverings (ofGrothendieck C J) X
[PROOFSTEP]
exact h _ ⟨_, hR, Sieve.le_generate R⟩
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K ≤ ofGrothendieck C J → toGrothendieck C K ≤ J
[PROOFSTEP]
rintro h X S ⟨R, hR, RS⟩
[GOAL]
case mpr.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K ≤ ofGrothendieck C J
X : C
S : Sieve X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
apply J.superset_covering _ (h _ hR)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K ≤ ofGrothendieck C J
X : C
S : Sieve X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.generate R ≤ S
[PROOFSTEP]
rwa [Sieve.giGenerate.gc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
S : Presieve X
⊢ S ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X →
    pullbackArrows f S ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
[PROOFSTEP]
rintro ⟨Z, g, i, rfl⟩
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
[PROOFSTEP]
refine' ⟨pullback g f, pullback.snd, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ IsIso pullback.snd
[PROOFSTEP]
refine' ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨_, by aesop_cat⟩⟩⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (f ≫ inv g) ≫ g = 𝟙 Y ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f) ≫ pullback.snd = 𝟙 Y
[PROOFSTEP]
aesop_cat
[GOAL]
case intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.snd ≫ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f) = 𝟙 (pullback g f)
[PROOFSTEP]
ext
[GOAL]
case intro.intro.intro.refine'_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd ≫ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f)) ≫ pullback.fst =
    𝟙 (pullback g f) ≫ pullback.fst
[PROOFSTEP]
rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
[GOAL]
case intro.intro.intro.refine'_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.fst ≫ g ≫ inv g = 𝟙 (pullback g f) ≫ pullback.fst
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.refine'_1.h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd ≫ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f)) ≫ pullback.snd =
    𝟙 (pullback g f) ≫ pullback.snd
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton pullback.snd
[PROOFSTEP]
apply pullback_singleton
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
⊢ ∀ ⦃X : C⦄ (S : Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y),
    S ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X →
      (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y) →
        Presieve.bind S Ti ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X
[PROOFSTEP]
rintro X S Ti ⟨Z, g, i, rfl⟩ hS
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
⊢ Presieve.bind (Presieve.singleton g) Ti ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X
[PROOFSTEP]
rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ Presieve.bind (Presieve.singleton g) Ti ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X
[PROOFSTEP]
refine' ⟨_, f ≫ g, _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ IsIso (f ≫ g)
[PROOFSTEP]
infer_instance
  -- Porting note: the next four lines were just "ext (W k)"
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ Presieve.bind (Presieve.singleton g) Ti = Presieve.singleton (f ≫ g)
[PROOFSTEP]
apply funext
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ ∀ (x : C), Presieve.bind (Presieve.singleton g) Ti = Presieve.singleton (f ≫ g)
[PROOFSTEP]
rintro W
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
⊢ Presieve.bind (Presieve.singleton g) Ti = Presieve.singleton (f ≫ g)
[PROOFSTEP]
apply Set.ext
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
⊢ ∀ (x : W ⟶ X), x ∈ Presieve.bind (Presieve.singleton g) Ti ↔ x ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
rintro k
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
k : W ⟶ X
⊢ k ∈ Presieve.bind (Presieve.singleton g) Ti ↔ k ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
k : W ⟶ X
⊢ k ∈ Presieve.bind (Presieve.singleton g) Ti → k ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
rintro ⟨V, h, k, ⟨_⟩, hh, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Ti g (_ : singleton' g g) h
⊢ h ≫ g ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
rw [hTi] at hh
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Presieve.singleton f h
⊢ h ≫ g ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
cases hh
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp.intro.intro.intro.intro.mk.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ f ≫ g ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
apply singleton.mk
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
k : W ⟶ X
⊢ k ∈ Presieve.singleton (f ≫ g) → k ∈ Presieve.bind (Presieve.singleton g) Ti
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ f ≫ g ∈ Presieve.bind (Presieve.singleton g) Ti
[PROOFSTEP]
refine' bind_comp g singleton.mk _
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ Ti g (_ : Presieve.singleton g g) f
[PROOFSTEP]
rw [hTi]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ Presieve.singleton f f
[PROOFSTEP]
apply singleton.mk
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
R : Presieve X
⊢ R ∈ coverings ⊥ X → R ∈ coverings K X
[PROOFSTEP]
rintro ⟨Y, f, hf, rfl⟩
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
f : Y ⟶ X
hf : IsIso f
⊢ Presieve.singleton f ∈ coverings K X
[PROOFSTEP]
exact K.has_isos f