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

- 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`

).

## Instances

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

## Instances

If `C`

has pullbacks then it has the pullbacks relevant to `HasPullbacksOfInclusions`

.

- 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`

## Instances

The regular coverage on a regular category `C`

.

## Instances For

The extensive coverage on an extensive category `C`