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) : IsColimit (c.multicofork.map Set.functorToTypes)

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.

Equations

• CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram c = ⋯.some

noncomputable def CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram' {X : Type u} {ι : Type w} {A : Set X} {U : ι → Set X} {V : ι → ι → Set X} [LinearOrder ι] (c : CompleteLattice.MulticoequalizerDiagram A U V) : IsColimit (c.multicofork.toLinearOrder.map Set.functorToTypes)

Let 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. In this version, we assume ι has a linear order, which allows to consider only the V i j for which i < j.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.Types.isPushout_of_bicartSq {X : Type u} {S₁ S₂ S₃ S₄ : Set X} (h : Lattice.BicartSq S₁ S₂ S₃ S₄) : IsPushout (Set.functorToTypes.map (homOfLE ⋯)) (Set.functorToTypes.map (homOfLE ⋯)) (Set.functorToTypes.map (homOfLE ⋯)) (Set.functorToTypes.map (homOfLE ⋯))

A bicartesian square in the lattice Set X gives a pushout diagram in the category of types.