mathlib documentation

category_theory.limits.shapes.equalizers

Equalizers and coequalizers

This file defines (co)equalizers as special cases of (co)limits.

An equalizer is the categorical generalization of the subobject {a ∈ A | f(a) = g(a)} known from abelian groups or modules. It is a limit cone over the diagram formed by f and g.

A coequalizer is the dual concept.

Main definitions

Each of these has a dual.

Main statements

Implementation notes

As with the other special shapes in the limits library, all the definitions here are given as abbreviations of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

References

The type of objects for the diagram indexing a (co)equalizer.

@[instance]

Equations

parallel_pair f g is the diagram in C consisting of the two morphisms f and g with common domain and codomain.

Equations
def category_theory.limits.fork {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)(X Y)Type (max u v)

A fork on f and g is just a cone (parallel_pair f g).

def category_theory.limits.cofork {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)(X Y)Type (max u v)

A cofork on f and g is just a cocone (parallel_pair f g).

@[simp]
theorem category_theory.limits.fork.of_ι_X {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) :

@[simp]
theorem category_theory.limits.fork.of_ι_π_app {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) (X_1 : category_theory.limits.walking_parallel_pair) :
(category_theory.limits.fork.of_ι ι w).π.app X_1 = X_1.cases_on ι f)

def category_theory.limits.fork.of_ι {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (ι : P X) :

A fork on f g : X ⟶ Y is determined by the morphism ι : P ⟶ X satisfying ι ≫ f = ι ≫ g.

Equations
def category_theory.limits.cofork.of_π {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (π : Y P) :
f «π» = g «π»category_theory.limits.cofork f g

A cofork on f g : X ⟶ Y is determined by the morphism π : Y ⟶ P satisfying f ≫ π = g ≫ π.

Equations
@[simp]
theorem category_theory.limits.cofork.of_π_X {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f «π» = g «π») :

@[simp]
theorem category_theory.limits.cofork.of_π_ι_app {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f «π» = g «π») (X_1 : category_theory.limits.walking_parallel_pair) :
(category_theory.limits.cofork.of_π «π» w).ι.app X_1 = X_1.cases_on (f «π») «π»

A fork t on the parallel pair f g : X ⟶ Y consists of two morphisms t.π.app zero : t.X ⟶ X and t.π.app one : t.X ⟶ Y. Of these, only the first one is interesting, and we give it the shorter name fork.ι t.

A cofork t on the parallel_pair f g : X ⟶ Y consists of two morphisms t.ι.app zero : X ⟶ t.X and t.ι.app one : Y ⟶ t.X. Of these, only the second one is interesting, and we give it the shorter name cofork.π t.

@[simp]
theorem category_theory.limits.fork.ι_of_ι {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) :

@[simp]
theorem category_theory.limits.cofork.π_of_π {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f «π» = g «π») :

theorem category_theory.limits.fork.condition {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (t : category_theory.limits.fork f g) :
t.ι f = t.ι g

theorem category_theory.limits.fork.condition_assoc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (t : category_theory.limits.fork f g) {X' : C} (f' : Y X') :
t.ι f f' = t.ι g f'

theorem category_theory.limits.cofork.condition {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (t : category_theory.limits.cofork f g) :
f t.π = g t.π

theorem category_theory.limits.fork.equalizer_ext {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (s : category_theory.limits.fork f g) {W : C} {k l : W s.X} (h : k s.ι = l s.ι) (j : category_theory.limits.walking_parallel_pair) :
k s.π.app j = l s.π.app j

To check whether two maps are equalized by both maps of a fork, it suffices to check it for the first map

theorem category_theory.limits.cofork.coequalizer_ext {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (s : category_theory.limits.cofork f g) {W : C} {k l : s.X W} (h : s.π k = s.π l) (j : category_theory.limits.walking_parallel_pair) :
s.ι.app j k = s.ι.app j l

To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for the second map

theorem category_theory.limits.fork.is_limit.hom_ext {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s : category_theory.limits.fork f g} (hs : category_theory.limits.is_limit s) {W : C} {k l : W s.X} :
k s.ι = l s.ιk = l

theorem category_theory.limits.cofork.is_colimit.hom_ext {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s : category_theory.limits.cofork f g} (hs : category_theory.limits.is_colimit s) {W : C} {k l : s.X W} :
s.π k = s.π lk = l

def category_theory.limits.fork.is_limit.lift' {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s : category_theory.limits.fork f g} (hs : category_theory.limits.is_limit s) {W : C} (k : W X) :
k f = k g{l // l s.ι = k}

If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ s.X such that l ≫ fork.ι s = k.

Equations
def category_theory.limits.cofork.is_colimit.desc' {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s : category_theory.limits.cofork f g} (hs : category_theory.limits.is_colimit s) {W : C} (k : Y W) :
f k = g k{l // s.π l = k}

If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : s.X ⟶ W such that cofork.π s ≫ l = k.

Equations
def category_theory.limits.fork.is_limit.mk {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (t : category_theory.limits.fork f g) (lift : Π (s : category_theory.limits.fork f g), s.X t.X) :
(∀ (s : category_theory.limits.fork f g), lift s t.ι = s.ι)(∀ (s : category_theory.limits.fork f g) (m : s.X t.X), (∀ (j : category_theory.limits.walking_parallel_pair), m t.π.app j = s.π.app j)m = lift s)category_theory.limits.is_limit t

This is a slightly more convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content

Equations

This is another convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

Equations
def category_theory.limits.cofork.is_colimit.mk {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} (t : category_theory.limits.cofork f g) (desc : Π (s : category_theory.limits.cofork f g), t.X s.X) :
(∀ (s : category_theory.limits.cofork f g), t.π desc s = s.π)(∀ (s : category_theory.limits.cofork f g) (m : t.X s.X), (∀ (j : category_theory.limits.walking_parallel_pair), t.ι.app j m = s.ι.app j)m = desc s)category_theory.limits.is_colimit t

This is a slightly more convenient method to verify that a cofork is a colimit cocone. It only asks for a proof of facts that carry any mathematical content

Equations

This is another convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

Equations

This is a helper construction that can be useful when verifying that a category has all equalizers. Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right), and a fork on F.map left and F.map right, we get a cone on F.

If you're thinking about using this, have a look at has_equalizers_of_has_limit_parallel_pair, which you may find to be an easier way of achieving your goal.

Equations

This is a helper construction that can be useful when verifying that a category has all coequalizers. Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right), and a cofork on F.map left and F.map right, we get a cocone on F.

If you're thinking about using this, have a look at has_coequalizers_of_has_colimit_parallel_pair, which you may find to be an easier way of achieving your goal.

Equations

Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right) and a cone on F, we get a fork on F.map left and F.map right.

Equations

Given F : walking_parallel_pair ⥤ C, which is really the same as parallel_pair (F.map left) (F.map right) and a cocone on F, we get a cofork on F.map left and F.map right.

Equations
def category_theory.limits.fork.mk_hom {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s t : category_theory.limits.fork f g} (k : s.X t.X) :
k t.ι = s.ι(s t)

Helper function for constructing morphisms between equalizer forks.

Equations
@[simp]
theorem category_theory.limits.fork.mk_hom_hom {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s t : category_theory.limits.fork f g} (k : s.X t.X) (w : k t.ι = s.ι) :

def category_theory.limits.fork.ext {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s t : category_theory.limits.fork f g} (i : s.X t.X) :
i.hom t.ι = s.ι(s t)

To construct an isomorphism between forks, it suffices to give an isomorphism between the cone points and check that it commutes with the ι morphisms.

Equations
def category_theory.limits.cofork.mk_hom {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s t : category_theory.limits.cofork f g} (k : s.X t.X) :
s.π k = t.π(s t)

Helper function for constructing morphisms between coequalizer coforks.

Equations
@[simp]
theorem category_theory.limits.cofork.mk_hom_hom {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s t : category_theory.limits.cofork f g} (k : s.X t.X) (w : s.π k = t.π) :

def category_theory.limits.cofork.ext {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} {s t : category_theory.limits.cofork f g} (i : s.X t.X) :
s.π i.hom = t.π(s t)

To construct an isomorphism between coforks, it suffices to give an isomorphism between the cocone points and check that it commutes with the π morphisms.

Equations
def category_theory.limits.has_equalizer {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)(X Y) → Prop

has_equalizer f g represents a particular choice of limiting cone for the parallel pair of morphisms f and g.

Instances

If an equalizer of f and g exists, we can access an arbitrary choice of such by saying equalizer f g.

If an equalizer of f and g exists, we can access the inclusion equalizer f g ⟶ X by saying equalizer.ι f g.

An equalizer cone for a parallel pair f and g.

def category_theory.limits.equalizer.lift {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} [category_theory.limits.has_equalizer f g] {W : C} (k : W X) :

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g factors through the equalizer of f and g via equalizer.lift : W ⟶ equalizer f g.

@[simp]
theorem category_theory.limits.equalizer.lift_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} [category_theory.limits.has_equalizer f g] {W : C} (k : W X) (h : k f = k g) {X' : C} (f' : X X') :

def category_theory.limits.equalizer.lift' {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} [category_theory.limits.has_equalizer f g] {W : C} (k : W X) :
k f = k g{l // l category_theory.limits.equalizer.ι f g = k}

A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ equalizer f g satisfying l ≫ equalizer.ι f g = k.

Equations
@[ext]

Two maps into an equalizer are equal if they are are equal when composed with the equalizer map.

@[instance]

An equalizer morphism is a monomorphism

def category_theory.limits.id_fork {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} :

The identity determines a cone on the equalizer diagram of f and g if f = g.

Equations
def category_theory.limits.has_coequalizer {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)(X Y) → Prop

has_coequalizer f g represents a particular choice of colimiting cocone for the parallel pair of morphisms f and g.

Instances

If a coequalizer of f and g exists, we can access an arbitrary choice of such by saying coequalizer f g.

If a coequalizer of f and g exists, we can access the corresponding projection by saying coequalizer.π f g.

An arbitrary choice of coequalizer cocone for a parallel pair f and g.

def category_theory.limits.coequalizer.desc {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} [category_theory.limits.has_coequalizer f g] {W : C} (k : Y W) :

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k factors through the coequalizer of f and g via coequalizer.desc : coequalizer f g ⟶ W.

@[simp]

def category_theory.limits.coequalizer.desc' {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} [category_theory.limits.has_coequalizer f g] {W : C} (k : Y W) :
f k = g k{l // category_theory.limits.coequalizer.π f g l = k}

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.

Equations
@[ext]

Two maps from a coequalizer are equal if they are equal when composed with the coequalizer map

@[instance]

A coequalizer morphism is an epimorphism

def category_theory.limits.id_cofork {C : Type u} [category_theory.category C] {X Y : C} {f g : X Y} :

The identity determines a cocone on the coequalizer diagram of f and g, if f = g.

Equations

The identity on Y is a coequalizer of (f, g), where f = g.

Equations

has_equalizers represents a choice of equalizer for every pair of morphisms

Instances

has_coequalizers represents a choice of coequalizer for every pair of morphisms

Instances

If C has all limits of diagrams parallel_pair f g, then it has all equalizers

If C has all colimits of diagrams parallel_pair f g, then it has all coequalizers

A split mono f equalizes (retraction f ≫ f) and (𝟙 Y). Here we build the cone, and show in split_mono_equalizes that it is a limit cone.

Equations

A split epi f coequalizes (f ≫ section_ f) and (𝟙 X). Here we build the cocone, and show in split_epi_coequalizes that it is a colimit cocone.

Equations