feat(AlgebraicTopology/SimplicialSet): exists_isPushout_of_ne_top

[jcreinhold]

Every proper subcomplex of a simplicial set extends by attaching a single cell along its boundary, exhibited as a pushout of ∂Δ[n] ↪ Δ[n]. This is the per-cell input for cell-by-cell filtrations of monomorphisms in SSet.

Adapted from @joelriou 's proof. I also added the supporting lemma Types.isPullback_of_eq_setPreimage (set-preimage square is a pullback in Type u).

AI use: Claude helped locate subtype_val_mono and the backward.isDefEq.respectTransparency option.

[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 c7129933ee

Import changes exceeding 2%

%	File
+4.60%	Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	914	956	+42 (+4.60%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic	1
Mathlib.AlgebraicTopology.SimplicialSet.Skeleton	14
Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory	15
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct	19
5 files Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.KanComplex	31
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	42

---

Declarations diff

+ exists_isPushout_of_ne_top
+ isPullback_of_eq_setPreimage
+ preimage_yonedaEquivSymm_eq_boundary

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.

---

Increase in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
5844	2	backward.isDefEq.respectTransparency

Current commit 4d4767932f
Reference commit c7129933ee

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]

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

[jcreinhold]

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

Cut the PR down to just the adaptation of @joelriou 's proof. None of this code is LLM generated, albeit I used an LLM to look through mathlib4 for existing relevant structures finding subtype_val_mono and for info on what backward.isDefEq.respectTransparency does exactly (added this to the PR description).

I made a few contributions last year, so I didn't re-read the contribution guide and see the (new?) section on AI/LLM use.

Happy to close this if I broke the intended conduct guidelines. Not my intent to waste any maintainer's time.

[jcreinhold]

On the large-import flag. I think this is because of the import Mathlib.CategoryTheory.Subobject.Types for subtype_val_mono.

Four options I see:

1. leave it and ignore the flag
2. inline the proof (for both haveI cases)
3. take another route shown here (arguably less clear, but it's a judgement call).
4. Move subtype_val_mono to CategoryTheory.Types.Basic, alongside the other monomorphism-related theorems (which seems appropriate long-term IMO), and delete the import (then it's reached through Limits.Types.Pushouts without importing the other unrelated machinery).

Perhaps there's another way I'm not seeing?