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

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

The type underlying the multiecoqualizer diagram.

Instances for category_theory.limits.walking_multispan
inductive category_theory.limits.walking_multicospan.hom {L R : Type w} {fst snd : R → L} (a b : category_theory.limits.walking_multicospan fst snd) :
Type w

Morphisms for walking_multicospan.

Instances for category_theory.limits.walking_multicospan.hom
inductive category_theory.limits.walking_multispan.hom {L R : Type v} {fst snd : L → R} (a b : category_theory.limits.walking_multispan fst snd) :
Type v

Morphisms for walking_multispan.

Instances for category_theory.limits.walking_multispan.hom
@[nolint]
structure category_theory.limits.multicospan_index (C : Type u) [category_theory.category C] :
Type (max u v (w+1))
  • L : Type ?
  • R : Type ?
  • fst_to : self.R → self.L
  • snd_to : self.R → self.L
  • left : self.L → C
  • right : self.R → C
  • fst : Π (b : self.R), self.left (self.fst_to b) self.right b
  • snd : Π (b : self.R), self.left (self.snd_to b) self.right b

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) [category_theory.category C] :
Type (max u v (w+1))
  • L : Type ?
  • R : Type ?
  • fst_from : self.L → self.R
  • snd_from : self.L → self.R
  • left : self.L → C
  • right : self.R → C
  • fst : Π (a : self.L), self.left a self.right (self.fst_from a)
  • snd : Π (a : self.L), self.left a self.right (self.snd_from a)

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_ι {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) :
f.hom K₂.ι j = K₁.ι j
@[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) :
@[simp]
@[simp]
theorem category_theory.limits.multifork.is_limit.mk_lift {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (lift : Π (E : category_theory.limits.multifork I), E.X K.X) (fac : ∀ (E : category_theory.limits.multifork I) (i : I.L), lift E K.ι i = E.ι i) (uniq : ∀ (E : category_theory.limits.multifork I) (m : E.X K.X), (∀ (i : I.L), m K.ι i = E.ι i)m = lift E) (E : category_theory.limits.multifork I) :
def category_theory.limits.multifork.is_limit.mk {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (lift : Π (E : category_theory.limits.multifork I), E.X K.X) (fac : ∀ (E : category_theory.limits.multifork I) (i : I.L), lift E K.ι i = E.ι i) (uniq : ∀ (E : category_theory.limits.multifork I) (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

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
def category_theory.limits.multicofork.of_π {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)) :

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)) :
@[simp]
@[simp]
theorem category_theory.limits.multicofork.is_colimit.mk_desc {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (desc : Π (E : category_theory.limits.multicofork I), K.X E.X) (fac : ∀ (E : category_theory.limits.multicofork I) (i : I.R), K.π i desc E = E.π i) (uniq : ∀ (E : category_theory.limits.multicofork I) (m : K.X E.X), (∀ (i : I.R), K.π i m = E.π i)m = desc E) (E : category_theory.limits.multicofork I) :
def category_theory.limits.multicofork.is_colimit.mk {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (desc : Π (E : category_theory.limits.multicofork I), K.X E.X) (fac : ∀ (E : category_theory.limits.multicofork I) (i : I.R), K.π i desc E = E.π i) (uniq : ∀ (E : category_theory.limits.multicofork I) (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

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.

@[simp]
@[reducible]

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

@[reducible]

Construct a morphism from the multicoequalizer from its universal property.