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 : C} {Y : C} (f : X Y) (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

    Composition of ι with f and with g agree

    @[simp]

    leftRetraction splits ι

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

    f composed with rightRetraction is leftRetraction composed with ι

    @[simp]
    theorem CategoryTheory.IsSplitEqualizer.bottom_rightRetraction_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {W : C} {ι : W X} (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : X Z) :
    @[simp]
    theorem CategoryTheory.IsSplitEqualizer.ι_leftRetraction_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {W : C} {ι : W X} (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : W Z) :
    @[simp]
    theorem CategoryTheory.IsSplitEqualizer.map_leftRetraction {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} {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 : C} {Y : C} {f : X Y} {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
    def CategoryTheory.IsSplitEqualizer.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} {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.asFork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {W : C} {h : W X} (t : CategoryTheory.IsSplitEqualizer f g h) :
      t.asFork.pt = W
      def CategoryTheory.IsSplitEqualizer.asFork {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {W : C} {h : W X} (t : CategoryTheory.IsSplitEqualizer f g h) :

      A split equalizer clearly induces a fork.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.IsSplitEqualizer.asFork_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {W : C} {h : W X} (t : CategoryTheory.IsSplitEqualizer f g h) :
        t.asFork = h
        def CategoryTheory.IsSplitEqualizer.isEqualizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {W : C} {h : W X} (t : CategoryTheory.IsSplitEqualizer f g 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
          class CategoryTheory.HasSplitEqualizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) (g : X Y) :

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

            There is some split equalizer

            @[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.

                  Equations
                  • =
                  @[instance 1]

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

                  Equations
                  • =