[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (G.obj (op U))
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ U},
    (fun V i => ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s) Y f_1 →
      ∀ (g : Z ⟶ Y), (fun V i => ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s) Z (g ≫ f_1)
[PROOFSTEP]
rintro V W i ⟨t, ht⟩ j
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (G.obj (op U))
V W : C
i : V ⟶ U
t : (forget A).obj (F.obj (op V))
ht : ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s
j : W ⟶ V
⊢ ∃ t, ↑(NatTrans.app f (op W)) t = ↑(G.map (j ≫ i).op) s
[PROOFSTEP]
refine' ⟨F.map j.op t, _⟩
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (G.obj (op U))
V W : C
i : V ⟶ U
t : (forget A).obj (F.obj (op V))
ht : ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s
j : W ⟶ V
⊢ ↑(NatTrans.app f (op W)) (↑(F.map j.op) t) = ↑(G.map (j ≫ i).op) s
[PROOFSTEP]
rw [op_comp, G.map_comp, comp_apply, ← ht, elementwise_of% f.naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
⊢ imageSieve f (↑(NatTrans.app f (op U)) s) = ⊤
[PROOFSTEP]
ext V i
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
V : C
i : V ⟶ U
⊢ (imageSieve f (↑(NatTrans.app f (op U)) s)).arrows i ↔ ⊤.arrows i
[PROOFSTEP]
simp only [Sieve.top_apply, iff_true_iff, imageSieve_apply]
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
V : C
i : V ⟶ U
⊢ ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) (↑(NatTrans.app f (op U)) s)
[PROOFSTEP]
have := elementwise_of% (f.naturality i.op)
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
V : C
i : V ⟶ U
this :
  ∀ (x : (forget A).obj (F.obj (op U))),
    ↑(NatTrans.app f (op V)) (↑(F.map i.op) x) = ↑(G.map i.op) (↑(NatTrans.app f (op U)) x)
⊢ ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) (↑(NatTrans.app f (op U)) s)
[PROOFSTEP]
exact ⟨F.map i.op s, this s⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤
[PROOFSTEP]
simp only [Subpresheaf.ext_iff, Function.funext_iff, Set.ext_iff, top_subpresheaf_obj, Set.top_eq_univ, Set.mem_univ,
  iff_true_iff]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔
    ∀ (a : Cᵒᵖ) (x : (G ⋙ forget A).obj a),
      x ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A)))) a
[PROOFSTEP]
exact ⟨fun H U => H (unop U), fun H U => H (op U)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf f) = ⊤
[PROOFSTEP]
simp only [Subpresheaf.ext_iff, Function.funext_iff, Set.ext_iff, top_subpresheaf_obj, Set.top_eq_univ, Set.mem_univ,
  iff_true_iff]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ ∀ (a : Cᵒᵖ) (x : G.obj a), x ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f)) a
[PROOFSTEP]
exact ⟨fun H U => H (unop U), fun H U => H (op U)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallySurjective J f.val ↔ IsIso (imageSheafι f)
[PROOFSTEP]
rw [imageSheafι, isLocallySurjective_iff_imagePresheaf_sheafify_eq_top', Subpresheaf.eq_top_iff_isIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val))) ↔
    IsIso { val := Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val)) }
[PROOFSTEP]
exact
  ⟨fun h => @isIso_of_reflects_iso _ _ _ _ _ _ (imageSheafι f) (sheafToPresheaf J _) h _, fun h =>
    @Functor.map_isIso _ _ _ _ _ _ (sheafToPresheaf J _) _ h⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))
[PROOFSTEP]
simp only [isLocallySurjective_iff_imagePresheaf_sheafify_eq_top]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤ ↔
    Subpresheaf.sheafify J (imagePresheaf (whiskerRight (whiskerRight f (forget A)) (forget (Type w')))) = ⊤
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
⊢ IsLocallySurjective J f
[PROOFSTEP]
intro U s
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
U : C
s : (forget A).obj (G.obj (op U))
⊢ imageSieve f s ∈ sieves J U
[PROOFSTEP]
obtain ⟨t, rfl⟩ := H _ s
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
U : C
t : (forget A).obj (F.obj (op U))
⊢ imageSieve f (↑(NatTrans.app f (op U)) t) ∈ sieves J U
[PROOFSTEP]
rw [imageSieve_app]
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
U : C
t : (forget A).obj (F.obj (op U))
⊢ ⊤ ∈ sieves J U
[PROOFSTEP]
exact J.top_mem _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
⊢ IsLocallySurjective J f
[PROOFSTEP]
apply isLocallySurjective_of_surjective
[GOAL]
case H
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
⊢ ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
[PROOFSTEP]
intro U
[GOAL]
case H
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ Function.Surjective ↑(NatTrans.app f U)
[PROOFSTEP]
apply Function.Bijective.surjective
[GOAL]
case H.hf
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ Function.Bijective ↑(NatTrans.app f U)
[PROOFSTEP]
rw [← isIso_iff_bijective, ← forget_map_eq_coe]
[GOAL]
case H.hf
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ IsIso ((forget A).map (NatTrans.app f U))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J (f₁ ≫ f₂)
[PROOFSTEP]
intro U s
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
⊢ imageSieve (f₁ ≫ f₂) s ∈ sieves J U
[PROOFSTEP]
have : (Sieve.bind (imageSieve f₂ s) fun _ _ h => imageSieve f₁ h.choose) ≤ imageSieve (f₁ ≫ f₂) s :=
  by
  rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
  refine' ⟨t', _⟩
  rw [op_comp, F₃.map_comp, NatTrans.comp_app, comp_apply, comp_apply, ht', elementwise_of% f₂.naturality,
    H.choose_spec]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
⊢ (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
[PROOFSTEP]
rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve f₂ s).arrows j
t' : (forget A).obj (F₁.obj (op V))
ht' : ↑(NatTrans.app f₁ (op V)) t' = ↑(F₂.map i.op) (Exists.choose H)
⊢ (imageSieve (f₁ ≫ f₂) s).arrows (i ≫ j)
[PROOFSTEP]
refine' ⟨t', _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve f₂ s).arrows j
t' : (forget A).obj (F₁.obj (op V))
ht' : ↑(NatTrans.app f₁ (op V)) t' = ↑(F₂.map i.op) (Exists.choose H)
⊢ ↑(NatTrans.app (f₁ ≫ f₂) (op V)) t' = ↑(F₃.map (i ≫ j).op) s
[PROOFSTEP]
rw [op_comp, F₃.map_comp, NatTrans.comp_app, comp_apply, comp_apply, ht', elementwise_of% f₂.naturality, H.choose_spec]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ imageSieve (f₁ ≫ f₂) s ∈ sieves J U
[PROOFSTEP]
apply J.superset_covering this
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ∈ sieves J U
[PROOFSTEP]
apply J.bind_covering
[GOAL]
case hS
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ imageSieve f₂ s ∈ sieves J U
[PROOFSTEP]
apply h₂
[GOAL]
case hR
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U⦄ (H : (imageSieve f₂ s).arrows f), imageSieve f₁ (Exists.choose H) ∈ sieves J Y
[PROOFSTEP]
intros
[GOAL]
case hR
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
Y✝ : C
f✝ : Y✝ ⟶ U
H✝ : (imageSieve f₂ s).arrows f✝
⊢ imageSieve f₁ (Exists.choose H✝) ∈ sieves J Y✝
[PROOFSTEP]
apply h₁
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ toSheafify J F ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    toSheafify J F ≫ 𝟙 (sheafify J F)
[PROOFSTEP]
simp [toImagePresheafSheafify]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
        (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) =
    𝟙 (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))
[PROOFSTEP]
rw [← cancel_mono (Subpresheaf.ι _), Category.id_comp, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F)))
[PROOFSTEP]
refine' Eq.trans _ (Category.comp_id _)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫ 𝟙 (sheafify J F)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
        (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
      Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    𝟙 (sheafify J F)
[PROOFSTEP]
exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [toImagePresheafSheafify])
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ toSheafify J F ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    toSheafify J F ≫ 𝟙 (sheafify J F)
[PROOFSTEP]
simp [toImagePresheafSheafify]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (toSheafify J F)
[PROOFSTEP]
rw [isLocallySurjective_iff_whisker_forget, ← toSheafify_comp_sheafifyCompIso_inv]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (toSheafify J (F ⋙ forget B) ≫ (sheafifyCompIso J (forget B) F).inv)
[PROOFSTEP]
apply IsLocallySurjective.comp
[GOAL]
case h₁
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (toSheafify J (F ⋙ forget B))
[PROOFSTEP]
rw [isLocallySurjective_iff_imagePresheaf_sheafify_eq_top, Subpresheaf.eq_top_iff_isIso]
[GOAL]
case h₁
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsIso
    (Subpresheaf.ι
      (Subpresheaf.sheafify J (imagePresheaf (whiskerRight (toSheafify J (F ⋙ forget B)) (forget (Type (max u v)))))))
[PROOFSTEP]
exact IsIso.of_iso_inv (sheafificationIsoImagePresheaf J (F ⋙ forget B))
[GOAL]
case h₂
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (sheafifyCompIso J (forget B) F).inv
[PROOFSTEP]
exact isLocallySurjective_of_iso _ _


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.611, u_1} C
inst✝ : Precoherent C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Presieve X),
    S ∈ (fun B => {S | ∃ α x X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}) X →
      ∃ T,
        T ∈ (fun B => {S | ∃ α x X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}) Y ∧
          Presieve.FactorsThruAlong T S f
[PROOFSTEP]
rintro B₁ B₂ f S ⟨α, _, X₁, π₁, rfl, hS⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{?u.611, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝ : Fintype α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
⊢ ∃ T,
    T ∈ (fun B => {S | ∃ α x X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}) B₂ ∧
      Presieve.FactorsThruAlong T (Presieve.ofArrows X₁ π₁) f
[PROOFSTEP]
obtain ⟨β, _, X₂, π₂, h, i, ι, hh⟩ := Precoherent.pullback f α X₁ π₁ hS
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{?u.611, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Fintype α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Fintype β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ T,
    T ∈ (fun B => {S | ∃ α x X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}) B₂ ∧
      Presieve.FactorsThruAlong T (Presieve.ofArrows X₁ π₁) f
[PROOFSTEP]
refine ⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{?u.611, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Fintype α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Fintype β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ Presieve.FactorsThruAlong (Presieve.ofArrows X₂ π₂) (Presieve.ofArrows X₁ π₁) f
[PROOFSTEP]
rintro _ _ ⟨b⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk
C : Type u_1
inst✝¹ : Category.{?u.611, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Fintype α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Fintype β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
Y : C
b : β
⊢ ∃ W i e, Presieve.ofArrows X₁ π₁ e ∧ i ≫ e = π₂ b ≫ f
[PROOFSTEP]
refine ⟨(X₁ (i b)), ι _, π₁ _, ⟨_⟩, hh _⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P →
    ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
[PROOFSTEP]
intro hP B α _ X π h
[GOAL]
case mp
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Fintype α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
[PROOFSTEP]
simp only [coherentTopology, Presieve.isSheaf_coverage] at hP
[GOAL]
case mp
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Fintype α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C} (R : Presieve X), R ∈ Coverage.covering (coherentCoverage C) X → Presieve.IsSheafFor P R
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
[PROOFSTEP]
apply hP
[GOAL]
case mp.a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
B : C
α : Type
inst✝ : Fintype α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP : ∀ {X : C} (R : Presieve X), R ∈ Coverage.covering (coherentCoverage C) X → Presieve.IsSheafFor P R
⊢ Presieve.ofArrows X π ∈ Coverage.covering (coherentCoverage C) B
[PROOFSTEP]
refine ⟨α, inferInstance, X, π, rfl, h⟩
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ (∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)) →
    Presieve.IsSheaf (coherentTopology C) P
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf (coherentTopology C) P
[PROOFSTEP]
simp only [coherentTopology, Presieve.isSheaf_coverage]
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ ∀ {X : C} (R : Presieve X), R ∈ Coverage.covering (coherentCoverage C) X → Presieve.IsSheafFor P R
[PROOFSTEP]
rintro B S ⟨α, _, X, π, rfl, hS⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
h :
  ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
B : C
α : Type
w✝ : Fintype α
X : α → C
π : (a : α) → X a ⟶ B
hS : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
[PROOFSTEP]
exact h _ _ _ _ hS
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
rintro ⟨α, ⟨h, ⟨Y, ⟨π, hπ⟩⟩⟩⟩
[GOAL]
case intro.intro.intro.intro
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
have h_le : Sieve.generate (Presieve.ofArrows _ π) ≤ S :=
  by
  rw [Sieve.sets_iff_generate (Presieve.ofArrows _ π) S]
  apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows (fun i => Y i) π) S _
  intro W g f
  use W, 𝟙 W
  rcases f with ⟨i⟩
  exact ⟨π i, ⟨hπ.2 i, Category.id_comp (π i)⟩⟩
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Sieve.generate (Presieve.ofArrows (fun i => Y i) π) ≤ S
[PROOFSTEP]
rw [Sieve.sets_iff_generate (Presieve.ofArrows _ π) S]
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows (fun i => Y i) π ≤ S.arrows
[PROOFSTEP]
apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows (fun i => Y i) π) S _
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.FactorsThru (Presieve.ofArrows (fun i => Y i) π) S.arrows
[PROOFSTEP]
intro W g f
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun i => Y i) π g
⊢ ∃ W_1 i e, S.arrows e ∧ i ≫ e = g
[PROOFSTEP]
use W, 𝟙 W
[GOAL]
case h
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun i => Y i) π g
⊢ ∃ e, S.arrows e ∧ 𝟙 W ≫ e = g
[PROOFSTEP]
rcases f with ⟨i⟩
[GOAL]
case h.mk
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
hπ : EffectiveEpiFamily Y✝ π ∧ ∀ (a : α), S.arrows (π a)
Y : C
i : α
⊢ ∃ e, S.arrows e ∧ 𝟙 (Y✝ i) ≫ e = π i
[PROOFSTEP]
exact ⟨π i, ⟨hπ.2 i, Category.id_comp (π i)⟩⟩
[GOAL]
case intro.intro.intro.intro
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
h_le : Sieve.generate (Presieve.ofArrows (fun i => Y i) π) ≤ S
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
apply Coverage.saturate_of_superset (coherentCoverage C) h_le
[GOAL]
case intro.intro.intro.intro
C✝ : Type u_1
inst✝² : Category.{?u.3154, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
h : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
h_le : Sieve.generate (Presieve.ofArrows (fun i => Y i) π) ≤ S
⊢ Coverage.saturate (coherentCoverage C) X (Sieve.generate (Presieve.ofArrows (fun i => Y i) π))
[PROOFSTEP]
exact Coverage.saturate.of X _ ⟨α, inferInstance, Y, π, ⟨rfl, hπ.1⟩⟩
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X W : C
⊢ Presieve.IsSheaf (coherentTopology C) (yoneda.obj W)
[PROOFSTEP]
rw [isSheaf_coherent]
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X W : C
⊢ ∀ (B : C) (α : Type) [inst : Fintype α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X π)
[PROOFSTEP]
intro X α _ Y π H
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
[PROOFSTEP]
have h_colim := isColimitOfEffectiveEpiFamilyStruct Y π H.effectiveEpiFamily.some
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generateFamily Y π).arrows)
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
[PROOFSTEP]
rw [← Sieve.generateFamily_eq] at h_colim
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
[PROOFSTEP]
intro x hx
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let x_ext := Presieve.FamilyOfElements.sieveExtend x
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have hx_ext := Presieve.FamilyOfElements.Compatible.sieveExtend hx
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
hx_ext : Presieve.FamilyOfElements.Compatible (Presieve.FamilyOfElements.sieveExtend x)
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let S := Sieve.generate (Presieve.ofArrows Y π)
[GOAL]
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
hx_ext : Presieve.FamilyOfElements.Compatible (Presieve.FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
obtain ⟨t, t_amalg, t_uniq⟩ : ∃! t, x_ext.IsAmalgamation t :=
  (Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext
[GOAL]
case intro.intro
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
hx_ext : Presieve.FamilyOfElements.Compatible (Presieve.FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : Presieve.FamilyOfElements.IsAmalgamation x_ext t
t_uniq :
  ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine ⟨t, ?_, ?_⟩
[GOAL]
case intro.intro.refine_1
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
hx_ext : Presieve.FamilyOfElements.Compatible (Presieve.FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : Presieve.FamilyOfElements.IsAmalgamation x_ext t
t_uniq :
  ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ (fun t => Presieve.FamilyOfElements.IsAmalgamation x t) t
[PROOFSTEP]
convert Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg
[GOAL]
case h.e.h.e'_6.h.h.h
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
hx_ext : Presieve.FamilyOfElements.Compatible (Presieve.FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : Presieve.FamilyOfElements.IsAmalgamation x_ext t
t_uniq :
  ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ x =
    Presieve.FamilyOfElements.restrict (_ : Presieve.ofArrows Y π ≤ (Sieve.generate (Presieve.ofArrows Y π)).arrows)
      x_ext
[PROOFSTEP]
exact (Presieve.restrict_extend hx).symm
[GOAL]
case intro.intro.refine_2
C✝ : Type u_1
inst✝³ : Category.{?u.4892, u_1} C✝
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Precoherent C
X✝ W X : C
α : Type
inst✝ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : IsColimit (Presieve.cocone (Sieve.generate (Presieve.ofArrows Y π)).arrows)
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : Presieve.FamilyOfElements.Compatible x
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  Presieve.FamilyOfElements.sieveExtend x
hx_ext : Presieve.FamilyOfElements.Compatible (Presieve.FamilyOfElements.sieveExtend x)
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : Presieve.FamilyOfElements.IsAmalgamation x_ext t
t_uniq :
  ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x_ext t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x t) y → y = t
[PROOFSTEP]
exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst
[PROOFSTEP]
rw [← Sieve.effectiveEpimorphic_family]
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
[PROOFSTEP]
suffices h₂ :
  (Sieve.generate (Presieve.ofArrows (fun (⟨a, b⟩ : Σ _, β _) => Y_n a b) (fun ⟨a, b⟩ => π_n a b ≫ π a))) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
  by
  change Nonempty _
  rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
  exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
[PROOFSTEP]
change Nonempty _
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ Nonempty
    (IsColimit
      (Presieve.cocone
        (Sieve.generate (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows))
[PROOFSTEP]
rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor (yoneda.obj W)
      (Sieve.generate (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
[PROOFSTEP]
exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
let h' := h
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpiFamily Y π := h
⊢ Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
rw [← Sieve.effectiveEpimorphic_family] at h'
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
⊢ Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
let H' := H
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
⊢ Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
conv at H' =>
  intro a
  rw [← Sieve.effectiveEpimorphic_family]
    -- Show that a covering sieve is a colimit, which implies the original set of arrows is regular
      -- epimorphic. We use the transitivity property of saturation
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
| ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
[PROOFSTEP]
  intro a
  rw [← Sieve.effectiveEpimorphic_family]
    -- Show that a covering sieve is a colimit, which implies the original set of arrows is regular
      -- epimorphic. We use the transitivity property of saturation
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
| ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
[PROOFSTEP]
  intro a
  rw [← Sieve.effectiveEpimorphic_family]
    -- Show that a covering sieve is a colimit, which implies the original set of arrows is regular
      -- epimorphic. We use the transitivity property of saturation
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
| ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
[PROOFSTEP]
intro a
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
a : α
| EffectiveEpiFamily (Y_n a) (π_n a)
[PROOFSTEP]
rw [← Sieve.effectiveEpimorphic_family]
  -- Show that a covering sieve is a colimit, which implies the original set of arrows is regular
    -- epimorphic. We use the transitivity property of saturation
[GOAL]
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
⊢ Sieve.generate
      (Presieve.ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
apply Coverage.saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
[GOAL]
case a
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
⊢ Coverage.saturate (coherentCoverage C) X (Sieve.generate (Presieve.ofArrows Y π))
[PROOFSTEP]
apply Coverage.saturate.of
[GOAL]
case a.hS
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
⊢ Presieve.ofArrows Y π ∈ Coverage.covering (coherentCoverage C) X
[PROOFSTEP]
use α, inferInstance, Y, π
[GOAL]
case a
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      Coverage.saturate (coherentCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (Presieve.ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a)))
[PROOFSTEP]
intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
[GOAL]
case a
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)))
[PROOFSTEP]
rw [← hf, Sieve.pullback_comp]
[GOAL]
case a
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows
            (fun x =>
              match x with
              | { fst := a, snd := b } => Y_n a b)
            fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a))))
[PROOFSTEP]
apply (coherentTopology C).pullback_stable'
[GOAL]
case a.a
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ Sieve.pullback g
      (Sieve.generate
        (Presieve.ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)) ∈
    GrothendieckTopology.sieves (coherentTopology C) Y₁
[PROOFSTEP]
apply coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
[GOAL]
case a.a.a
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ ∃ α_1 x Y_1 π_1,
    EffectiveEpiFamily Y_1 π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback g
              (Sieve.generate
                (Presieve.ofArrows
                  (fun x =>
                    match x with
                    | { fst := a, snd := b } => Y_n a b)
                  fun x =>
                  match x with
                  | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
          (π_1 a)
[PROOFSTEP]
rcases hY with ⟨i⟩
[GOAL]
case a.a.a.mk
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y✝ π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∃ α_1 x Y π_1,
    EffectiveEpiFamily Y π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback (π i)
              (Sieve.generate
                (Presieve.ofArrows
                  (fun x =>
                    match x with
                    | { fst := a, snd := b } => Y_n a b)
                  fun x =>
                  match x with
                  | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
          (π_1 a)
[PROOFSTEP]
use β i, inferInstance, Y_n i, π_n i, H i
[GOAL]
case right
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y✝ π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∀ (a : β i),
    (Sieve.pullback (π i)
          (Sieve.generate
            (Presieve.ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
      (π_n i a)
[PROOFSTEP]
intro b
[GOAL]
case right
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y✝ π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ (Sieve.pullback (π i)
        (Sieve.generate
          (Presieve.ofArrows
            (fun x =>
              match x with
              | { fst := a, snd := b } => Y_n a b)
            fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
    (π_n i b)
[PROOFSTEP]
use Y_n i b, (𝟙 _), π_n i b ≫ π i, ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩
[GOAL]
case right
C✝ : Type u_1
inst✝⁴ : Category.{?u.13158, u_1} C✝
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : Presieve.EffectiveEpimorphic (Presieve.ofArrows Y✝ π)
H' : ∀ (a : α), Presieve.EffectiveEpimorphic (Presieve.ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ 𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i
[PROOFSTEP]
exact Category.id_comp (π_n i b ≫ π i)
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X ↔ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
[PROOFSTEP]
constructor
[GOAL]
case mp
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X → ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
[PROOFSTEP]
intro h
[GOAL]
case mp
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
[PROOFSTEP]
induction' h with Y T hS Y Y R S _ _ a b
[GOAL]
case mp.of
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ Coverage.covering (coherentCoverage C) Y
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
[PROOFSTEP]
rcases hS with ⟨a, h, Y', π, h'⟩
[GOAL]
case mp.of.intro.intro.intro.intro
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
[PROOFSTEP]
use a, h, Y', π, by tauto
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ EffectiveEpiFamily Y' π
[PROOFSTEP]
tauto
[GOAL]
case right
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∀ (a : a), (Sieve.generate T).arrows (π a)
[PROOFSTEP]
intro a'
[GOAL]
case right
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π ∧ EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')
[PROOFSTEP]
rcases h' with ⟨rfl, _⟩
[GOAL]
case right.intro
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
right✝ : EffectiveEpiFamily Y' π
⊢ (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')
[PROOFSTEP]
simp only [Sieve.generate_apply]
[GOAL]
case right.intro
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
right✝ : EffectiveEpiFamily Y' π
⊢ ∃ Y_1 h g, Presieve.ofArrows Y' π g ∧ h ≫ g = π a'
[PROOFSTEP]
use Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a'
[GOAL]
case right
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
right✝ : EffectiveEpiFamily Y' π
⊢ 𝟙 Y' a' ≫ π a' = π a'
[PROOFSTEP]
apply Category.id_comp
[GOAL]
case mp.top
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), ⊤.arrows (π a)
[PROOFSTEP]
use Unit, Unit.fintype, fun _ => Y, fun _ => (𝟙 Y)
[GOAL]
case h
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ (EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y) ∧ (Unit → ⊤.arrows (𝟙 Y))
[PROOFSTEP]
cases' S with arrows downward_closed
[GOAL]
case h.mk
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ (EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y) ∧ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)
[PROOFSTEP]
exact ⟨inferInstance, by simp only [Sieve.top_apply, forall_const]⟩
[GOAL]
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)
[PROOFSTEP]
simp only [Sieve.top_apply, forall_const]
[GOAL]
case mp.transitive
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
a : ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
[PROOFSTEP]
rcases a with ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩
[GOAL]
case mp.transitive.intro.intro.intro.intro.intro
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
[PROOFSTEP]
choose β _ Y_n π_n H using fun a => b (h₂ a)
[GOAL]
case mp.transitive.intro.intro.intro.intro.intro
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
[PROOFSTEP]
use(Σ a, β a), inferInstance, fun ⟨a, b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a)
[GOAL]
case h
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ (EffectiveEpiFamily
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a) ∧
    ∀ (a : (a : α) × β a),
      S.arrows
        (match a with
        | { fst := a, snd := b } => π_n a b ≫ π a)
[PROOFSTEP]
constructor
[GOAL]
case h.left
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ EffectiveEpiFamily
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    fun x =>
    match x with
    | { fst := a, snd := b } => π_n a b ≫ π a
[PROOFSTEP]
exact EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1)
[GOAL]
case h.right
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∀ (a : (a : α) × β a),
    S.arrows
      (match a with
      | { fst := a, snd := b } => π_n a b ≫ π a)
[PROOFSTEP]
exact fun c => (H c.fst).2 c.snd
[GOAL]
case mpr
C✝ : Type u_1
inst✝² : Category.{?u.18072, u_1} C✝
C : Type u_2
inst✝¹ : Category.{u_3, u_2} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
[PROOFSTEP]
exact coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S