mathlib documentation

category_theory.limits.shapes.split_coequalizer

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 (category_theory.is_split_coequalizer.is_coequalizer) and absolute (category_theory.is_split_coequalizer.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.

TODO #

Dualise to split equalizers.

structure category_theory.is_split_coequalizer {C : Type u} [category_theory.category 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 category_theory.is_split_coequalizer.is_coequalizer. Split coequalizers are also absolute, since a functor preserves all the structure above.

theorem category_theory.is_split_coequalizer.condition_assoc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (self : category_theory.is_split_coequalizer f g «π») {X' : C} (f' : Z X') :
f «π» f' = g «π» f'
@[simp]
theorem category_theory.is_split_coequalizer.right_section_π_assoc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (self : category_theory.is_split_coequalizer f g «π») {X' : C} (f' : Z X') :
self.right_section «π» f' = f'
@[simp]
theorem category_theory.is_split_coequalizer.left_section_top_assoc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (self : category_theory.is_split_coequalizer f g «π») {X' : C} (f' : Y X') :
self.left_section f f' = «π» self.right_section f'
@[simp]
theorem category_theory.is_split_coequalizer.left_section_bottom_assoc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (self : category_theory.is_split_coequalizer f g «π») {X' : C} (f' : Y X') :
self.left_section g f' = f'
def category_theory.is_split_coequalizer.map {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (q : category_theory.is_split_coequalizer f g «π») (F : C D) :

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

Equations
@[simp]
theorem category_theory.is_split_coequalizer.map_left_section {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (q : category_theory.is_split_coequalizer f g «π») (F : C D) :
@[simp]
theorem category_theory.is_split_coequalizer.map_right_section {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} {f g : X Y} {Z : C} {π : Y Z} (q : category_theory.is_split_coequalizer f g «π») (F : C D) :

A split coequalizer clearly induces a cofork.

Equations
@[simp]
theorem category_theory.is_split_coequalizer.as_cofork_ι_app {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {Z : C} {h : Y Z} (t : category_theory.is_split_coequalizer f g h) (X_1 : category_theory.limits.walking_parallel_pair) :
t.as_cofork.ι.app X_1 = category_theory.limits.walking_parallel_pair.rec (f h) h X_1
@[simp]
theorem category_theory.is_split_coequalizer.as_cofork_X {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {Z : C} {h : Y Z} (t : category_theory.is_split_coequalizer f g h) :

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
@[class]
structure category_theory.has_split_coequalizer {C : Type u} [category_theory.category C] {X Y : C} (f g : X Y) :
Prop

The pair f,g is a split pair if there is a h : Y ⟶ Z so that f, g, h forms a split coequalizer in C.

Instances
def category_theory.functor.is_split_pair {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C D) {X Y : C} (f g : X Y) :
Prop

The pair f,g is a G-split pair if there is a h : G Y ⟶ Z so that G f, G g, h forms a split coequalizer in D.

Get the coequalizer object from the typeclass is_split_pair.

Equations
@[instance]

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

@[instance]

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