The Coherent, Regular and Extensive Grothendieck Topologies

This file defines three related Grothendieck topologies on a category C.

The first one is called the coherent topology. For that to exist, the category C must satisfy a condition called Precoherent C, which is essentially the minimal requirement for the coherent coverage to exist. It means that finite effective epimorphic families can be "pulled back". Given such a category, the coherent coverage is coherentCoverage C and the corresponding Grothendieck topology is coherentTopology C. The covering sieves of this coverage are generated by presieves consisting of finite effective epimorphic families.

The second one is called the regular topology 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 regular coverage is regularCoverage C and the corresponding Grothendieck topology is regularTopology C. The covering sieves of this coverage are generated by presieves consisting of a single effective epimorphism.

The third one is called the extensive coverage and for that to exist, the category C must satisfy a condition called FinitaryPreExtensive C. This means C has finite coproducts and that those are preserved by pullbacks. This condition is weaker than FinitaryExtensive, where in addition finite coproducts are disjoint. The extensive coverage is extensiveCoverage C and the corresponding Grothendieck topology is extensiveTopology C. 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.

References:

• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1, Example 2.1.12.
• nLab, Coherent Coverage

class CategoryTheory.Precoherent (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Prop

The condition Precoherent C is essentially the minimal condition required to define the coherent coverage on C.

• pullback : ∀ {B₁ B₂ : C} (f : B₂ ⟶ B₁) (α : Type) [inst : Fintype α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁), CategoryTheory.EffectiveEpiFamily X₁ π₁ → ∃ (β : Type) (x : Fintype β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂), CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f

  Given an effective epi family π₁ over B₁ and a morphism f : B₂ ⟶ B₁, there exists an effective epi family π₂ over B₂, such that π₂ factors through π₁.

def CategoryTheory.coherentCoverage (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] : CategoryTheory.Coverage C

The coherent coverage on a precoherent category C.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.coherentTopology (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] : CategoryTheory.GrothendieckTopology C

The coherent Grothendieck topology on a precoherent category C.

Equations

• CategoryTheory.coherentTopology C = CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.coherentCoverage C)

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

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).

• exists_fac : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [inst : CategoryTheory.EffectiveEpi g], ∃ (W : C) (h : W ⟶ X) (_ : CategoryTheory.EffectiveEpi h) (i : W ⟶ Z), 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
  

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

The regular coverage on a regular category C.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.regularTopology (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preregular C] : CategoryTheory.GrothendieckTopology C

The regular Grothendieck topology on a preregular category C.

Equations

• CategoryTheory.regularTopology C = CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.regularCoverage C)

def CategoryTheory.extensiveCoverage (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.FinitaryPreExtensive C] : CategoryTheory.Coverage C

The extensive coverage on an extensive category C

TODO: use general colimit API instead of IsIso (Sigma.desc π)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.extensiveTopology (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.FinitaryPreExtensive C] : CategoryTheory.GrothendieckTopology C

The extensive Grothendieck topology on a finitary pre-extensive category C.

Equations

• CategoryTheory.extensiveTopology C = CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.extensiveCoverage C)