Documentation

Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Effective epimorphisms #

We define the notion of effective epimorphic (pre)sieves, morphisms and family of morphisms and provide some API for relating the three notions.

More precisely, if f is a morphism, then f is an effective epi if and only if the sieve it generates is effective epimorphic; see CategoryTheory.Sieve.effectiveEpimorphic_singleton. The analogous statement for a family of morphisms is in the theorem CategoryTheory.Sieve.effectiveEpimorphic_family.

We have defined the notion of effective epi for morphisms and families of morphisms in such a way that avoids requiring the existence of pullbacks. However, if the relevant pullbacks exist then these definitions should be equivalent (project: formalize this!). See nlab: Effective Epimorphism and Stacks 00WP for the standard definitions.

References #

source
def CategoryTheory.Sieve.EffectiveEpimorphic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} (S : CategoryTheory.Sieve X) :
Prop

A sieve is effective epimorphic if the associated cocone is a colimit cocone.

Instances For
    source
    @[inline, reducible]
    abbrev CategoryTheory.Presieve.EffectiveEpimorphic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} (S : CategoryTheory.Presieve X) :
    Prop

    A presieve is effective epimorphic if the cocone associated to the sieve it generates is a colimit cocone.

    Instances For
      source
      def CategoryTheory.Sieve.generateSingleton {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) :
      CategoryTheory.Sieve X

      The sieve of morphisms which factor through a given morphism f. This is equal to Sieve.generate (Presieve.singleton f), but has more convenient definitional properties.

      Instances For
        source
        theorem CategoryTheory.Sieve.generateSingleton_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) :
        CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = CategoryTheory.Sieve.generateSingleton f
        source
        structure CategoryTheory.EffectiveEpiStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) :
        Type (max u_1 u_2)

        This structure encodes the data required for a morphism to be an effective epimorphism.

        Instances For
          source
          class CategoryTheory.EffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) :
          Prop

          A morphism f : Y ⟶ X is an effective epimorphism provided that f exhibits X as a colimit of the diagram of all "relations" R ⇉ Y. If f has a kernel pair, then this is equivalent to showing that the corresponding cofork is a colimit.

          Instances
            source
            noncomputable def CategoryTheory.EffectiveEpi.getStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] :
            CategoryTheory.EffectiveEpiStruct f

            Some chosen EffectiveEpiStruct associated to an effective epi.

            Instances For
              source
              noncomputable def CategoryTheory.EffectiveEpi.desc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) :
              X ⟶ W

              Descend along an effective epi.

              Instances For
                source
                @[simp]
                theorem CategoryTheory.EffectiveEpi.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) {Z : C} (h : W ⟶ Z) :
                CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.EffectiveEpi.desc f e fun {Z} => h Z) h) = CategoryTheory.CategoryStruct.comp e h
                source
                @[simp]
                theorem CategoryTheory.EffectiveEpi.fac {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) :
                CategoryTheory.CategoryStruct.comp f (CategoryTheory.EffectiveEpi.desc f e fun {Z} => h Z) = e
                source
                theorem CategoryTheory.EffectiveEpi.uniq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {W : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) (m : X ⟶ W) (hm : CategoryTheory.CategoryStruct.comp f m = e) :
                m = CategoryTheory.EffectiveEpi.desc f e fun {Z} => h Z
                source
                instance CategoryTheory.epiOfEffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f] :
                CategoryTheory.Epi f
                source
                def CategoryTheory.isColimitOfEffectiveEpiStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) (Hf : CategoryTheory.EffectiveEpiStruct f) :
                CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateSingleton f).arrows)

                Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

                Instances For
                  source
                  noncomputable def CategoryTheory.effectiveEpiStructOfIsColimit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) (Hf : CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateSingleton f).arrows)) :
                  CategoryTheory.EffectiveEpiStruct f

                  Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

                  Instances For
                    source
                    theorem CategoryTheory.Sieve.effectiveEpimorphic_singleton {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y ⟶ X) :
                    CategoryTheory.Presieve.EffectiveEpimorphic (CategoryTheory.Presieve.singleton f) ↔ CategoryTheory.EffectiveEpi f
                    source
                    def CategoryTheory.Sieve.generateFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) :
                    CategoryTheory.Sieve B

                    The sieve of morphisms which factor through a morphism in a given family. This is equal to Sieve.generate (Presieve.ofArrows X π), but has more convenient definitional properties.

                    Instances For
                      source
                      theorem CategoryTheory.Sieve.generateFamily_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) :
                      CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows X π) = CategoryTheory.Sieve.generateFamily X π
                      source
                      structure CategoryTheory.EffectiveEpiFamilyStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) :
                      Type (max (max u_1 u_2) u_3)

                      This structure encodes the data required for a family of morphisms to be effective epimorphic.

                      Instances For
                        source
                        class CategoryTheory.EffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) :
                        Prop

                        A family of morphisms f a : X a ⟶ B indexed by α is effective epimorphic provided that the f a exhibit B as a colimit of the diagram of all "relations" R → X a₁, R ⟶ X a₂ for all a₁ a₂ : α.

                        Instances
                          source
                          noncomputable def CategoryTheory.EffectiveEpiFamily.getStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] :
                          CategoryTheory.EffectiveEpiFamilyStruct X π

                          Some chosen EffectiveEpiFamilyStruct associated to an effective epi family.

                          Instances For
                            source
                            noncomputable def CategoryTheory.EffectiveEpiFamily.desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) :
                            B ⟶ W

                            Descend along an effective epi family.

                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.EffectiveEpiFamily.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (a : α) {Z : C} (h : W ⟶ Z) :
                              CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.EffectiveEpiFamily.desc X π e fun {Z} => h Z) h) = CategoryTheory.CategoryStruct.comp (e a) h
                              source
                              @[simp]
                              theorem CategoryTheory.EffectiveEpiFamily.fac {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (a : α) :
                              CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.EffectiveEpiFamily.desc X π e fun {Z} => h Z) = e a
                              source
                              def CategoryTheory.effectiveEpiFamilyStructId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {α : Unit → C} :
                              CategoryTheory.EffectiveEpiFamilyStruct α fun x => CategoryTheory.CategoryStruct.id (α ())

                              The effective epi family structure on the identity

                              Instances For
                                source
                                instance CategoryTheory.instEffectiveEpiFamilyUnitIdToCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} :
                                CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => CategoryTheory.CategoryStruct.id X
                                source
                                theorem CategoryTheory.EffectiveEpiFamily.uniq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (m : B ⟶ W) (hm : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) :
                                m = CategoryTheory.EffectiveEpiFamily.desc X π e fun {Z} => h Z
                                source
                                theorem CategoryTheory.EffectiveEpiFamily.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {W : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (m₁ : B ⟶ W) (m₂ : B ⟶ W) (h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m₁ = CategoryTheory.CategoryStruct.comp (π a) m₂) :
                                m₁ = m₂
                                source
                                instance CategoryTheory.epiCoproductDescOfEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] [CategoryTheory.Limits.HasCoproduct X] :
                                CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π)
                                source
                                def CategoryTheory.isColimitOfEffectiveEpiFamilyStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (H : CategoryTheory.EffectiveEpiFamilyStruct X π) :
                                CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateFamily X π).arrows)

                                Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.

                                Instances For
                                  source
                                  noncomputable def CategoryTheory.effectiveEpiFamilyStructOfIsColimit {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (H : CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateFamily X π).arrows)) :
                                  CategoryTheory.EffectiveEpiFamilyStruct X π

                                  Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.

                                  Instances For
                                    source
                                    theorem CategoryTheory.Sieve.effectiveEpimorphic_family {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) :
                                    CategoryTheory.Presieve.EffectiveEpimorphic (CategoryTheory.Presieve.ofArrows X π) ↔ CategoryTheory.EffectiveEpiFamily X π
                                    source
                                    noncomputable def CategoryTheory.EffectiveEpiFamily_descStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π] :
                                    CategoryTheory.EffectiveEpiStruct (CategoryTheory.Limits.Sigma.desc π)

                                    Given an EffectiveEpiFamily X π such that the coproduct of X exists, Sigma.desc π is an EffectiveEpi.

                                    Instances For
                                      source
                                      instance CategoryTheory.instEffectiveEpiSigmaObjDesc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π] :
                                      CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)
                                      source
                                      noncomputable def CategoryTheory.EffectiveEpi_familyStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpi f] :
                                      CategoryTheory.EffectiveEpiFamilyStruct (fun x => X) fun x => match x with | PUnit.unit => f

                                      An EffectiveEpiFamily consisting of a single EffectiveEpi

                                      Instances For
                                        source
                                        instance CategoryTheory.instEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpi f] :
                                        CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => match x with | PUnit.unit => f
                                        source
                                        noncomputable def CategoryTheory.EffectiveEpiFamilyStruct_of_isIso_desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)] :
                                        CategoryTheory.EffectiveEpiFamilyStruct X π

                                        A family of morphisms with the same target inducing an isomorphism from the coproduct to the target is an EffectiveEpiFamily.

                                        Instances For
                                          source
                                          instance CategoryTheory.instEffectiveEpiFamily_1 {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)] :
                                          CategoryTheory.EffectiveEpiFamily X π