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

    Composition of π with f and with g agree

    @[simp]

    rightSection splits π

    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.leftSection_top {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 π) :

    leftSection composed with f is pi composed with rightSection

    @[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.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.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) :
    (q.map F).rightSection = F.map q.rightSection
    @[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) :
    (q.map F).leftSection = F.map q.leftSection
    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.

    Equations
    • q.map F = { rightSection := F.map q.rightSection, leftSection := F.map q.leftSection, condition := , rightSection_π := , leftSection_bottom := , leftSection_top := }
    Instances For
      @[simp]
      theorem CategoryTheory.IsSplitCoequalizer.asCofork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {h : Y Z} (t : CategoryTheory.IsSplitCoequalizer f g h) :
      t.asCofork.pt = Z

      A split coequalizer clearly induces a cofork.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.IsSplitCoequalizer.asCofork_π {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {Z : C} {h : Y Z} (t : CategoryTheory.IsSplitCoequalizer f g h) :
        t.asCofork = h

        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.

        Equations
        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
            theorem CategoryTheory.HasSplitCoequalizer.splittable {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} [self : CategoryTheory.HasSplitCoequalizer f g] :
            ∃ (Z : C) (h : Y Z), Nonempty (CategoryTheory.IsSplitCoequalizer f g h)

            There is some split coequalizer

            @[reducible, inline]

            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.

            Equations
            Instances For

              Get the coequalizer object from the typeclass IsSplitPair.

              Equations
              Instances For

                Get the coequalizer morphism from the typeclass IsSplitPair.

                Equations
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    • =
                    @[instance 1]

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

                    Equations
                    • =