# 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: #

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 : ] (X₁ : αC) (π₁ : (a : α) → X₁ a B₁), ∃ (β : Type) (_ : ) (X₂ : βC) (π₂ : (b : β) → X₂ b B₂), ∃ (i : βα) (ι : (b : β) → X₂ b X₁ (i b)), ∀ (b : β), CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) =

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 π₁.

Instances
theorem CategoryTheory.Precoherent.pullback {C : Type u_1} [] [self : ] {B₁ : C} {B₂ : C} (f : B₂ B₁) (α : Type) [] (X₁ : αC) (π₁ : (a : α) → X₁ a B₁) :
∃ (β : Type) (_ : ) (X₂ : βC) (π₂ : (b : β) → X₂ b B₂), ∃ (i : βα) (ι : (b : β) → X₂ b X₁ (i b)), ∀ (b : β), CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) =

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 π₁.

The coherent coverage on a precoherent category C.

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

The coherent Grothendieck topology on a precoherent category C.

Equations
Instances For
class CategoryTheory.Preregular (C : Type u_1) [] :

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 : ], ∃ (W : C) (h : W X) (_ : ) (i : W Z),

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

Instances
theorem CategoryTheory.Preregular.exists_fac {C : Type u_1} [] [self : ] {X : C} {Y : C} {Z : C} (f : X Y) (g : Z Y) :
∃ (W : C) (h : W X) (_ : ) (i : W Z),

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 regular coverage on a regular category C.

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

The regular Grothendieck topology on a preregular category C.

Equations
Instances For

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.
Instances For

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

Equations
Instances For