Nonsingular simplicial sets, as colimits of standard simplices

In the file Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesColimit.lean, it was shown that any simplicial set X is the colimit (indexed by the type X.N of nondegenerate simplices) of its monogenous subcomplexes.

In this file, we assume that X is nonsingular, in which case its monogenous subcomplexes identify to standard simplices. This allows to show that X is the colimit of Δ[x.dim] for x : X.N.

noncomputable def SSet.N.toSemiSimplexCategory (X : SSet) [X.Nonsingular] : CategoryTheory.Functor X.N SemiSimplexCategory

If X is a nonsingular simplicial set, this is the functor X.N ⥤ SemiSimplexCategory which sends a nondegenerate simplex s : X : N to ⦋s.dim⦌ₛ

Equations

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

@[simp]

theorem SSet.N.toSemiSimplexCategory_map (X : SSet) [X.Nonsingular] {X✝ Y✝ : X.N} (f : X✝ ⟶ Y✝) : (toSemiSimplexCategory X).map f = SemiSimplexCategory.homOfMono (monoOfLE ⋯)

@[simp]

theorem SSet.N.toSemiSimplexCategory_obj (X : SSet) [X.Nonsingular] (s : X.N) : (toSemiSimplexCategory X).obj s = { len := s.dim }

@[reducible, inline]

noncomputable abbrev SSet.functorN' (X : SSet) [X.Nonsingular] : CategoryTheory.Functor X.N SSet

The functor X.N ⥤ SSet which sends x : X.N to Δ[x.dim].

Equations

• X.functorN' = (SSet.N.toSemiSimplexCategory X).comp (SemiSimplexCategory.toSimplexCategory.comp SSet.stdSimplex)

noncomputable def SSet.functorN'Iso (X : SSet) [X.Nonsingular] : X.functorN' ≅ X.functorN

The isomorphism X.functorN' ≅ X.functorN for a nonsingular simplicial set X.

Equations

• X.functorN'Iso = CategoryTheory.NatIso.ofComponents (fun (x : X.N) => SSet.Nonsingular.iso x.simplex ⋯) ⋯

noncomputable def SSet.coconeN' (X : SSet) [X.Nonsingular] : CategoryTheory.Limits.Cocone X.functorN'

If X is a nonsingular simplicial set, this is the cocone consisting of the (mono)morphisms Δ[x.dim] ⟶ X for all nondegenerate simplices x : X.N.

Equations

• X.coconeN' = { pt := X, ι := { app := fun (s : X.N) => SSet.yonedaEquiv.symm s.simplex, naturality := ⋯ } }

@[simp]

theorem SSet.coconeN'_ι_app (X : SSet) [X.Nonsingular] (s : X.N) : X.coconeN'.ι.app s = yonedaEquiv.symm s.simplex

@[simp]

theorem SSet.coconeN'_pt (X : SSet) [X.Nonsingular] : X.coconeN'.pt = X

noncomputable def SSet.isColimitCoconeN' (X : SSet) [X.Nonsingular] : CategoryTheory.Limits.IsColimit X.coconeN'

If X is a nonsingular simplicial set, X is the colimit of Δ[x.dim] for all nondegenerate simplices x : X.N.

Equations

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