Split Equalizers

We define what it means for a triple of morphisms f g : X ⟶ Y, ι : W ⟶ X to be a split equalizer: there is a retraction r of ι and a retraction t of g, which additionally satisfy t ≫ f = r ≫ ι.

In addition, we show that every split equalizer is an equalizer (CategoryTheory.IsSplitEqualizer.isEqualizer) and absolute (CategoryTheory.IsSplitEqualizer.map)

A pair f g : X ⟶ Y has a split equalizer if there is a W and ι : W ⟶ X making f,g,ι a split equalizer. A pair f g : X ⟶ Y has a G-split equalizer if G f, G g has a split equalizer.

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

This file was adapted from Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean. Please try to keep them in sync.

structure CategoryTheory.IsSplitEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {W : C} (ι : W ⟶ X) : Type v

A split equalizer diagram consists of morphisms

      ι   f
    W → X ⇉ Y
          g

satisfying ι ≫ f = ι ≫ g together with morphisms

      r   t
    W ← X ← Y

satisfying ι ≫ r = 𝟙 W, g ≫ t = 𝟙 X and f ≫ t = r ≫ ι.

The name "equalizer" is appropriate, since any split equalizer is an equalizer, see CategoryTheory.IsSplitEqualizer.isEqualizer. Split equalizers are also absolute, since a functor preserves all the structure above.

• leftRetraction : X ⟶ W

  A map from X to the equalizer

• rightRetraction : 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

• ι_leftRetraction : CategoryStruct.comp ι self.leftRetraction = CategoryStruct.id W

  leftRetraction splits ι

• bottom_rightRetraction : CategoryStruct.comp g self.rightRetraction = CategoryStruct.id X

  rightRetraction splits g

• top_rightRetraction : CategoryStruct.comp f self.rightRetraction = CategoryStruct.comp self.leftRetraction ι

  f composed with rightRetraction is leftRetraction composed with ι

@[implicit_reducible]

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

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

Composition of ι with f and with g agree

@[simp]

theorem CategoryTheory.IsSplitEqualizer.ι_leftRetraction_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (self : IsSplitEqualizer f g ι) {Z : C} (h : W ⟶ Z) : CategoryStruct.comp ι (CategoryStruct.comp self.leftRetraction h) = h

leftRetraction splits ι

@[simp]

theorem CategoryTheory.IsSplitEqualizer.top_rightRetraction_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (self : IsSplitEqualizer f g ι) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp self.rightRetraction h) = CategoryStruct.comp self.leftRetraction (CategoryStruct.comp ι h)

f composed with rightRetraction is leftRetraction composed with ι

@[simp]

theorem CategoryTheory.IsSplitEqualizer.bottom_rightRetraction_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (self : IsSplitEqualizer f g ι) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp g (CategoryStruct.comp self.rightRetraction h) = h

rightRetraction splits g

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

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

@[simp]

theorem CategoryTheory.IsSplitEqualizer.map_rightRetraction {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (q : IsSplitEqualizer f g ι) (F : Functor C D) : (q.map F).rightRetraction = F.map q.rightRetraction

@[simp]

theorem CategoryTheory.IsSplitEqualizer.map_leftRetraction {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (q : IsSplitEqualizer f g ι) (F : Functor C D) : (q.map F).leftRetraction = F.map q.leftRetraction

def CategoryTheory.IsSplitEqualizer.asFork {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : Limits.Fork f g

A split equalizer clearly induces a fork.

@[simp]

theorem CategoryTheory.IsSplitEqualizer.asFork_pt {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : t.asFork.pt = W

@[simp]

theorem CategoryTheory.IsSplitEqualizer.asFork_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : t.asFork.ι = h

def CategoryTheory.IsSplitEqualizer.isEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : Limits.IsLimit t.asFork

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

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

The pair f,g is a cosplit pair if there is an h : W ⟶ X so that f, g, h forms a split equalizer in C.

• splittable : ∃ (W : C) (h : W ⟶ X), Nonempty (IsSplitEqualizer f g h)

  There is some split equalizer

@[reducible, inline]

abbrev CategoryTheory.Functor.IsCosplitPair {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-cosplit pair if there is an h : W ⟶ G X so that G f, G g, h forms a split equalizer in D.

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

Get the equalizer object from the typeclass IsCosplitPair.

noncomputable def CategoryTheory.HasSplitEqualizer.equalizerι {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitEqualizer f g] : equalizerOfSplit f g ⟶ X

Get the equalizer morphism from the typeclass IsCosplitPair.

noncomputable def CategoryTheory.HasSplitEqualizer.isSplitEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitEqualizer f g] : IsSplitEqualizer f g (equalizerι f g)

The equalizer morphism equalizerι gives a split equalizer on f,g.

instance CategoryTheory.map_is_cosplit_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) [HasSplitEqualizer f g] : HasSplitEqualizer (G.map f) (G.map g)

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

@[instance 1]

instance CategoryTheory.Limits.hasEqualizer_of_hasSplitEqualizer {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasSplitEqualizer f g] : HasEqualizer f g

If a pair has a split equalizer, it has an equalizer.