feat(AlgebraicTopology/SimplicialSet): single-cell boundary and horn attachments

[jcreinhold]

Introduces single-cell pushouts for attachments to a subcomplex of a simplicial set: one for attaching a nondegenerate simplex along its boundary, one for a horn-filling monic σ : Δ[n+1] ⟶ X. Skeleton.relativeCellComplexOfMono already presents every monomorphism as a relative cell complex by attaching all nondegenerate cells at each dimension simultaneously; the new lemmas are the per-cell version, and apply against arbitrary base subcomplexes (not only skeletonOfMono).

Added three files under Mathlib/AlgebraicTopology/SimplicialSet/:

• SubcomplexAttach.lean builds the abstract attachment-as-pushout machinery. The image–preimage square in X.Subcomplex is bicartesian and is a pushout in SSet; specializing to a chosen preimage A.preimage σ = K defines the attaching map K ⟶ A, and the resulting square is a pushout whenever σ is injective off K at every dimension. The hypothesis stops short of Mono σ, so it covers nondegenerate single-simplex maps, which are not monic.
• BoundaryAttach.lean specializes to single-cell boundary attachment: for a nondegenerate x ∉ A whose boundary lies in A, the square ∂Δ[n] → A, Δ[n] → A ⊔ ofSimplex x is a pushout. The injectivity input comes from an Eilenberg–Zilber argument.
• HornAttach.lean does the same for horns: for a monic σ : Δ[n+1] ⟶ X with A.preimage σ = Λ[n+1, i], the analogous square is a pushout.

These pushouts are the per-step input for cell-by-cell filtrations in arbitrary bases.

Examples that can use this directly (follow-on PRs):

• the saturated closure of {∂Δ[n] ↪ Δ[n]} recovering all monomorphisms (Joyal–Tierney, Quasi-Categories vs Segal Spaces, Proposition 1.2; Riehl–Verity Remark 1.1.27);
• pairing-driven inner-anodyne presentations of the Joyal model structure (Moss, Another Approach to the Kan–Quillen Model Structure);
• marked-simplicial and complicial cell technology (Riehl–Verity Appendix D).

References:

• Riehl–Verity, Elements of ∞-Category Theory.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary d9874e4268

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexAttach (new file)	895
Mathlib.AlgebraicTopology.SimplicialSet.BoundaryAttach (new file)	930
Mathlib.AlgebraicTopology.SimplicialSet.HornAttach (new file)	931

---

Declarations diff

+ applies
+ attachingMap
+ attachingMap_comp_homOfLE
+ attachingMap_isPullback_app
+ attachingMap_isPushout_of_injOn_compl
+ attachingMap_ι
+ boundaryAttach_isPushout_of_nonDegenerate
+ hornAttach_isPushout_of_mono
+ imagePreimageBicartSq
+ imagePreimage_isPushout
+ injOn_compl_boundary_yonedaEquiv_symm
+ injOn_compl_horn_of_mono
+ mem_range_ι_app
+ preimage_eq_horn_of_face_image_le_of_omitted_not_le
+ preimage_eq_horn_of_face_le_of_omitted_not_le
+ preimage_yonedaEquiv_symm_eq_boundary
+ range_app_union_range_app

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mckoen]

I don't see how Proposition 1.1.29 has any relevance here. I mention this because I am explicitly working on formalizing this proposition 😁

[mckoen]

Thanks for the PR! Was any of this generated by a LLM? If so, you might consider adding the LLM-generated label