# mathlib3documentation

category_theory.limits.shapes.multiequalizer

# Multi-(co)equalizers #

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

A multiequalizer is an equalizer of two morphisms between two products. Since both products and equalizers are limits, such an object is again a limit. This file provides the diagram whose limit is indeed such an object. In fact, it is well-known that any limit can be obtained as a multiequalizer. The dual construction (multicoequalizers) is also provided.

## Projects #

Prove that a multiequalizer can be identified with an equalizer between products (and analogously for multicoequalizers).

Prove that the limit of any diagram is a multiequalizer (and similarly for colimits).

@[nolint]
inductive category_theory.limits.walking_multicospan {L R : Type w} (fst snd : R L) :
• left : Π {L R : Type w} {fst snd : R L},
• right : Π {L R : Type w} {fst snd : R L},

The type underlying the multiequalizer diagram.

Instances for `category_theory.limits.walking_multicospan`
@[nolint]
inductive category_theory.limits.walking_multispan {L R : Type w} (fst snd : L R) :
• left : Π {L R : Type w} {fst snd : L R},
• right : Π {L R : Type w} {fst snd : L R},

The type underlying the multiecoqualizer diagram.

Instances for `category_theory.limits.walking_multispan`
@[protected, instance]
Equations
inductive category_theory.limits.walking_multicospan.hom {L R : Type w} {fst snd : R L} (a b : snd) :
• id : Π {L R : Type w} {fst snd : R L} (A : , A.hom A
• fst : Π {L R : Type w} {fst snd : R L} (b : R),
• snd : Π {L R : Type w} {fst snd : R L} (b : R),

Morphisms for `walking_multicospan`.

Instances for `category_theory.limits.walking_multicospan.hom`
@[protected, instance]
def category_theory.limits.walking_multicospan.hom.inhabited {L R : Type w} {fst snd : R L} {a : snd} :
Equations
def category_theory.limits.walking_multicospan.hom.comp {L R : Type w} {fst snd : R L} {A B C : snd} (f : A.hom B) (g : B.hom C) :
A.hom C

Composition of morphisms for `walking_multicospan`.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
inductive category_theory.limits.walking_multispan.hom {L R : Type v} {fst snd : L R} (a b : snd) :
• id : Π {L R : Type v} {fst snd : L R} (A : , A.hom A
• fst : Π {L R : Type v} {fst snd : L R} (a : L),
• snd : Π {L R : Type v} {fst snd : L R} (a : L),

Morphisms for `walking_multispan`.

Instances for `category_theory.limits.walking_multispan.hom`
@[protected, instance]
def category_theory.limits.walking_multispan.hom.inhabited {L R : Type v} {fst snd : L R} {a : snd} :
Equations
def category_theory.limits.walking_multispan.hom.comp {L R : Type v} {fst snd : L R} {A B C : snd} (f : A.hom B) (g : B.hom C) :
A.hom C

Composition of morphisms for `walking_multispan`.

Equations
@[protected, instance]
Equations
@[nolint]
structure category_theory.limits.multicospan_index (C : Type u)  :
Type (max u v (w+1))

This is a structure encapsulating the data necessary to define a `multicospan`.

Instances for `category_theory.limits.multicospan_index`
• category_theory.limits.multicospan_index.has_sizeof_inst
@[nolint]
structure category_theory.limits.multispan_index (C : Type u)  :
Type (max u v (w+1))

This is a structure encapsulating the data necessary to define a `multispan`.

Instances for `category_theory.limits.multispan_index`
• category_theory.limits.multispan_index.has_sizeof_inst

The multicospan associated to `I : multicospan_index`.

Equations
• I.multicospan = {obj := λ (x : , category_theory.limits.multicospan_index.multicospan._match_1 I x, map := λ (x y : (f : x y), category_theory.limits.multicospan_index.multicospan._match_2 I x y f, map_id' := _, map_comp' := _}
• category_theory.limits.multicospan_index.multicospan._match_1 I = I.right b
• category_theory.limits.multicospan_index.multicospan._match_1 I = I.left a
• category_theory.limits.multicospan_index.multicospan._match_2 I = I.snd b
• category_theory.limits.multicospan_index.multicospan._match_2 I = I.fst b
• category_theory.limits.multicospan_index.multicospan._match_2 I x x = 𝟙 (category_theory.limits.multicospan_index.multicospan._match_1 I x)

The induced map `∏ I.left ⟶ ∏ I.right` via `I.fst`.

Equations

The induced map `∏ I.left ⟶ ∏ I.right` via `I.snd`.

Equations
@[simp]
theorem category_theory.limits.multicospan_index.fst_pi_map_π_assoc {C : Type u} (b : I.R) {X' : C} (f' : I.right b X') :
@[simp]
theorem category_theory.limits.multicospan_index.snd_pi_map_π_assoc {C : Type u} (b : I.R) {X' : C} (f' : I.right b X') :
@[simp]
theorem category_theory.limits.multicospan_index.parallel_pair_diagram_obj {C : Type u}  :
= category_theory.limits.parallel_pair._match_1 x
@[simp]
theorem category_theory.limits.multicospan_index.parallel_pair_diagram_map {C : Type u} (h : x y) :
= category_theory.limits.parallel_pair._match_2 I.fst_pi_map I.snd_pi_map x y h
@[protected]

Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over the two morphsims `∏ I.left ⇉ ∏ I.right`. This is the diagram of the latter.

Equations

The multispan associated to `I : multispan_index`.

Equations
• I.multispan = {obj := λ (x : , category_theory.limits.multispan_index.multispan._match_1 I x, map := λ (x y : (f : x y), category_theory.limits.multispan_index.multispan._match_2 I x y f, map_id' := _, map_comp' := _}
• category_theory.limits.multispan_index.multispan._match_1 I = I.right b
• category_theory.limits.multispan_index.multispan._match_1 I = I.left a
• category_theory.limits.multispan_index.multispan._match_2 I = I.snd b
• category_theory.limits.multispan_index.multispan._match_2 I = I.fst b
• category_theory.limits.multispan_index.multispan._match_2 I x x = 𝟙 (category_theory.limits.multispan_index.multispan._match_1 I x)
Instances for `category_theory.limits.multispan_index.multispan`

The induced map `∐ I.left ⟶ ∐ I.right` via `I.fst`.

Equations

The induced map `∐ I.left ⟶ ∐ I.right` via `I.snd`.

Equations
@[simp]
theorem category_theory.limits.multispan_index.ι_fst_sigma_map_assoc {C : Type u} (b : I.L) {X' : C} (f' : I.right X') :
= I.fst b f'
@[simp]
@[simp]
theorem category_theory.limits.multispan_index.ι_snd_sigma_map_assoc {C : Type u} (b : I.L) {X' : C} (f' : I.right X') :
= I.snd b f'
@[simp]
@[protected, reducible]

Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer over the two morphsims `∐ I.left ⇉ ∐ I.right`. This is the diagram of the latter.

@[nolint, reducible]
def category_theory.limits.multifork {C : Type u}  :
Type (max u_1 u v)

A multifork is a cone over a multicospan.

@[nolint, reducible]
def category_theory.limits.multicofork {C : Type u}  :
Type (max u_1 u v)

A multicofork is a cocone over a multispan.

def category_theory.limits.multifork.ι {C : Type u} (a : I.L) :
K.X I.left a

The maps from the cone point of a multifork to the objects on the left.

Equations
@[simp]
@[simp]
theorem category_theory.limits.multifork.app_right_eq_ι_comp_snd_assoc {C : Type u} (b : I.R) {X' : C} (f' : X') :
= K.ι (I.snd_to b) I.snd b f'
@[simp]
theorem category_theory.limits.multifork.hom_comp_ι {C : Type u} (K₁ K₂ : category_theory.limits.multifork I) (f : K₁ K₂) (j : I.L) :
f.hom K₂.ι j = K₁.ι j
@[simp]
theorem category_theory.limits.multifork.hom_comp_ι_assoc {C : Type u} (K₁ K₂ : category_theory.limits.multifork I) (f : K₁ K₂) (j : I.L) {X' : C} (f' : I.left j X') :
f.hom K₂.ι j f' = K₁.ι j f'
@[simp]
theorem category_theory.limits.multifork.of_ι_π_app {C : Type u} (P : C) (ι : Π (a : I.L), P I.left a) (w : (b : I.R), ι (I.fst_to b) I.fst b = ι (I.snd_to b) I.snd b)  :
.π.app x = category_theory.limits.multifork.of_ι._match_1 I P ι x
def category_theory.limits.multifork.of_ι {C : Type u} (P : C) (ι : Π (a : I.L), P I.left a) (w : (b : I.R), ι (I.fst_to b) I.fst b = ι (I.snd_to b) I.snd b) :

Construct a multifork using a collection `ι` of morphisms.

Equations
• = {X := P, π := {app := λ (x : , category_theory.limits.multifork.of_ι._match_1 I P ι x, naturality' := _}}
• category_theory.limits.multifork.of_ι._match_1 I P ι = ι (I.fst_to b) I.fst b
• category_theory.limits.multifork.of_ι._match_1 I P ι = ι a
@[simp]
theorem category_theory.limits.multifork.of_ι_X {C : Type u} (P : C) (ι : Π (a : I.L), P I.left a) (w : (b : I.R), ι (I.fst_to b) I.fst b = ι (I.snd_to b) I.snd b) :
.X = P
@[simp]
theorem category_theory.limits.multifork.condition {C : Type u} (b : I.R) :
K.ι (I.fst_to b) I.fst b = K.ι (I.snd_to b) I.snd b
@[simp]
theorem category_theory.limits.multifork.condition_assoc {C : Type u} (b : I.R) {X' : C} (f' : I.right b X') :
K.ι (I.fst_to b) I.fst b f' = K.ι (I.snd_to b) I.snd b f'
@[simp]
theorem category_theory.limits.multifork.is_limit.mk_lift {C : Type u} (lift : Π (E : , E.X K.X) (fac : (E : (i : I.L), lift E K.ι i = E.ι i) (uniq : (E : (m : E.X K.X), ( (i : I.L), m K.ι i = E.ι i) m = lift E)  :
fac uniq).lift E = lift E
def category_theory.limits.multifork.is_limit.mk {C : Type u} (lift : Π (E : , E.X K.X) (fac : (E : (i : I.L), lift E K.ι i = E.ι i) (uniq : (E : (m : E.X K.X), ( (i : I.L), m K.ι i = E.ι i) m = lift E) :

This definition provides a convenient way to show that a multifork is a limit.

Equations
@[simp]
@[simp]
theorem category_theory.limits.multifork.pi_condition_assoc {C : Type u} {X' : C} (f' : I.right X') :
=

Given a multifork, we may obtain a fork over `∏ I.left ⇉ ∏ I.right`.

Equations
@[simp]
@[simp]
@[simp]

Given a fork over `∏ I.left ⇉ ∏ I.right`, we may obtain a multifork.

Equations
• = {X := c.X, π := {app := λ (x : , category_theory.limits.multifork.of_pi_fork._match_1 I c x, naturality' := _}}
• category_theory.limits.multifork.of_pi_fork._match_1 I c =
• category_theory.limits.multifork.of_pi_fork._match_1 I c =
@[simp]
@[simp]
@[simp]
@[simp]

`multifork.to_pi_fork` is functorial.

Equations
@[simp]

`multifork.of_pi_fork` is functorial.

Equations
@[simp]
@[simp]
@[simp]
@[simp]

The category of multiforks is equivalent to the category of forks over `∏ I.left ⇉ ∏ I.right`. It then follows from `category_theory.is_limit_of_preserves_cone_terminal` (or `reflects`) that it preserves and reflects limit cones.

Equations
def category_theory.limits.multicofork.π {C : Type u} (b : I.R) :
I.right b K.X

The maps to the cocone point of a multicofork from the objects on the right.

Equations
@[simp]
theorem category_theory.limits.multicofork.fst_app_right {C : Type u} (a : I.L) :
= I.fst a K.π (I.fst_from a)
theorem category_theory.limits.multicofork.snd_app_right_assoc {C : Type u} (a : I.L) {X' : C}  :
= I.snd a K.π (I.snd_from a) f'
@[simp]
theorem category_theory.limits.multicofork.of_π_ι_app {C : Type u} (P : C) (π : Π (b : I.R), I.right b P) (w : (a : I.L), I.fst a π (I.fst_from a) = I.snd a π (I.snd_from a))  :
.ι.app x = category_theory.limits.multicofork.of_π._match_1 I P π x
def category_theory.limits.multicofork.of_π {C : Type u} (P : C) (π : Π (b : I.R), I.right b P) (w : (a : I.L), I.fst a π (I.fst_from a) = I.snd a π (I.snd_from a)) :

Construct a multicofork using a collection `π` of morphisms.

Equations
• = {X := P, ι := {app := λ (x : , category_theory.limits.multicofork.of_π._match_1 I P π x, naturality' := _}}
• category_theory.limits.multicofork.of_π._match_1 I P π = π b
• category_theory.limits.multicofork.of_π._match_1 I P π = I.fst a π (I.fst_from a)
@[simp]
theorem category_theory.limits.multicofork.of_π_X {C : Type u} (P : C) (π : Π (b : I.R), I.right b P) (w : (a : I.L), I.fst a π (I.fst_from a) = I.snd a π (I.snd_from a)) :
.X = P
@[simp]
theorem category_theory.limits.multicofork.condition_assoc {C : Type u} (a : I.L) {X' : C} (f' : K.X X') :
I.fst a K.π (I.fst_from a) f' = I.snd a K.π (I.snd_from a) f'
@[simp]
theorem category_theory.limits.multicofork.condition {C : Type u} (a : I.L) :
I.fst a K.π (I.fst_from a) = I.snd a K.π (I.snd_from a)
@[simp]
theorem category_theory.limits.multicofork.is_colimit.mk_desc {C : Type u} (desc : Π (E : , K.X E.X) (fac : (E : (i : I.R), K.π i desc E = E.π i) (uniq : (E : (m : K.X E.X), ( (i : I.R), K.π i m = E.π i) m = desc E)  :
uniq).desc E = desc E
def category_theory.limits.multicofork.is_colimit.mk {C : Type u} (desc : Π (E : , K.X E.X) (fac : (E : (i : I.R), K.π i desc E = E.π i) (uniq : (E : (m : K.X E.X), ( (i : I.R), K.π i m = E.π i) m = desc E) :

This definition provides a convenient way to show that a multicofork is a colimit.

Equations
@[simp]
theorem category_theory.limits.multicofork.sigma_condition_assoc {C : Type u} {X' : C} (f' : K.X X') :
@[simp]

Given a multicofork, we may obtain a cofork over `∐ I.left ⇉ ∐ I.right`.

Equations
@[simp]
@[simp]

Given a cofork over `∐ I.left ⇉ ∐ I.right`, we may obtain a multicofork.

Equations
• = {X := c.X, ι := {app := λ (x : , category_theory.limits.multicofork.of_sigma_cofork._match_1 I c x, naturality' := _}}
• category_theory.limits.multicofork.of_sigma_cofork._match_1 I c =
• category_theory.limits.multicofork.of_sigma_cofork._match_1 I c =
@[simp]
@[simp]
@[simp]
@[simp]

`multicofork.to_sigma_cofork` is functorial.

Equations
@[simp]

`multicofork.of_sigma_cofork` is functorial.

Equations
@[simp]
@[simp]
@[simp]

The category of multicoforks is equivalent to the category of coforks over `∐ I.left ⇉ ∐ I.right`. It then follows from `category_theory.is_colimit_of_preserves_cocone_initial` (or `reflects`) that it preserves and reflects colimit cocones.

Equations
@[simp]
@[simp]
@[reducible]

For `I : multicospan_index C`, we say that it has a multiequalizer if the associated multicospan has a limit.

@[reducible]
noncomputable def category_theory.limits.multiequalizer {C : Type u}  :
C

The multiequalizer of `I : multicospan_index C`.

@[reducible]

For `I : multispan_index C`, we say that it has a multicoequalizer if the associated multicospan has a limit.

@[reducible]
noncomputable def category_theory.limits.multicoequalizer {C : Type u}  :
C

The multiecoqualizer of `I : multispan_index C`.

@[reducible]
noncomputable def category_theory.limits.multiequalizer.ι {C : Type u} (a : I.L) :

The canonical map from the multiequalizer to the objects on the left.

@[reducible]

The multifork associated to the multiequalizer.

@[simp]
@[simp]
theorem category_theory.limits.multiequalizer.condition_assoc {C : Type u} (b : I.R) {X' : C} (f' : I.right b X') :
I.fst b f' = I.snd b f'
@[reducible]
noncomputable def category_theory.limits.multiequalizer.lift {C : Type u} (W : C) (k : Π (a : I.L), W I.left a) (h : (b : I.R), k (I.fst_to b) I.fst b = k (I.snd_to b) I.snd b) :

Construct a morphism to the multiequalizer from its universal property.

@[simp]
theorem category_theory.limits.multiequalizer.lift_ι_assoc {C : Type u} (W : C) (k : Π (a : I.L), W I.left a) (h : (b : I.R), k (I.fst_to b) I.fst b = k (I.snd_to b) I.snd b) (a : I.L) {X' : C} (f' : I.left a X') :
= k a f'
@[simp]
theorem category_theory.limits.multiequalizer.lift_ι {C : Type u} (W : C) (k : Π (a : I.L), W I.left a) (h : (b : I.R), k (I.fst_to b) I.fst b = k (I.snd_to b) I.snd b) (a : I.L) :
@[ext]
theorem category_theory.limits.multiequalizer.hom_ext {C : Type u} {W : C} (i j : W ) (h : (a : I.L), ) :
i = j
@[protected, instance]

The multiequalizer is isomorphic to the equalizer of `∏ I.left ⇉ ∏ I.right`.

Equations

The canonical injection `multiequalizer I ⟶ ∏ I.left`.

Equations
Instances for `category_theory.limits.multiequalizer.ι_pi`
@[simp]
@[simp]
theorem category_theory.limits.multiequalizer.ι_pi_π_assoc {C : Type u} (a : I.L) {X' : C} (f' : I.left a X') :
@[protected, instance]
@[reducible]
noncomputable def category_theory.limits.multicoequalizer.π {C : Type u} (b : I.R) :

The canonical map from the multiequalizer to the objects on the left.

@[reducible]

The multicofork associated to the multicoequalizer.

@[simp]
@[simp]
theorem category_theory.limits.multicoequalizer.condition_assoc {C : Type u} (a : I.L) {X' : C} (f' : X') :
I.fst a = I.snd a
@[reducible]
noncomputable def category_theory.limits.multicoequalizer.desc {C : Type u} (W : C) (k : Π (b : I.R), I.right b W) (h : (a : I.L), I.fst a k (I.fst_from a) = I.snd a k (I.snd_from a)) :

Construct a morphism from the multicoequalizer from its universal property.

@[simp]
theorem category_theory.limits.multicoequalizer.π_desc {C : Type u} (W : C) (k : Π (b : I.R), I.right b W) (h : (a : I.L), I.fst a k (I.fst_from a) = I.snd a k (I.snd_from a)) (b : I.R) :
@[simp]
theorem category_theory.limits.multicoequalizer.π_desc_assoc {C : Type u} (W : C) (k : Π (b : I.R), I.right b W) (h : (a : I.L), I.fst a k (I.fst_from a) = I.snd a k (I.snd_from a)) (b : I.R) {X' : C} (f' : W X') :
= k b f'
@[ext]
theorem category_theory.limits.multicoequalizer.hom_ext {C : Type u} {W : C} (i j : W) (h : (b : I.R), ) :
i = j
@[protected, instance]

The multicoequalizer is isomorphic to the coequalizer of `∐ I.left ⇉ ∐ I.right`.

Equations

The canonical projection `∐ I.right ⟶ multicoequalizer I`.

Equations
Instances for `category_theory.limits.multicoequalizer.sigma_π`
@[simp]
@[simp]
@[protected, instance]