Commit 2025-11-17 08:49 4c16d406

View on Github →

feat(AlgebraicTopology): inductive construction of StrictSegal structures (#31250) We obtain a computable StrictSegal (nerve C) structure by using an inductive construction based on a new StrictSegalCore structure which provides a way to construct a n + 1-simplex by from a 1-simplex and a n-simplex satisfying a compatibility.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

added theorem SSet.Path.arrow_interval

added theorem SSet.Path.congr_arrow

added theorem SSet.Path.congr_vertex

added theorem SSet.Path.ext₀

modified def SSet.Path.interval

added theorem SSet.spine_δ₀

Modified Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

added def CategoryTheory.Nerve.strictSegal

added def SSet.StrictSegal.ofCore

deleted def SSet.StrictSegal.truncation

added theorem SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex

added def SSet.StrictSegalCore.spineToSimplex

added def SSet.StrictSegalCore.spineToSimplexAux

added theorem SSet.StrictSegalCore.spineToSimplex_spine

added theorem SSet.StrictSegalCore.spineToSimplex_succ

added theorem SSet.StrictSegalCore.spineToSimplex_zero

added theorem SSet.StrictSegalCore.spine_spineToSimplex

added theorem SSet.StrictSegalCore.δ₀_spineToSimplex

added structure SSet.StrictSegalCore

added theorem SSet.Truncated.IsStrictSegal.ext

added theorem SSet.Truncated.IsStrictSegal.hom_ext

added theorem SSet.Truncated.spine_injective

added theorem SSet.Truncated.spine_surjective

Modified Mathlib/CategoryTheory/ComposableArrows/Basic.lean

added def CategoryTheory.ComposableArrows.arrowEquiv