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 #

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

Instances For
    @[inline, reducible]

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

    Instances For

      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
        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
          class CategoryTheory.EffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : Y X) :

          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

            Some chosen EffectiveEpiStruct associated to an effective epi.

            Instances For
              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₂ fCategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) :
              X W

              Descend along an effective epi.

              Instances For

                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

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

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

                        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
                          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 π] :

                          Some chosen EffectiveEpiFamilyStruct associated to an effective epi family.

                          Instances For
                            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
                              @[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) :
                              @[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 : α) :

                              The effective epi family structure on the identity

                              Instances For
                                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) :
                                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₂

                                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

                                  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

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

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

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

                                        Instances For