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

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

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

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

        Instances
          source
          theorem CategoryTheory.Preregular.exists_fac {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [self : CategoryTheory.Preregular C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [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
          source
          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.
          Instances For
            source
            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
            Instances For
              source
              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.
              Instances For
                source
                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
                Instances For