Documentation

Mathlib.CategoryTheory.EffectiveEpi.Basic

Effective epimorphisms #

We define the notion of effective epimorphism and effective epimorphic family of morphisms.

A morphism is an effective epi if it is a joint coequalizer of all pairs of morphisms which it coequalizes.

A family of morphisms with fixed target is effective epimorphic if it is initial among families of morphisms with its sources and a general fixed target, coequalizing every pair of morphisms it coequalizes (here, the pair of morphisms coequalized can have different targets among the sources of the 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 are equivalent, see the file CategoryTheory/EffectiveEpi/RegularEpi.lean See nlab: Effective Epimorphism and Stacks 00WP for the standard definitions. Note that our notion of EffectiveEpi is often called "strict epi" in the literature.

References #

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

    ...factorizing e through f...

    theorem CategoryTheory.EffectiveEpiStruct.uniq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {f : Y X} (self : CategoryTheory.EffectiveEpiStruct f) {W : C} (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) (m : X W) :
    CategoryTheory.CategoryStruct.comp f m = em = self.desc e

    ...and as such, unique.

    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

      f is an effective epimorphism if there exists an EffectiveEpiStruct for f.

      Some chosen EffectiveEpiStruct associated to an effective epi.

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

        Equations
        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
            theorem CategoryTheory.EffectiveEpiFamilyStruct.fac {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} {X : αC} {π : (a : α) → X a B} (self : CategoryTheory.EffectiveEpiFamilyStruct X π) {W : C} (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) (self.desc e ) = e a

            ...factorizing the components of e through the components of π...

            theorem CategoryTheory.EffectiveEpiFamilyStruct.uniq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} {X : αC} {π : (a : α) → X a B} (self : CategoryTheory.EffectiveEpiFamilyStruct X π) {W : C} (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) :
            (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a)m = self.desc e

            ...and as such, unique.

            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 π a : X a ⟶ B indexed by α is effective epimorphic provided that the π a exhibit B as a colimit of the diagram of all "relations" R → X a₁, R ⟶ X a₂ for all a₁ a₂ : α.

            Instances
              theorem CategoryTheory.EffectiveEpiFamily.effectiveEpiFamily {C : Type u_1} :
              ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {B : C} {α : Type u_2} {X : αC} {π : (a : α) → X a B} [self : CategoryTheory.EffectiveEpiFamily X π], Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)

              π is an effective epimorphic family if there exists an EffectiveEpiFamilyStruct for π

              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.

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

                Equations
                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 : α) :
                  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₂

                  An EffectiveEpiFamily consisting of a single EffectiveEpi

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    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 : Unit) => X) fun (x : Unit) => match x with | PUnit.unit => f
                    Equations
                    • =

                    A single element EffectiveEpiFamily consists of an EffectiveEpi

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • =

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Any isomorphism is an effective epi.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def CategoryTheory.EffectiveEpiFamilyStruct.reindex {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {B : C} {α : Type u_2} {α' : Type u_3} (X : αC) (π : (a : α) → X a B) (e : α' α) (P : CategoryTheory.EffectiveEpiFamilyStruct (fun (a : α') => X (e a)) fun (a : α') => π (e a)) :

                          Reindex the indexing type of an effective epi family struct.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem CategoryTheory.EffectiveEpiFamily.reindex {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {B : C} {α : Type u_2} {α' : Type u_3} (X : αC) (π : (a : α) → X a B) (e : α' α) (h : CategoryTheory.EffectiveEpiFamily (fun (a : α') => X (e a)) fun (a : α') => π (e a)) :

                            Reindex the indexing type of an effective epi family.