Documentation

Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

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. Please try to keep them in sync.

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

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 a equalizer, see CategoryTheory.IsSplitEqualizer.isEqualizer. Split equalizers are also absolute, since a functor preserves all the structure above.

Instances For
    @[simp]
    @[simp]
    theorem CategoryTheory.IsSplitEqualizer.ι_leftRetraction_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X Y} {W : C} {ι : W X} (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : W Z) :
    def CategoryTheory.IsSplitEqualizer.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f g : X Y} {W : C} {ι : W X} (q : CategoryTheory.IsSplitEqualizer f g ι) (F : CategoryTheory.Functor C D) :
    CategoryTheory.IsSplitEqualizer (F.map f) (F.map g) (F.map ι)

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

    Equations
    • q.map F = { leftRetraction := F.map q.leftRetraction, rightRetraction := F.map q.rightRetraction, condition := , ι_leftRetraction := , bottom_rightRetraction := , top_rightRetraction := }
    Instances For
      @[simp]
      theorem CategoryTheory.IsSplitEqualizer.map_leftRetraction {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f g : X Y} {W : C} {ι : W X} (q : CategoryTheory.IsSplitEqualizer f g ι) (F : CategoryTheory.Functor C D) :
      (q.map F).leftRetraction = F.map q.leftRetraction
      @[simp]
      theorem CategoryTheory.IsSplitEqualizer.map_rightRetraction {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} {f g : X Y} {W : C} {ι : W X} (q : CategoryTheory.IsSplitEqualizer f g ι) (F : CategoryTheory.Functor C D) :
      (q.map F).rightRetraction = F.map q.rightRetraction

      A split equalizer clearly induces a fork.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.IsSplitEqualizer.asFork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X Y} {W : C} {h : W X} (t : CategoryTheory.IsSplitEqualizer f g h) :
        t.asFork.pt = W
        @[simp]
        theorem CategoryTheory.IsSplitEqualizer.asFork_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X Y} {W : C} {h : W X} (t : CategoryTheory.IsSplitEqualizer f g h) :
        t.asFork = h

        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.

        Equations
        Instances For

          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.

          Instances
            @[reducible, inline]

            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.

            Equations
            Instances For

              Get the equalizer object from the typeclass IsCosplitPair.

              Equations
              Instances For

                Get the equalizer morphism from the typeclass IsCosplitPair.

                Equations
                Instances For

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

                  @[instance 1]

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