[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) ↔ ∃ T, Sieve.functorPullback G ↑T = S
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) → ∃ T, Sieve.functorPullback G ↑T = S
[PROOFSTEP]
intro hS
[GOAL]
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
⊢ ∃ T, Sieve.functorPullback G ↑T = S
[PROOFSTEP]
exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
[GOAL]
case mpr
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
[PROOFSTEP]
rintro ⟨T, rfl⟩
[GOAL]
case mpr.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))
[PROOFSTEP]
exact Hld T
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
⊢ ⊤ ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
[PROOFSTEP]
change K _ _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G ⊤)
[PROOFSTEP]
rw [Sieve.functorPushforward_top]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
⊢ GrothendieckTopology.sieves K (G.obj X) ⊤
[PROOFSTEP]
exact K.top_mem _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
⊢ Sieve.pullback f S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
[PROOFSTEP]
have : S.pullback f = ((S.functorPushforward G).pullback (G.map f)).functorPullback G :=
  by
  conv_lhs => rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
  ext
  change (S.functorPushforward G) _ ↔ (S.functorPushforward G) _
  rw [G.map_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
⊢ Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
[PROOFSTEP]
conv_lhs => rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
| Sieve.pullback f S
[PROOFSTEP]
rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
| Sieve.pullback f S
[PROOFSTEP]
rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
| Sieve.pullback f S
[PROOFSTEP]
rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
⊢ Sieve.pullback f (Sieve.functorPullback G (Sieve.functorPushforward G S)) =
    Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
Y✝ : C
f✝ : Y✝ ⟶ Y
⊢ (Sieve.pullback f (Sieve.functorPullback G (Sieve.functorPushforward G S))).arrows f✝ ↔
    (Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))).arrows f✝
[PROOFSTEP]
change (S.functorPushforward G) _ ↔ (S.functorPushforward G) _
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
Y✝ : C
f✝ : Y✝ ⟶ Y
⊢ (Sieve.functorPushforward G S).arrows (G.map (f✝ ≫ f)) ↔ (Sieve.functorPushforward G S).arrows (G.map f✝ ≫ G.map f)
[PROOFSTEP]
rw [G.map_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
this : Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
⊢ Sieve.pullback f S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
this : Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
⊢ Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S)) ∈
    (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
[PROOFSTEP]
change K _ _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
this : Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
⊢ GrothendieckTopology.sieves K (G.obj Y)
    (Sieve.functorPushforward G (Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))))
[PROOFSTEP]
apply Hld ⟨_, K.pullback_stable (G.map f) hS⟩
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
⊢ S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
[PROOFSTEP]
apply K.transitive hS
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ G.obj X⦄,
    (Sieve.functorPushforward G S).arrows f →
      Sieve.pullback f (Sieve.functorPushforward G S') ∈ GrothendieckTopology.sieves K Y
[PROOFSTEP]
rintro Y _ ⟨Z, g, i, hg, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G S') ∈ GrothendieckTopology.sieves K Y
[PROOFSTEP]
rw [Sieve.pullback_comp]
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ GrothendieckTopology.sieves K Y
[PROOFSTEP]
apply K.pullback_stable i
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (G.map g) (Sieve.functorPushforward G S') ∈ GrothendieckTopology.sieves K (G.obj Z)
[PROOFSTEP]
refine' K.superset_covering _ (H' hg)
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.functorPushforward G (Sieve.pullback g S') ≤ Sieve.pullback (G.map g) (Sieve.functorPushforward G S')
[PROOFSTEP]
rintro W _ ⟨Z', g', i', hg, rfl⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg✝ : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')).arrows (i' ≫ G.map g')
[PROOFSTEP]
refine' ⟨Z', g' ≫ g, i', hg, _⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg✝ : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (i' ≫ G.map g') ≫ G.map g = i' ≫ G.map (g' ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
⊢ LocallyCoverDense K G
[PROOFSTEP]
intro X T
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ GrothendieckTopology.sieves K (G.obj X)
[PROOFSTEP]
refine' K.superset_covering _ (K.bind_covering T.property fun Y f _ => H.is_cover Y)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ (Sieve.bind (↑T).arrows fun Y f x => Sieve.coverByImage G Y) ≤ Sieve.functorPushforward G (Sieve.functorPullback G ↑T)
[PROOFSTEP]
rintro Y _ ⟨Z, _, f, hf, ⟨W, g, f', rfl : _ = _⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)).arrows ((g ≫ f') ≫ f)
[PROOFSTEP]
use W
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ ∃ g_1 h, (Sieve.functorPullback G ↑T).arrows g_1 ∧ (g ≫ f') ≫ f = h ≫ G.map g_1
[PROOFSTEP]
use G.preimage (f' ≫ f)
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ ∃ h, (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f)) ∧ (g ≫ f') ≫ f = h ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
use g
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f)) ∧ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f))
case h.right
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
simpa using T.val.downward_closed hf f'
[GOAL]
case h.right
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
⊢ LocallyCoverDense J (Over.forget X)
[PROOFSTEP]
intro Y T
[GOAL]
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) ∈
    GrothendieckTopology.sieves J ((Over.forget X).obj Y)
[PROOFSTEP]
convert T.property
[GOAL]
case h.e'_4
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) = ↑T
[PROOFSTEP]
ext Z f
[GOAL]
case h.e'_4.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f ↔ (↑T).arrows f
[PROOFSTEP]
constructor
[GOAL]
case h.e'_4.h.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f → (↑T).arrows f
[PROOFSTEP]
rintro ⟨_, _, g', hg, rfl⟩
[GOAL]
case h.e'_4.h.mp.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
w✝¹ : Over X
w✝ : w✝¹ ⟶ Y
g' : Z ⟶ (Over.forget X).obj w✝¹
hg : (Sieve.functorPullback (Over.forget X) ↑T).arrows w✝
⊢ (↑T).arrows (g' ≫ (Over.forget X).map w✝)
[PROOFSTEP]
exact T.val.downward_closed hg g'
[GOAL]
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (↑T).arrows f → (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
[PROOFSTEP]
intro hf
[GOAL]
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
hf : (↑T).arrows f
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
[PROOFSTEP]
exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩
