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.

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

source
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) :
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.

Instances For
    source
    theorem CategoryTheory.IsSplitCoequalizer.condition {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 π) :
    CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π

    Composition of π with f and with g agree

    source
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.rightSection_π {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 π) :
    CategoryTheory.CategoryStruct.comp self.rightSection π = CategoryTheory.CategoryStruct.id Z

    rightSection splits π

    source
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.leftSection_bottom {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 π) :
    CategoryTheory.CategoryStruct.comp self.leftSection g = CategoryTheory.CategoryStruct.id Y

    leftSection splits g

    source
    @[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 π) :
    CategoryTheory.CategoryStruct.comp self.leftSection f = CategoryTheory.CategoryStruct.comp π self.rightSection

    leftSection composed with f is pi composed with rightSection

    source
    instance CategoryTheory.instInhabitedIsSplitCoequalizerId {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} :
    Inhabited (CategoryTheory.IsSplitCoequalizer (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem CategoryTheory.IsSplitCoequalizer.condition_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) :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp π h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp π h)
    source
    @[simp]
    theorem CategoryTheory.IsSplitCoequalizer.leftSection_top_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) :
    CategoryTheory.CategoryStruct.comp self.leftSection (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp π (CategoryTheory.CategoryStruct.comp self.rightSection h)
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp self.rightSection (CategoryTheory.CategoryStruct.comp π h) = h
    source
    @[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) :
    CategoryTheory.CategoryStruct.comp self.leftSection (CategoryTheory.CategoryStruct.comp g h) = h
    source
    @[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
    source
    @[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
    source
    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
      source
      @[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
      source
      def 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) :
      CategoryTheory.Limits.Cofork f g

      A split coequalizer clearly induces a cofork.

      Equations
      Instances For
        source
        @[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
        source
        def CategoryTheory.IsSplitCoequalizer.isCoequalizer {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) :
        CategoryTheory.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.

        Equations
        Instances For
          source
          class CategoryTheory.HasSplitCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) (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.

          Instances
            source
            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

            source
            @[reducible, inline]
            abbrev CategoryTheory.Functor.IsSplitPair {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (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.

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

              Get the coequalizer object from the typeclass IsSplitPair.

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

                Get the coequalizer morphism from the typeclass IsSplitPair.

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

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

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

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

                    Equations
                    • ⋯ = ⋯
                    source
                    @[instance 1]
                    instance CategoryTheory.Limits.hasCoequalizer_of_hasSplitCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.HasSplitCoequalizer f g] :
                    CategoryTheory.Limits.HasCoequalizer f g

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

                    Equations
                    • ⋯ = ⋯