The Regular and Extensive Coverages

This file defines two coverages on a category C.

The first one is called the regular coverage and for that to exist, the category C must satisfy a condition called Preregular C. This means that effective epimorphisms can be "pulled back". The covering sieves of this coverage are generated by presieves consisting of a single effective epimorphism.

The second one is called the extensive coverage and for that to exist, the category C must satisfy a condition called Extensive C. This means C has finite coproducts and that those are preserved by pullbacks. The covering sieves of this coverage are generated by presieves consisting finitely many arrows that together induce an isomorphism from the coproduct to the target.

In extensive_union_regular_generates_coherent, we prove that the union of these two coverages generates the coherent topology on C if C is precoherent, extensive and regular.

TODO: figure out under what conditions Preregular and Extensive are implied by Precoherent and vice versa.

class CategoryTheory.Preregular (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• exists_fac : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [inst : CategoryTheory.EffectiveEpi g], ∃ W h x i, CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f

  For X, Y, Z, f, g like in the diagram, where g is an effective epi, there exists an object W, an effective epi h : W ⟶ X and a morphism i : W ⟶ Z making the diagram commute.

  W --i-→ Z
  |       |
  h       g
  ↓       ↓
  X --f-→ Y
  

The condition Preregular C is property that effective epis can be "pulled back" along any morphism. This is satisfied e.g. by categories that have pullbacks that preserve effective epimorphisms (like Profinite and CompHaus), and categories where every object is projective (like Stonean).

class CategoryTheory.HasPullbacksOfInclusions (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• has_pullback : ∀ {X Z : C} {α : Type w} (f : X ⟶ Z) {Y : α → C} (i : (a : α) → Y a ⟶ Z) [inst : Fintype α] [inst : CategoryTheory.Limits.HasCoproduct Y] [inst : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc i)] (a : α), CategoryTheory.Limits.HasPullback f (i a)

  For any morphism f : X ⟶ Z, where Z is the coproduct of i : (a : α) → Y a ⟶ Z with α finite, the pullback of f and i a exists for every a : α.

Describes the property of having pullbacks of morphsims into a finite coproduct, where one of the morphisms is an inclusion map into the coproduct (up to isomorphism).

instance CategoryTheory.instHasPullback (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasPullbacksOfInclusions C] {X : C} {Z : C} {α : Type w} (f : X ⟶ Z) {Y : α → C} (i : (a : α) → Y a ⟶ Z) [Fintype α] [CategoryTheory.Limits.HasCoproduct Y] [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc i)] (a : α) : CategoryTheory.Limits.HasPullback f (i a)

instance CategoryTheory.instHasPullbacksOfInclusions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.HasPullbacksOfInclusions C

If C has pullbacks then it has the pullbacks relevant to HasPullbacksOfInclusions.

class CategoryTheory.Extensive (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.Limits.HasFiniteCoproducts , CategoryTheory.HasPullbacksOfInclusions : Prop

• out : ∀ (n : ℕ), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C
• has_pullback : ∀ {X Z : C} {α : Type} (f : X ⟶ Z) {Y : α → C} (i : (a : α) → Y a ⟶ Z) [inst : Fintype α] [inst : CategoryTheory.Limits.HasCoproduct Y] [inst : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc i)] (a : α), CategoryTheory.Limits.HasPullback f (i a)
• sigma_desc_iso : ∀ {α : Type} [inst : Fintype α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (x : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)), CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun x_1 => CategoryTheory.Limits.pullback.fst)

  Pulling back an isomorphism from a coproduct yields an isomorphism.

A category is extensive if it has all finite coproducts and those coproducts are preserved by pullbacks (we only require the relevant pullbacks to exist, via HasPullbacksOfInclusions).

TODO: relate this to the class FinitaryExtensive

def CategoryTheory.regularCoverage (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preregular C] : CategoryTheory.Coverage C

The regular coverage on a regular category C.

def CategoryTheory.extensiveCoverage (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Extensive C] : CategoryTheory.Coverage C

The extensive coverage on an extensive category C