feat(AlgebraicTopology/SimplicialSet): anodyne extensions

[joelriou]

---

• depends on: feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing #28462

[github-actions]

PR summary e40140d761

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation (new file)	886
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (new file)	1058
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (new file)	1209

---

Declarations diff

+ Cells
+ Cells.mapHorn
+ Cells.mapHorn_ι
+ Cells.mapToSucc
+ Cells.mapToSucc_ι
+ Cells.preimage_filtration_map
+ Cells.subcomplex_not_le_filtration
+ Cells.type₁
+ Cells.type₂
+ Cells.ιSigmaHorn
+ Cells.ιSigmaStdSimplex
+ Cells.ι_b
+ Cells.ι_m
+ Cells.ι_t
+ Subcomplex.Pairing.anodyneExtensions
+ Subcomplex.Pairing.strongAnodyneExtensions
+ anodyneExtensions
+ anodyneExtensions.horn_ι
+ anodyneExtensions.of_isIso
+ anodyneExtensions_eq_llp_rlp
+ anodyneExtensions_eq_retracts_transfiniteCompositions
+ anodyneExtensions_eq_retracts_transfiniteCompositionsOfShape
+ b
+ basicCell
+ bijective_image_objEquiv_toOrderHom_univ
+ cases
+ dim
+ dim_toN_le
+ eq_iff_ofSimplex_eq
+ eq_iff_sMk_eq
+ evaluation
+ existsN
+ existsUnique_toNπ
+ exists_or_of_range_m_N
+ ext
+ face_bot
+ face_le_horn_iff
+ face_nonDegenerateEquiv'
+ face_univ
+ filtration
+ filtration_bot
+ filtration_monotone
+ filtration_of_isSuccLimit
+ filtration_succ
+ hasDimensionLT_face
+ horn
+ horn_obj_eq_top
+ iSup_filtration
+ iSup_filtration_iio
+ image_face_index_compl
+ image_horn_lt_subcomplex
+ index
+ induction
+ instance (j : ι) : Mono (f.m j)
+ instance (n : ℕ) : MorphismProperty.IsSmall.{u}
+ instance (x : X.S) : Epi x.toNπ := (existsUnique_toNπ rfl).exists.choose_spec.1
+ instance : HasSmallObjectArgument.{u} modelCategoryQuillen.J.{u}
+ instance : IsCardinalForSmallObjectArgument modelCategoryQuillen.J.{u} Cardinal.aleph0.{u}
+ instance : IsStableUnderCoproducts.{w} T.llp
+ instance : MorphismProperty.IsSmall.{u} modelCategoryQuillen.J.{u}
+ instance : MorphismProperty.IsStableUnderTransfiniteComposition.{w} W.llp
+ instance : f.filtration_monotone.functor.IsWellOrderContinuous
+ instance {J : Type*} [Category J] {X : SSet.{u}} [IsFilteredOrEmpty J] :
+ instance {j : ι} (c : f.Cells j) :
+ instance {n : ℕ} (i : Fin (n + 1)) : HasDimensionLT (horn.{u} n i) n := by
+ instance {n : ℕ} : HasDimensionLT (boundary n) n := by
+ isPullback
+ isPushout
+ isPushout_aux₁
+ isPushout_aux₂
+ isPushout_aux₃
+ isSmall_iSup
+ le_filtration
+ llp_rlp_of_isCardinalForSmallObjectArgument_aleph0
+ lt
+ m
+ map
+ mapN
+ mapN_type₁
+ mapN_type₂
+ map_app_objEquiv_symm_δ_index
+ map_objEquiv_op_apply
+ map_toNπ_op_apply
+ mem_horn_iff
+ nonDegenerateEquiv'
+ nonDegenerateEquiv'_iff
+ nonDegenerateEquiv'_symm_apply_mem
+ nonDegenerateEquiv'_symm_mem_iff_face_le
+ objEquiv_symm_notMem_horn_of_isIso
+ objEquiv_symm_δ_mem_horn_iff
+ objEquiv_symm_δ_notMem_horn_iff
+ ofSimplex_eq_subcomplex_mk
+ ofSimplex_map
+ orderBotAleph0OrdToType
+ orderIsoOfNonDegenerate
+ preimage_comp
+ preimage_ι
+ range_homOfLE_app_union_range_b_app
+ range_map
+ range_succAboveOrderEmb
+ relativeCellComplex
+ sigmaHorn
+ sigmaStdSimplex
+ strongAnodyneExtensions
+ strongAnodyneExtensions_le_anodyneExtensions
+ strongAnodyneExtensions_ι_iff
+ subcomplex_cast
+ subcomplex_eq_of_epi
+ subcomplex_le_filtration
+ subcomplex_le_horn_iff
+ subcomplex_le_iff
+ subcomplex_not_le_image_horn
+ t
+ toNπ
+ unique
+ univ_neq_empty
+ w
+ yonedaEquiv_symm_app_id
+ ιSigmaHorn_jointly_surjective
+ ιSigmaStdSimplex_eq_iff
+ ιSigmaStdSimplex_jointly_surjective
++ inj_apply_eq_iff_of_isColimit
++ le
++ lt_iff

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

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

Current number	Change	Type
7448	14	backward.isDefEq

Current commit 14dbc638c6
Reference commit e40140d761

You can run this locally as

./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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing #28462
  By Dependent Issues (🤖). Happy coding!