Commit 2025-11-26 09:48 b815664c

View on Github →

feat(AlgebraicTopology): edges and "triangles" in the nerve of a category (#31274) We study Edge and Edge.CompStruct in the case of the nerve of a category. In particular, Edge.CompStruct are related to commutative triangles.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialNerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/CompStruct.lean

added theorem SSet.Edge.CompStruct.d₀

added theorem SSet.Edge.CompStruct.d₁

added theorem SSet.Edge.CompStruct.d₂

modified def SSet.Edge.CompStruct.simplex

added theorem SSet.Edge.map_edge

modified def SSet.Edge.mk'

added def SSet.Edge.mk

added theorem SSet.Edge.mk_edge

Modified Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

added def CategoryTheory.nerve.edgeMk

added theorem CategoryTheory.nerve.edgeMk_edge

added theorem CategoryTheory.nerve.edgeMk_surjective

added def CategoryTheory.nerve.homEquiv

added theorem CategoryTheory.nerve.homEquiv_comp

added theorem CategoryTheory.nerve.homEquiv_edgeMk

added theorem CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap

added theorem CategoryTheory.nerve.homEquiv_id

added theorem CategoryTheory.nerve.left_edge

added theorem CategoryTheory.nerve.mk₁_homEquiv_apply

added theorem CategoryTheory.nerve.nonempty_compStruct_iff

added theorem CategoryTheory.nerve.right_edge

modified theorem CategoryTheory.nerve.δ_obj

modified theorem CategoryTheory.nerve.δ₀_eq

added theorem CategoryTheory.nerve.δ₂_two

added theorem CategoryTheory.nerve.δ₂_zero

modified theorem CategoryTheory.nerve.σ_obj

added theorem CategoryTheory.nerve.σ_zero_nerveEquiv_symm

modified def CategoryTheory.nerveEquiv

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

Modified Mathlib/CategoryTheory/ComposableArrows/Basic.lean

added theorem CategoryTheory.ComposableArrows.ext₂_of_arrow

added theorem CategoryTheory.ComposableArrows.mk₁_comp_eqToHom

added theorem CategoryTheory.ComposableArrows.mk₁_eqToHom_comp

added theorem CategoryTheory.ComposableArrows.mk₁_hom