Documentation

Mathlib.CategoryTheory.Sites.Coherent.Basic

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.

Instances
    theorem CategoryTheory.Precoherent.pullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [self : CategoryTheory.Precoherent C] {B₁ : C} {B₂ : C} (f : B₂ B₁) (α : Type) [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 π₁.

    The coherent coverage on a precoherent category C.

    Equations
    • One or more equations did not get rendered due to their size.
    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).

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