Documentation

Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Split coequalizers #

We define what it means for a triple of morphisms f g : X ⟶ Y, π : Y ⟶ Z to be a split coequalizer: there is a section s of π and a section t of g, which additionally satisfy t ≫ f = π ≫ s.

In addition, we show that every split coequalizer is a coequalizer (CategoryTheory.IsSplitCoequalizer.isCoequalizer) and absolute (CategoryTheory.IsSplitCoequalizer.map)

A pair f g : X ⟶ Y has a split coequalizer if there is a Z and π : Y ⟶ Z making f,g,π a split coequalizer. A pair f g : X ⟶ Y has a G-split coequalizer if G f, G g has a split coequalizer.

These definitions and constructions are useful in particular for the monadicity theorems.

TODO #

Dualise to split equalizers.

structure CategoryTheory.IsSplitCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) (g : X Y) {Z : C} (π : Y Z) :

A split coequalizer diagram consists of morphisms

  f   π
X ⇉ Y → Z
  g

satisfying f ≫ π = g ≫ π together with morphisms

  t   s
X ← Y ← Z

satisfying s ≫ π = 𝟙 Z, t ≫ g = 𝟙 Y and t ≫ f = π ≫ s.

The name "coequalizer" is appropriate, since any split coequalizer is a coequalizer, see Category_theory.IsSplitCoequalizer.isCoequalizer. Split coequalizers are also absolute, since a functor preserves all the structure above.

Instances For
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.leftSection_bottom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {π : Y Z} (self : CategoryTheory.IsSplitCoequalizer f g π) {Z : C} (h : Y Z) :
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.rightSection_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {π : Y Z} (self : CategoryTheory.IsSplitCoequalizer f g π) {Z : C} (h : Z Z) :
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.map_leftSection {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {π : Y Z} (q : CategoryTheory.IsSplitCoequalizer f g π) (F : CategoryTheory.Functor C D) :
    (CategoryTheory.IsSplitCoequalizer.map q F).leftSection = F.map q.leftSection
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.map_rightSection {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {π : Y Z} (q : CategoryTheory.IsSplitCoequalizer f g π) (F : CategoryTheory.Functor C D) :
    (CategoryTheory.IsSplitCoequalizer.map q F).rightSection = F.map q.rightSection
    def CategoryTheory.IsSplitCoequalizer.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {π : Y Z} (q : CategoryTheory.IsSplitCoequalizer f g π) (F : CategoryTheory.Functor C D) :
    CategoryTheory.IsSplitCoequalizer (F.map f) (F.map g) (F.map π)

    Split coequalizers are absolute: they are preserved by any functor.

    Instances For

      A split coequalizer clearly induces a cofork.

      Instances For

        The cofork induced by a split coequalizer is a coequalizer, justifying the name. In some cases it is more convenient to show a given cofork is a coequalizer by showing it is split.

        Instances For
          class CategoryTheory.HasSplitCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) (g : X Y) :

          The pair f,g is a split pair if there is an h : Y ⟶ Z so that f, g, h forms a split coequalizer in C.

          Instances
            @[inline, reducible]

            The pair f,g is a G-split pair if there is an h : G Y ⟶ Z so that G f, G g, h forms a split coequalizer in D.

            Instances For

              Get the coequalizer object from the typeclass IsSplitPair.

              Instances For

                Get the coequalizer morphism from the typeclass IsSplitPair.

                Instances For

                  The coequalizer morphism coequalizeπ gives a split coequalizer on f,g.

                  Instances For

                    If f, g is split, then G f, G g is split.

                    If a pair has a split coequalizer, it has a coequalizer.