Colimits involving subcomplexes of a simplicial set

If X is a simplicial set, and we have subcomplexes A, U i (for i : ι) and V i j which satisfy Subcomplex.MulticoequalizerDiagram A U V (an abbreviation for CompleteLattice.MulticoequalizerDiagram), we show that the simplicial sset corresponding to A is the multicoequalizer of the U i along the V i j.

Similarly, bicartesian squares in the lattice Subcomplex X give pushout squares in the category of simplicial sets.

@[reducible, inline]

abbrev SSet.Subcomplex.MulticoequalizerDiagram {X : SSet} (A : X.Subcomplex) {ι : Type u_1} (U : ι → X.Subcomplex) (V : ι → ι → X.Subcomplex) : Prop

Abbreviation for multicoequalizer diagrams in the complete lattice of subcomplexes of a simplicial set.

noncomputable def SSet.Subcomplex.MulticoequalizerDiagram.isColimit {X : SSet} {A : X.Subcomplex} {ι : Type u_1} {U : ι → X.Subcomplex} {V : ι → ι → X.Subcomplex} (h : A.MulticoequalizerDiagram U V) : CategoryTheory.Limits.IsColimit ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor)

The colimit multicofork attached to a MulticoequalizerDiagram structure in the complete lattice of subcomplexes of a simplicial set.

noncomputable def SSet.Subcomplex.MulticoequalizerDiagram.isColimit' {X : SSet} {A : X.Subcomplex} {ι : Type u_1} {U : ι → X.Subcomplex} {V : ι → ι → X.Subcomplex} (h : A.MulticoequalizerDiagram U V) [LinearOrder ι] : CategoryTheory.Limits.IsColimit ((CompleteLattice.MulticoequalizerDiagram.multicofork h).toLinearOrder.map toSSetFunctor)

A colimit multicofork attached to a MulticoequalizerDiagram structure in the complete lattice of subcomplexes of a simplicial set. In this variant, we assume that the index type ι has a linear order. This allows to consider only the "relations" given by tuples (i, j) such that i < j.

@[reducible, inline]

abbrev SSet.Subcomplex.BicartSq {X : SSet} (A₁ A₂ A₃ A₄ : X.Subcomplex) : Prop

Abbreviation for bicartesian squares in the lattice of subcomplexes of a simplicial set.

theorem SSet.Subcomplex.BicartSq.isPushout {X : SSet} {A₁ A₂ A₃ A₄ : X.Subcomplex} (sq : A₁.BicartSq A₂ A₃ A₄) : CategoryTheory.IsPushout (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)