Commit 2024-12-04 20:12 fa8f1757

View on Github →

feat(AlgebraicTopology/SimplicialSet): StrictSegal simplicial sets are 2-coskeletal (#19057) We prove that if X is a simplicial set that is StrictSegal then X is 2-coskeletal, meaning (coskAdj 2).unit.app X defines an isomorphism StrictSegal.cosk2Iso : X ≅ (Truncated.cosk 2).obj ((truncation 2).obj X). This is proven by demonstrating that (rightExtensionInclusion X n).IsPointwiseRightKanExtension holds. Co-Authored-By: Mario Carneiro and Joël Riou

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

added theorem SimplexCategory.mkOfLe_refl

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

added def CategoryTheory.Nerve.nerveFunctor₂

added theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁

added theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂

added theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃

added theorem SSet.StrictSegal.isRightKanExtension

added def SSet.Truncated.rightExtensionInclusion

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

modified def CategoryTheory.nerveFunctor

Modified Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

added theorem SSet.spine_map_vertex

Modified Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean