The subdivision functors

In this file, we define the subdivision functor sd : SSet ⥤ SSet and its right adjoint ex.

TODO (@joelriou)

• define another functor SSet.B : SSet ⥤ SSet by sending X to the nerve of the partially ordered type X.N of nondegenerate simplices in X, define a natural transformation sd ⟶ B, and show that on suitable simplicial sets X, this natural transformation is an isomorphism.

References

• J. F. Jardine, Simplicial approximation

noncomputable def SimplexCategory.sd : CategoryTheory.Functor SimplexCategory SSet

The functor SimplexCategory ⥤ SSet which sends ⦋n⦌ to the nerve of the partially ordered type of nonempty finite chains in {0, ..., n} (ulifted to Type u). Vertices in SimplexCategory.sd.obj ⦋n⦌ identify to nonempty subsets of {0, ..., n}.

Equations

• SimplexCategory.sd = SimplexCategory.toPartOrd.comp (PartOrd.nonemptyFiniteChainsFunctor.comp PartOrd.nerveFunctor)

noncomputable def SSet.sd : CategoryTheory.Functor SSet SSet

The subdivision functor on simplicial sets.

Equations

• SSet.sd = CategoryTheory.Functor.leftKanExtension SSet.stdSimplex SimplexCategory.sd

noncomputable def SSet.ex : CategoryTheory.Functor SSet SSet

The right adjoint to the subdivision functor on simplicial sets.

Equations

• SSet.ex = CategoryTheory.Presheaf.restrictedULiftYoneda SimplexCategory.sd

noncomputable def SSet.sdExAdjunction : sd ⊣ ex

The adjunction between the subdivision functor sd and ex.

Equations

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

instance SSet.instIsLeftAdjointSd : sd.IsLeftAdjoint

instance SSet.instIsRightAdjointEx : ex.IsRightAdjoint

noncomputable def SSet.stdSimplex.sdIso : CategoryTheory.Functor.comp stdSimplex sd ≅ SimplexCategory.sd

The natural isomorphism stdSimplex ⋙ sd ≅ SimplexCategory.sd.

Equations

• SSet.stdSimplex.sdIso = CategoryTheory.Presheaf.isExtensionAlongULiftYoneda SimplexCategory.sd

instance SSet.instIsLeftKanExtensionSimplexCategorySdInvFunctorSdIso : sd.IsLeftKanExtension stdSimplex.sdIso.inv