feat(CategoryTheory): Preregular and FinitaryPreExtensive implies Precoherent (#8643)

We prove some results about effective epimorphisms which allow us to deduce that a category which is `FinitaryPreExtensive` and `Preregular` is also `Precoherent`.

Author: dagurtomas

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -254,6 +254,11 @@ abbrev Sigma.desc {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P)
   colimit.desc _ (Cofan.mk P p)
 #align category_theory.limits.sigma.desc CategoryTheory.Limits.Sigma.desc
 
+instance {f : β → C} [HasCoproduct f] : IsIso (Sigma.desc (fun a ↦ Sigma.ι f a)) := by
+  convert IsIso.id _
+  ext
+  simp
+
 /-- A version of `Cocones.ext` for `Cofan`s. -/
 @[simps!]
 def Cofan.ext {f : β → C} {c₁ c₂ : Cofan f} (e : c₁.pt ≅ c₂.pt)

Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

@@ -6,6 +6,7 @@ Authors: Adam Topaz
 
 import Mathlib.CategoryTheory.Sites.Sieves
 import Mathlib.CategoryTheory.Limits.Shapes.KernelPair
+import Mathlib.Tactic.ApplyFun
 
 /-!
 
@@ -32,9 +33,10 @@ our notion of `EffectiveEpi` is often called "strict epi" in the literature.
 - [nlab: *Effective Epimorphism*](https://ncatlab.org/nlab/show/effective+epimorphism) and
 - [Stacks 00WP](https://stacks.math.columbia.edu/tag/00WP) for the standard definitions.
 
--/
+## TODO
+- Find sufficient conditions on functors to preserve/reflect effective epis.
 
-set_option autoImplicit true
+-/
 
 namespace CategoryTheory
 
@@ -303,12 +305,12 @@ attribute [nolint simpNF]
   EffectiveEpiFamily.fac_assoc
 
 /-- The effective epi family structure on the identity -/
-def effectiveEpiFamilyStructId : EffectiveEpiFamilyStruct (α : Unit → C) (fun _ => 𝟙 (α ())) where
+def effectiveEpiFamilyStructId {α : Unit → C} : EffectiveEpiFamilyStruct α (fun _ => 𝟙 (α ())) where
   desc := fun e _ => e ()
   fac := by aesop_cat
   uniq := by aesop_cat
 
-instance : EffectiveEpiFamily (fun _ => X : Unit → C) (fun _ => 𝟙 X) :=
+instance {X : C} : EffectiveEpiFamily (fun _ => X : Unit → C) (fun _ => 𝟙 X) :=
   ⟨⟨effectiveEpiFamilyStructId⟩⟩
 
 example {B W : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B))
@@ -455,8 +457,9 @@ Given an `EffectiveEpiFamily X π` such that the coproduct of `X` exists, `Sigma
 `EffectiveEpi`.
 -/
 noncomputable
-def EffectiveEpiFamily_descStruct {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B))
-    [HasCoproduct X] [EffectiveEpiFamily X π] : EffectiveEpiStruct (Sigma.desc π) where
+def effectiveEpiStructDescOfEffectiveEpiFamily {B : C} {α : Type*} (X : α → C)
+    (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpiFamily X π] :
+    EffectiveEpiStruct (Sigma.desc π) where
   desc e h := EffectiveEpiFamily.desc X π (fun a ↦ Sigma.ι X a ≫ e) (fun a₁ a₂ g₁ g₂ hg ↦ by
     simp only [← Category.assoc]
     apply h (g₁ ≫ Sigma.ι X a₁) (g₂ ≫ Sigma.ι X a₂)
@@ -478,26 +481,88 @@ def EffectiveEpiFamily_descStruct {B : C} {α : Type*} (X : α → C) (π : (a :
 
 instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X]
     [EffectiveEpiFamily X π] : EffectiveEpi (Sigma.desc π) :=
-  ⟨⟨EffectiveEpiFamily_descStruct X π⟩⟩
+  ⟨⟨effectiveEpiStructDescOfEffectiveEpiFamily X π⟩⟩
+
+/--
+This is an auxiliary lemma used twice in the definition of  `EffectiveEpiFamilyOfEffectiveEpiDesc`.
+It is the `h` hypothesis of `EffectiveEpi.desc` and `EffectiveEpi.fac`. 
+-/
+theorem effectiveEpiFamilyStructOfEffectiveEpiDesc_aux {B : C} {α : Type*} {X : α → C}
+    {π : (a : α) → X a ⟶ B} [HasCoproduct X]
+    [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)]
+    [∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)]
+    [∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst (f := g) (g := (Sigma.ι X a)))]
+    {W : C} {e : (a : α) → X a ⟶ W} (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
+      g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) {Z : C}
+    {g₁ g₂ : Z ⟶ ∐ fun b ↦ X b} (hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π) :
+    g₁ ≫ Sigma.desc e = g₂ ≫ Sigma.desc e := by
+  apply_fun ((Sigma.desc fun a ↦ pullback.fst (f := g₁) (g := (Sigma.ι X a))) ≫ ·) using
+    (fun a b ↦ (cancel_epi _).mp)
+  ext a
+  simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app]
+  rw [← Category.assoc, pullback.condition]
+  simp only [Category.assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
+  apply_fun ((Sigma.desc fun a ↦ pullback.fst (f := pullback.fst ≫ g₂)
+    (g := (Sigma.ι X a))) ≫ ·) using (fun a b ↦ (cancel_epi _).mp)
+  ext b
+  simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app]
+  simp only [← Category.assoc]
+  rw [(Category.assoc _ _ g₂), pullback.condition]
+  simp only [Category.assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
+  rw [← Category.assoc]
+  apply h
+  apply_fun (pullback.fst (f := g₁) (g := (Sigma.ι X a)) ≫ ·) at hg
+  rw [← Category.assoc, pullback.condition] at hg
+  simp only [Category.assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app] at hg
+  apply_fun ((Sigma.ι (fun a ↦ pullback _ _) b) ≫ (Sigma.desc fun a ↦ pullback.fst
+    (f := pullback.fst ≫ g₂) (g := (Sigma.ι X a))) ≫ ·) at hg
+  simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app] at hg
+  simp only [← Category.assoc] at hg
+  rw [(Category.assoc _ _ g₂), pullback.condition] at hg
+  simpa using hg
+
+/--
+If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of
+the coproduct is effective epimorphic whenever `Sigma.desc` induces an effective epimorphism from
+the coproduct itself.
+-/
+noncomputable
+def effectiveEpiFamilyStructOfEffectiveEpiDesc {B : C} {α : Type*} (X : α → C)
+    (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpi (Sigma.desc π)]
+    [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)]
+    [∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct (fun a ↦ pullback g (Sigma.ι X a))]
+    [∀ {Z : C} (g : Z ⟶ ∐ X),
+      Epi (Sigma.desc (fun a ↦ pullback.fst (f := g) (g := (Sigma.ι X a))))] :
+    EffectiveEpiFamilyStruct X π where
+  desc e h := EffectiveEpi.desc (Sigma.desc π) (Sigma.desc e) fun _ _ hg ↦
+    effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg
+  fac e h a := by
+    rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
+      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
+      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]
+  uniq _ _ _ hm := by
+    apply EffectiveEpi.uniq (Sigma.desc π)
+    ext
+    simpa using hm _
 
 /--
 An `EffectiveEpiFamily` consisting of a single `EffectiveEpi`
 -/
 noncomputable
-def EffectiveEpi_familyStruct {B X : C} (f : X ⟶ B) [EffectiveEpi f] :
+def effectiveEpiFamilyStructSingletonOfEffectiveEpi {B X : C} (f : X ⟶ B) [EffectiveEpi f] :
     EffectiveEpiFamilyStruct (fun () ↦ X) (fun () ↦ f) where
   desc e h := EffectiveEpi.desc f (e ()) (fun g₁ g₂ hg ↦ h () () g₁ g₂ hg)
   fac e h := fun _ ↦ EffectiveEpi.fac f (e ()) (fun g₁ g₂ hg ↦ h () () g₁ g₂ hg)
   uniq e h m hm := by apply EffectiveEpi.uniq f (e ()) (h () ()); exact hm ()
 
 instance {B X : C} (f : X ⟶ B) [EffectiveEpi f] : EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f) :=
-  ⟨⟨EffectiveEpi_familyStruct f⟩⟩
+  ⟨⟨effectiveEpiFamilyStructSingletonOfEffectiveEpi f⟩⟩
 
 /--
 A single element `EffectiveEpiFamily` constists of an `EffectiveEpi`
 -/
 noncomputable
-def EffectiveEpiStruct_ofFamily {B X : C} (f : X ⟶ B)
+def effectiveEpiStructOfEffectiveEpiFamilySingleton {B X : C} (f : X ⟶ B)
     [EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f)] :
     EffectiveEpiStruct f where
   desc e h := EffectiveEpiFamily.desc
@@ -509,9 +574,9 @@ def EffectiveEpiStruct_ofFamily {B X : C} (f : X ⟶ B)
 
 instance {B X : C} (f : X ⟶ B) [EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f)] :
     EffectiveEpi f :=
-  ⟨⟨EffectiveEpiStruct_ofFamily f⟩⟩
+  ⟨⟨effectiveEpiStructOfEffectiveEpiFamilySingleton f⟩⟩
 
-lemma effectiveEpi_iff_effectiveEpiFamily {B X : C} (f : X ⟶ B) :
+theorem effectiveEpi_iff_effectiveEpiFamily {B X : C} (f : X ⟶ B) :
     EffectiveEpi f ↔ EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f) :=
   ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
 
@@ -520,7 +585,7 @@ A family of morphisms with the same target inducing an isomorphism from the copr
 is an `EffectiveEpiFamily`.
 -/
 noncomputable
-def EffectiveEpiFamilyStruct_of_isIso_desc {B : C} {α : Type*} (X : α → C)
+def effectiveEpiFamilyStructOfIsIsoDesc {B : C} {α : Type*} (X : α → C)
     (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [IsIso (Sigma.desc π)] :
     EffectiveEpiFamilyStruct X π where
   desc e _ := (asIso (Sigma.desc π)).inv ≫ (Sigma.desc e)
@@ -540,34 +605,51 @@ def EffectiveEpiFamilyStruct_of_isIso_desc {B : C} {α : Type*} (X : α → C)
 
 instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X]
     [IsIso (Sigma.desc π)] : EffectiveEpiFamily X π :=
-  ⟨⟨EffectiveEpiFamilyStruct_of_isIso_desc X π⟩⟩
+  ⟨⟨effectiveEpiFamilyStructOfIsIsoDesc X π⟩⟩
 
 /-- The identity is an effective epi. -/
-def EffectiveEpiStructId {X : C} : EffectiveEpiStruct (𝟙 X) where
-  desc e _ := e
-  fac _ _ := by simp only [Category.id_comp]
-  uniq _ _ _ h := by simp only [Category.id_comp] at h; exact h
-
-instance {X : C} : EffectiveEpi (𝟙 X) := ⟨⟨EffectiveEpiStructId⟩⟩
-
-end instances
+noncomputable
+def effectiveEpiStructOfIsIso {X Y : C} (f : X ⟶ Y) [IsIso f] : EffectiveEpiStruct f where
+  desc e _ := inv f ≫ e
+  fac _ _ := by simp
+  uniq _ _ _ h := by simpa using h
 
-section Epi
+instance {X Y : C} (f : X ⟶ Y) [IsIso f] : EffectiveEpi f := ⟨⟨effectiveEpiStructOfIsIso f⟩⟩
 
-variable [HasFiniteCoproducts C] (h : ∀ {α : Type} [Fintype α] {B : C}
-    (X : α → C) (π : (a : α) → (X a ⟶ B)), EffectiveEpiFamily X π ↔ Epi (Sigma.desc π ))
+/--
+A split epi followed by an effective epi is an effective epi. This version takes an explicit section
+to the split epi, and is mainly used to define `effectiveEpiStructCompOfEffectiveEpiSplitEpi`,
+which takes a `IsSplitEpi` instance instead.
+-/
+noncomputable
+def effectiveEpiStructCompOfEffectiveEpiSplitEpi' {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) (i : X ⟶ Y)
+    (hi : i ≫ g = 𝟙 _) [EffectiveEpi f] : EffectiveEpiStruct (g ≫ f) where
+  desc e w := EffectiveEpi.desc f (i ≫ e) fun g₁ g₂ _ ↦ (by
+    simp only [← Category.assoc]
+    apply w (g₁ ≫ i) (g₂ ≫ i)
+    simpa [← Category.assoc, hi])
+  fac e w := by
+    simp only [Category.assoc, EffectiveEpi.fac]
+    rw [← Category.id_comp e, ← Category.assoc, ← Category.assoc]
+    apply w
+    simp only [Category.comp_id, Category.id_comp, ← Category.assoc]
+    aesop
+  uniq _ _ _ hm := by
+    apply EffectiveEpi.uniq f
+    rw [← hm, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
+
+/-- A split epi followed by an effective epi is an effective epi. -/
+noncomputable
+def effectiveEpiStructCompOfEffectiveEpiSplitEpi {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) [IsSplitEpi g]
+    [EffectiveEpi f] : EffectiveEpiStruct (g ≫ f) :=
+  effectiveEpiStructCompOfEffectiveEpiSplitEpi' f g
+    (IsSplitEpi.exists_splitEpi (f := g)).some.section_
+    (IsSplitEpi.exists_splitEpi (f := g)).some.id
 
-lemma effectiveEpi_iff_epi {X Y : C} (f : X ⟶ Y) : EffectiveEpi f ↔ Epi f := by
-  rw [effectiveEpi_iff_effectiveEpiFamily, h]
-  have w : f = (Limits.Sigma.ι (fun () ↦ X) ()) ≫ (Limits.Sigma.desc (fun () ↦ f))
-  · simp only [Limits.colimit.ι_desc, Limits.Cofan.mk_pt, Limits.Cofan.mk_ι_app]
-  refine ⟨?_, fun _ ↦ epi_of_epi_fac w.symm⟩
-  intro
-  rw [w]
-  have : Epi (Limits.Sigma.ι (fun () ↦ X) ()) := ⟨fun _ _ h ↦ by ext; exact h⟩
-  exact epi_comp _ _
+instance {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) [IsSplitEpi g] [EffectiveEpi f] :
+    EffectiveEpi (g ≫ f) := ⟨⟨effectiveEpiStructCompOfEffectiveEpiSplitEpi f g⟩⟩
 
-end Epi
+end instances
 
 section Regular
 
@@ -615,4 +697,21 @@ noncomputable instance regularEpiOfEffectiveEpi {B X : C} (f : X ⟶ B) [HasPull
 
 end Regular
 
+section Epi
+
+variable [HasFiniteCoproducts C] (h : ∀ {α : Type} [Fintype α] {B : C}
+    (X : α → C) (π : (a : α) → (X a ⟶ B)), EffectiveEpiFamily X π ↔ Epi (Sigma.desc π ))
+
+lemma effectiveEpi_iff_epi {X Y : C} (f : X ⟶ Y) : EffectiveEpi f ↔ Epi f := by
+  rw [effectiveEpi_iff_effectiveEpiFamily, h]
+  have w : f = (Limits.Sigma.ι (fun () ↦ X) ()) ≫ (Limits.Sigma.desc (fun () ↦ f))
+  · simp only [Limits.colimit.ι_desc, Limits.Cofan.mk_pt, Limits.Cofan.mk_ι_app]
+  refine ⟨?_, fun _ ↦ epi_of_epi_fac w.symm⟩
+  intro
+  rw [w]
+  have : Epi (Limits.Sigma.ι (fun () ↦ X) ()) := ⟨fun _ _ h ↦ by ext; exact h⟩
+  exact epi_comp _ _
+
+end Epi
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/RegularExtensive.lean

@@ -27,6 +27,8 @@ disjoint.
 
 ## Main results
 
+* `instance : Precoherent C` given `Preregular C` and `FinitaryPreExtensive C`.
+
 * `extensive_union_regular_generates_coherent`: the union of the regular and extensive coverages
   generates the coherent topology on `C` if `C` is precoherent, preextensive and preregular.
 
@@ -40,11 +42,6 @@ disjoint.
 * `isSheaf_iff_preservesFiniteProducts`: In a finitary extensive category, the sheaves for the
   extensive topology are precisely those preserving finite products.
 
-TODO: figure out under what conditions `Preregular` and `Extensive` are implied by `Precoherent` and
-vice versa.
-
-TODO: refactor the section `RegularSheaves` to use the new `Arrows` sheaf API.
-
 -/
 
 universe v u w
@@ -77,6 +74,16 @@ class Preregular : Prop where
   exists_fac : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g],
     (∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f)
 
+instance [Precoherent C] [HasFiniteCoproducts C] : Preregular C where
+  exists_fac {X Y Z} f g _ := by
+    have hp := Precoherent.pullback f PUnit (fun () ↦ Z) (fun () ↦ g)
+    simp only [exists_const] at hp
+    rw [← effectiveEpi_iff_effectiveEpiFamily g] at hp
+    obtain ⟨β, _, X₂, π₂, h, ι, hι⟩ := hp inferInstance
+    refine ⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩
+    ext b
+    simpa using hι b
+
 /--
 The regular coverage on a regular category `C`.
 -/
@@ -117,9 +124,32 @@ def extensiveCoverage [FinitaryPreExtensive C] : Coverage C where
       rw [hS]
       exact Presieve.ofArrows.mk a
 
+theorem effectiveEpi_desc_iff_effectiveEpiFamily [FinitaryPreExtensive C] {α : Type} [Fintype α]
+    {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) :
+    EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π := by
+  exact ⟨fun h ↦ ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _ (fun g ↦
+    (FinitaryPreExtensive.sigma_desc_iso (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩,
+    fun _ ↦ inferInstance⟩
+
+instance [FinitaryPreExtensive C] [Preregular C] : Precoherent C where
+  pullback {B₁ B₂} f α _ X₁ π₁ h := by
+    refine ⟨α, inferInstance, ?_⟩
+    obtain ⟨Y, g, _, g', hg⟩ := Preregular.exists_fac f (Sigma.desc π₁)
+    let X₂ := fun a ↦ pullback g' (Sigma.ι X₁ a)
+    let π₂ := fun a ↦ pullback.fst (f := g') (g := Sigma.ι X₁ a) ≫ g
+    let π' := fun a ↦ pullback.fst (f := g') (g := Sigma.ι X₁ a)
+    have _ := FinitaryPreExtensive.sigma_desc_iso (fun a ↦ Sigma.ι X₁ a) g' inferInstance
+    refine ⟨X₂, π₂, ?_, ?_⟩
+    · have : (Sigma.desc π' ≫ g) = Sigma.desc π₂ := by ext; simp
+      rw [← effectiveEpi_desc_iff_effectiveEpiFamily, ← this]
+      infer_instance
+    · refine ⟨id, fun b ↦ pullback.snd, fun b ↦ ?_⟩
+      simp only [id_eq, Category.assoc, ← hg]
+      rw [← Category.assoc, pullback.condition]
+      simp
 
 /-- The union of the extensive and regular coverages generates the coherent topology on `C`. -/
-lemma extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] [Precoherent C] :
+lemma extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] :
     ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck =
     (coherentTopology C) := by
   ext B S