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.

This file has been adapted to Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean. Please try to keep them in sync.

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

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 CategoryTheory.IsSplitCoequalizer.isCoequalizer. Split coequalizers are also absolute, since a functor preserves all the structure above.

• rightSection : Z ⟶ Y

  A map from the coequalizer to Y

• leftSection : Y ⟶ X

  A map in the opposite direction to f and g

• condition : CategoryStruct.comp f π = CategoryStruct.comp g π

  Composition of π with f and with g agree

• rightSection_π : CategoryStruct.comp self.rightSection π = CategoryStruct.id Z

  rightSection splits π

• leftSection_bottom : CategoryStruct.comp self.leftSection g = CategoryStruct.id Y

  leftSection splits g

• leftSection_top : CategoryStruct.comp self.leftSection f = CategoryStruct.comp π self.rightSection

  leftSection composed with f is pi composed with rightSection

@[implicit_reducible]

instance CategoryTheory.instInhabitedIsSplitCoequalizerId {C : Type u} [Category.{v, u} C] {X : C} : Inhabited (IsSplitCoequalizer (CategoryStruct.id X) (CategoryStruct.id X) (CategoryStruct.id X))

theorem CategoryTheory.IsSplitCoequalizer.condition_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (self : IsSplitCoequalizer f g π) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp f (CategoryStruct.comp π h) = CategoryStruct.comp g (CategoryStruct.comp π h)

Composition of π with f and with g agree

@[simp]

theorem CategoryTheory.IsSplitCoequalizer.leftSection_bottom_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (self : IsSplitCoequalizer f g π) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp self.leftSection (CategoryStruct.comp g h) = h

leftSection splits g

@[simp]

theorem CategoryTheory.IsSplitCoequalizer.leftSection_top_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (self : IsSplitCoequalizer f g π) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp self.leftSection (CategoryStruct.comp f h) = CategoryStruct.comp π (CategoryStruct.comp self.rightSection h)

leftSection composed with f is pi composed with rightSection

@[simp]

theorem CategoryTheory.IsSplitCoequalizer.rightSection_π_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (self : IsSplitCoequalizer f g π) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp self.rightSection (CategoryStruct.comp π h) = h

rightSection splits π

def CategoryTheory.IsSplitCoequalizer.map {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (q : IsSplitCoequalizer f g π) (F : Functor C D) : IsSplitCoequalizer (F.map f) (F.map g) (F.map π)

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

@[simp]

theorem CategoryTheory.IsSplitCoequalizer.map_rightSection {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (q : IsSplitCoequalizer f g π) (F : Functor C D) : (q.map F).rightSection = F.map q.rightSection

@[simp]

theorem CategoryTheory.IsSplitCoequalizer.map_leftSection {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (q : IsSplitCoequalizer f g π) (F : Functor C D) : (q.map F).leftSection = F.map q.leftSection

def CategoryTheory.IsSplitCoequalizer.asCofork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {h : Y ⟶ Z} (t : IsSplitCoequalizer f g h) : Limits.Cofork f g

A split coequalizer clearly induces a cofork.

@[simp]

theorem CategoryTheory.IsSplitCoequalizer.asCofork_pt {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {h : Y ⟶ Z} (t : IsSplitCoequalizer f g h) : t.asCofork.pt = Z

@[simp]

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

def CategoryTheory.IsSplitCoequalizer.isCoequalizer {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {h : Y ⟶ Z} (t : IsSplitCoequalizer f g h) : Limits.IsColimit t.asCofork

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.

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

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.

• splittable : ∃ (Z : C) (h : Y ⟶ Z), Nonempty (IsSplitCoequalizer f g h)

  There is some split coequalizer

@[reducible, inline]

abbrev CategoryTheory.Functor.IsSplitPair {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y : C} (f g : X ⟶ Y) : Prop

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.

noncomputable def CategoryTheory.HasSplitCoequalizer.coequalizerOfSplit {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitCoequalizer f g] : C

Get the coequalizer object from the typeclass IsSplitPair.

noncomputable def CategoryTheory.HasSplitCoequalizer.coequalizerπ {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitCoequalizer f g] : Y ⟶ coequalizerOfSplit f g

Get the coequalizer morphism from the typeclass IsSplitPair.

noncomputable def CategoryTheory.HasSplitCoequalizer.isSplitCoequalizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitCoequalizer f g] : IsSplitCoequalizer f g (coequalizerπ f g)

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

instance CategoryTheory.map_is_split_pair {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y : C} (f g : X ⟶ Y) [HasSplitCoequalizer f g] : HasSplitCoequalizer (G.map f) (G.map g)

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

@[instance 1]

instance CategoryTheory.Limits.hasCoequalizer_of_hasSplitCoequalizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitCoequalizer f g] : HasCoequalizer f g

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