Commit 2025-09-09 19:57 f70fb8ef

View on Github →

feat(AlgebraicTopology): nondegenerate simplices in the nerve of a partially ordered type (#28337) In this PR, we show that nondegenerate simplices in the nerve of a partially ordered type X correspond to strictly monotone functions Fin (n + 1) → X. (Incidentally, better normal formal are used for the RHS of lemmas involving (non)degenerate simplices of dimension 0.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialNerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean

modified theorem SSet.degenerate_zero

modified theorem SSet.nondegenerate_zero

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

added theorem CategoryTheory.nerve.ext_of_isThin

added theorem CategoryTheory.nerve.δ_obj

added theorem CategoryTheory.nerve.σ_obj

Created Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean

added theorem PartialOrder.mem_nerve_degenerate_of_eq

added theorem PartialOrder.mem_nerve_nonDegenerate_iff_injective

added theorem PartialOrder.mem_nerve_nonDegenerate_iff_strictMono

added theorem PartialOrder.mem_range_nerve_σ_iff