Commit 2025-02-08 20:13 573d586b

View on Github →

feat(AlgebraicTopology): notations X _⦋n⦌ and X ^⦋n⦌ for (co)simplicial objects (#21581) We change the notation for the n-th term of a simplicial object X from X _[n] to X _⦋n⦌. We also change the notation for the n-th term of a cosimplicial object X from X ^[n] to X ^⦋n⦌. This change makes the notations for (co)simplicial objects consistent with the notation for objects of the simplex category, which was updated in #21565.

Estimated changes

modified theorem SSet.δ_comp_δ_apply
modified theorem SSet.δ_comp_δ_self_apply
modified theorem SSet.δ_comp_σ_self_apply
modified theorem SSet.δ_comp_σ_succ'_apply
modified theorem SSet.δ_comp_σ_succ_apply
modified theorem SSet.δ_naturality_apply
modified theorem SSet.σ_comp_σ_apply
modified theorem SSet.σ_naturality_apply
modified def SSet.OneTruncation₂
modified theorem SSet.Truncated.HoRel₂.mk'
modified def SSet.Truncated.ev0₂
modified def SSet.Truncated.ev1₂
modified def SSet.Truncated.ev2₂
modified def SSet.horn.edge
modified def SSet.horn.face
modified def SSet.unitHomEquiv
modified def SSet.spine
modified theorem SSet.spine_map_subinterval
modified theorem SSet.spine_map_vertex
modified def SSet.stdSimplex.edge
modified def SSet.stdSimplex.id