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).
- left: {L R : Type w} → {fst snd : R → L} → L → CategoryTheory.Limits.WalkingMulticospan fst snd
- right: {L R : Type w} → {fst snd : R → L} → R → CategoryTheory.Limits.WalkingMulticospan fst snd
The type underlying the multiequalizer diagram.
Instances For
- left: {L R : Type w} → {fst snd : L → R} → L → CategoryTheory.Limits.WalkingMultispan fst snd
- right: {L R : Type w} → {fst snd : L → R} → R → CategoryTheory.Limits.WalkingMultispan fst snd
The type underlying the multiecoqualizer diagram.
Instances For
- id: {L R : Type w} → {fst snd : R → L} → (A : CategoryTheory.Limits.WalkingMulticospan fst snd) → CategoryTheory.Limits.WalkingMulticospan.Hom A A
- fst: {L R : Type w} → {fst snd : R → L} → (b : R) → CategoryTheory.Limits.WalkingMulticospan.Hom (CategoryTheory.Limits.WalkingMulticospan.left (fst b)) (CategoryTheory.Limits.WalkingMulticospan.right b)
- snd: {L R : Type w} → {fst snd : R → L} → (b : R) → CategoryTheory.Limits.WalkingMulticospan.Hom (CategoryTheory.Limits.WalkingMulticospan.left (snd b)) (CategoryTheory.Limits.WalkingMulticospan.right b)
Morphisms for WalkingMulticospan
.
Instances For
Composition of morphisms for WalkingMulticospan
.
Instances For
- id: {L R : Type v} → {fst snd : L → R} → (A : CategoryTheory.Limits.WalkingMultispan fst snd) → CategoryTheory.Limits.WalkingMultispan.Hom A A
- fst: {L R : Type v} → {fst snd : L → R} → (a : L) → CategoryTheory.Limits.WalkingMultispan.Hom (CategoryTheory.Limits.WalkingMultispan.left a) (CategoryTheory.Limits.WalkingMultispan.right (fst a))
- snd: {L R : Type v} → {fst snd : L → R} → (a : L) → CategoryTheory.Limits.WalkingMultispan.Hom (CategoryTheory.Limits.WalkingMultispan.left a) (CategoryTheory.Limits.WalkingMultispan.right (snd a))
Morphisms for WalkingMultispan
.
Instances For
Composition of morphisms for WalkingMultispan
.
Instances For
- L : Type w
- R : Type w
- fstTo : s.R → s.L
- sndTo : s.R → s.L
- left : s.L → C
- right : s.R → C
- fst : (b : s.R) → CategoryTheory.Limits.MulticospanIndex.left s (CategoryTheory.Limits.MulticospanIndex.fstTo s b) ⟶ CategoryTheory.Limits.MulticospanIndex.right s b
- snd : (b : s.R) → CategoryTheory.Limits.MulticospanIndex.left s (CategoryTheory.Limits.MulticospanIndex.sndTo s b) ⟶ CategoryTheory.Limits.MulticospanIndex.right s b
This is a structure encapsulating the data necessary to define a Multicospan
.
Instances For
- L : Type w
- R : Type w
- fstFrom : s.L → s.R
- sndFrom : s.L → s.R
- left : s.L → C
- right : s.R → C
- fst : (a : s.L) → CategoryTheory.Limits.MultispanIndex.left s a ⟶ CategoryTheory.Limits.MultispanIndex.right s (CategoryTheory.Limits.MultispanIndex.fstFrom s a)
- snd : (a : s.L) → CategoryTheory.Limits.MultispanIndex.left s a ⟶ CategoryTheory.Limits.MultispanIndex.right s (CategoryTheory.Limits.MultispanIndex.sndFrom s a)
This is a structure encapsulating the data necessary to define a Multispan
.
Instances For
The multicospan associated to I : MulticospanIndex
.
Instances For
The induced map ∏ I.left ⟶ ∏ I.right
via I.fst
.
Instances For
The induced map ∏ I.left ⟶ ∏ I.right
via I.snd
.
Instances For
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.
Instances For
The multispan associated to I : MultispanIndex
.
Instances For
The induced map ∐ I.left ⟶ ∐ I.right
via I.fst
.
Instances For
The induced map ∐ I.left ⟶ ∐ I.right
via I.snd
.
Instances For
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.
Instances For
A multifork is a cone over a multicospan.
Instances For
A multicofork is a cocone over a multispan.
Instances For
The maps from the cone point of a multifork to the objects on the left.
Instances For
Construct a multifork using a collection ι
of morphisms.
Instances For
This definition provides a convenient way to show that a multifork is a limit.
Instances For
Given a multifork, we may obtain a fork over ∏ I.left ⇉ ∏ I.right
.
Instances For
Given a fork over ∏ I.left ⇉ ∏ I.right
, we may obtain a multifork.
Instances For
Multifork.toPiFork
as a functor.
Instances For
Multifork.ofPiFork
as a functor.
Instances For
The category of multiforks is equivalent to the category of forks over ∏ I.left ⇉ ∏ I.right
.
It then follows from CategoryTheory.IsLimit.ofPreservesConeTerminal
(or reflects
) that it
preserves and reflects limit cones.
Instances For
The maps to the cocone point of a multicofork from the objects on the right.
Instances For
Construct a multicofork using a collection π
of morphisms.
Instances For
This definition provides a convenient way to show that a multicofork is a colimit.
Instances For
Given a multicofork, we may obtain a cofork over ∐ I.left ⇉ ∐ I.right
.
Instances For
Given a cofork over ∐ I.left ⇉ ∐ I.right
, we may obtain a multicofork.
Instances For
Multicofork.toSigmaCofork
as a functor.
Instances For
Multicofork.ofSigmaCofork
as a functor.
Instances For
The category of multicoforks is equivalent to the category of coforks over ∐ I.left ⇉ ∐ I.right
.
It then follows from CategoryTheory.IsColimit.ofPreservesCoconeInitial
(or reflects
) that
it preserves and reflects colimit cocones.
Instances For
For I : MulticospanIndex C
, we say that it has a multiequalizer if the associated
multicospan has a limit.
Instances For
The multiequalizer of I : MulticospanIndex C
.
Instances For
For I : MultispanIndex C
, we say that it has a multicoequalizer if
the associated multicospan has a limit.
Instances For
The multiecoqualizer of I : MultispanIndex C
.
Instances For
The canonical map from the multiequalizer to the objects on the left.
Instances For
The multifork associated to the multiequalizer.
Instances For
Construct a morphism to the multiequalizer from its universal property.
Instances For
The multiequalizer is isomorphic to the equalizer of ∏ I.left ⇉ ∏ I.right
.
Instances For
The canonical injection multiequalizer I ⟶ ∏ I.left
.
Instances For
The canonical map from the multiequalizer to the objects on the left.
Instances For
The multicofork associated to the multicoequalizer.
Instances For
Construct a morphism from the multicoequalizer from its universal property.
Instances For
The multicoequalizer is isomorphic to the coequalizer of ∐ I.left ⇉ ∐ I.right
.
Instances For
The canonical projection ∐ I.right ⟶ multicoequalizer I
.