Multicoequalizers in the category of types #
Given J : MultispanShape, d : MultispanIndex J (Type u) and
c : d.multispan.CoconeTypes, we obtain a lemma isMulticoequalizer_iff
which gives a criteria for c to be a colimit (i.e. a multicoequalizer):
it restates in a more explicit manner the injectivity and surjectivity
conditions for the map d.multispan.descColimitType c : d.multispan.ColimitType → c.pt.
We deduce a definition Set.isColimitOfMulticoequalizerDiagram which shows
that given X : Type u, a MulticoequalizerDiagram in Set X gives
a multicoequalizer in the category of types.
theorem
CategoryTheory.Functor.CoconeTypes.isMulticoequalizer_iff
{J : Limits.MultispanShape}
{d : Limits.MultispanIndex J (Type u)}
(c : d.multispan.CoconeTypes)
:
c.IsColimit ↔ (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
c.ι (Limits.WalkingMultispan.right i₁) x₁ = c.ι (Limits.WalkingMultispan.right i₂) x₂ →
d.multispan.ιColimitType (Limits.WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (Limits.WalkingMultispan.right i₂) x₂) ∧ ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (Limits.WalkingMultispan.right i) a = x
noncomputable def
CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram
{X : Type u}
{ι : Type w}
{A : Set X}
{U : ι → Set X}
{V : ι → ι → Set X}
(c : CompleteLattice.MulticoequalizerDiagram A U V)
:
Given X : Type u, A : Set X, U : ι → Set X and V : ι → ι → Set X such
that MulticoequalizerDiagram A U V holds, then in the category of types,
A is the multicoequalizer of the U is along the V i js.