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

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

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 : Finite α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁), CategoryTheory.EffectiveEpiFamily X₁ π₁ → ∃ (β : Type) (_ : Finite β) (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`π₁`

.

## Instances

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

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`

## Instances

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`

.