mathlib3 documentation

category_theory.limits.shapes.split_coequalizer

Split coequalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

right_section : Z ⟶ Y
left_section : Y ⟶ X
condition : f ≫ π = g ≫ π
right_section_π : self.right_section ≫ π = 𝟙 Z
left_section_bottom : self.left_section ≫ g = 𝟙 Y
left_section_top : self.left_section ≫ f = π ≫ self.right_section

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.

Instances for category_theory.is_split_coequalizer

category_theory.is_split_coequalizer.has_sizeof_inst
category_theory.is_split_coequalizer.inhabited

@[protected, instance]

def category_theory.is_split_coequalizer.inhabited {C : Type u} [category_theory.category C] {X : C} :

inhabited (category_theory.is_split_coequalizer (𝟙 X) (𝟙 X) (𝟙 X))

Equations

category_theory.is_split_coequalizer.inhabited = {default := {right_section := 𝟙 X, left_section := 𝟙 X, condition := _, right_section_π := _, left_section_bottom := _, left_section_top := _}}

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

category_theory.is_split_coequalizer (F.map f) (F.map g) (F.map π)

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

Equations

q.map F = {right_section := F.map q.right_section, left_section := F.map q.left_section, condition := _, right_section_π := _, left_section_bottom := _, left_section_top := _}

@[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) :

(q.map F).left_section = F.map q.left_section

@[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) :

(q.map F).right_section = F.map q.right_section

def category_theory.is_split_coequalizer.as_cofork {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) :

category_theory.limits.cofork f g

A split coequalizer clearly induces a cofork.

Equations

t.as_cofork = category_theory.limits.cofork.of_π h _

@[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) :

t.as_cofork.X = Z

@[simp]

theorem category_theory.is_split_coequalizer.as_cofork_π {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) :

t.as_cofork.π = h

def category_theory.is_split_coequalizer.is_coequalizer {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) :

category_theory.limits.is_colimit t.as_cofork

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

t.is_coequalizer = category_theory.limits.cofork.is_colimit.mk' t.as_cofork (λ (s : category_theory.limits.cofork f g), ⟨t.right_section ≫ s.π, _⟩)

@[class]

structure category_theory.has_split_coequalizer {C : Type u} [category_theory.category C] {X Y : C} (f g : X ⟶ Y) :

Prop

splittable : ∃ {Z : C} (h : Y ⟶ Z), nonempty (category_theory.is_split_coequalizer f g h)

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 of this typeclass

@[reducible]

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.

noncomputable def category_theory.has_split_coequalizer.coequalizer_of_split {C : Type u} [category_theory.category C] {X Y : C} (f g : X ⟶ Y) [category_theory.has_split_coequalizer f g] :

C

Get the coequalizer object from the typeclass is_split_pair.

Equations

category_theory.has_split_coequalizer.coequalizer_of_split f g = _.some

noncomputable def category_theory.has_split_coequalizer.coequalizer_π {C : Type u} [category_theory.category C] {X Y : C} (f g : X ⟶ Y) [category_theory.has_split_coequalizer f g] :

Y ⟶ category_theory.has_split_coequalizer.coequalizer_of_split f g

Get the coequalizer morphism from the typeclass is_split_pair.

Equations

category_theory.has_split_coequalizer.coequalizer_π f g = Exists.some _

noncomputable def category_theory.has_split_coequalizer.is_split_coequalizer {C : Type u} [category_theory.category C] {X Y : C} (f g : X ⟶ Y) [category_theory.has_split_coequalizer f g] :

category_theory.is_split_coequalizer f g (category_theory.has_split_coequalizer.coequalizer_π f g)

The coequalizer morphism coequalizer_ι gives a split coequalizer on f,g.

Equations

category_theory.has_split_coequalizer.is_split_coequalizer f g = classical.choice _

@[protected, instance]

def category_theory.map_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) [category_theory.has_split_coequalizer f g] :

category_theory.has_split_coequalizer (G.map f) (G.map g)

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

@[protected, instance]

def category_theory.limits.has_coequalizer_of_has_split_coequalizer {C : Type u} [category_theory.category C] {X Y : C} (f g : X ⟶ Y) [category_theory.has_split_coequalizer f g] :

category_theory.limits.has_coequalizer f g

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