mathlib documentation

category_theory.limits.shapes.multiequalizer

Multi-(co)equalizers #

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

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

The type underlying the multiecoqualizer diagram.

Instances for category_theory.limits.walking_multispan

Morphisms for walking_multicospan.

Instances for category_theory.limits.walking_multicospan.hom

Morphisms for walking_multispan.

Instances for category_theory.limits.walking_multispan.hom
@[nolint]

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]

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
@[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
Instances for category_theory.limits.multispan_index.multispan
@[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]

A multifork is a cone over a multicospan.

@[nolint, reducible]

A multicofork is a cocone over a multispan.

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

Equations
@[simp]
theorem category_theory.limits.multifork.hom_comp_ι_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (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} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (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 : category_theory.limits.walking_multicospan I.fst_to I.snd_to) :
(category_theory.limits.multifork.of_ι I P ι w).π.app x = category_theory.limits.multifork.of_ι._match_1 I P ι x
def category_theory.limits.multifork.of_ι {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (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
@[simp]
theorem category_theory.limits.multifork.of_ι_X {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (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) :

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

Equations

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

Equations

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

Equations

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

Equations
@[simp]
theorem category_theory.limits.multicofork.of_π_ι_app {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (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 : category_theory.limits.walking_multispan I.fst_from I.snd_from) :
(category_theory.limits.multicofork.of_π I P π w).ι.app x = category_theory.limits.multicofork.of_π._match_1 I P π x

Construct a multicofork using a collection π of morphisms.

Equations
@[simp]
theorem category_theory.limits.multicofork.of_π_X {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (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)) :

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

Equations

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

Equations

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

Equations
@[reducible]

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

@[reducible]

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]

The multiecoqualizer of I : multispan_index C.

@[reducible]

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

@[reducible]

Construct a morphism to the multiequalizer from its universal property.

@[reducible]

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

@[reducible]

Construct a morphism from the multicoequalizer from its universal property.