Commit 2024-12-12 11:32 415efa61

View on Github →

feat(AlgebraicTopology): define the simplicial nerve of a simplicial category (#19837) This PR defines the simplicial (/homotopy coherent) nerve of a simplicial category.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialNerve.lean

added theorem CategoryTheory.SimplicialThickening.Path.le

added structure CategoryTheory.SimplicialThickening.Path

added theorem CategoryTheory.SimplicialThickening.SimplicialCategory.assoc

added theorem CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id

added theorem CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp

added def CategoryTheory.SimplicialThickening.compFunctor

added theorem CategoryTheory.SimplicialThickening.functor_comp

added theorem CategoryTheory.SimplicialThickening.functor_id

added theorem CategoryTheory.SimplicialThickening.hom_ext

added def CategoryTheory.SimplicialThickening.orderHom

added def CategoryTheory.SimplicialThickening

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

added theorem SSet.comp_app

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

added def CategoryTheory.nerveEquiv

added def CategoryTheory.nerveMap

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

added theorem CategoryTheory.EnrichedFunctor.ext

Modified Mathlib/Order/Hom/Basic.lean

added def OrderHom.uliftMap

Modified docs/references.bib