feat(AlgebraicTopology): filtration of Δ[p] ⊗ Δ[1]

[joelriou]

Previously, we defined an enumeration of the non-degenerate p + 1-dimensional simplices of Δ[p] ⊗ Δ[1]. They "cover" Δ[p] ⊗ Δ[1], and we use the enumeration to define a filtration of Δ[p] ⊗ Δ[1] by subcomplexes.
In a future PR, it will be used in order to define a constructor for morphisms from Δ[p] ⊗ Δ[1] which shall take as inputs a morphism on each of these p + 1-simplices, with a compatibility condition on the intersection of two consecutive simplices in the enumeration.

From https://github.com/joelriou/topcat-model-category

---

• depends on: feat(AlgebraicTopology): non-degenerate simplices in Δ[p] ⊗ Δ[q] #41624
• depends on: feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone #41617

[github-actions]

PR summary da98e621b1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
20 files Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.Topology.Homotopy.TopCat.ToSSet	2
Mathlib.Order.Fin.InsertNth (new file)	367
Mathlib.Order.Fin.Prod (new file)	386

---

Declarations diff (regex)

+ codimOneSimplex
+ exists_nonDegenerate_max_dim
+ exists_nonDegenerate_max_dim_aux
+ filtration
+ filtration_last
+ filtration_monotone
+ filtration_zero
+ insertNth_last_monotone
+ insertNth_monotone
+ insertNth_zero_monotone
+ intersectionNondeg
+ mem_ofSimplex_obj_iff
+ nonDegenerateEquiv
+ nonDegenerateEquiv_fst
+ nonDegenerateEquiv_snd
+ nonDegenerate_of_app_apply
+ objEquiv_apply_symm_apply
+ ofSimplex_le_filtration
+ prodStdSimplex.nonDegenerateEquiv₁
+ prodStdSimplex.nonDegenerateEquiv₁_fst
+ prodStdSimplex.nonDegenerateEquiv₂_snd
+ prod_exists_lt_lt_of_le_of_le
+ prod_lt_last_last_iff
+ prod_zero_zero_lt_iff
+ strictMono_insertNth
+ strictMono_insertNth_last
+ strictMono_insertNth_zero
+ subcomplex_eq_top_iff
+ δ_castSucc_nonDegenerateEquiv
+ δ_succ_nonDegenerateEquiv
- instance : Category (CosimplicialObject C) := by
- nonDegenerateEquiv₁
- nonDegenerateEquiv₁_fst
- nonDegenerateEquiv₁_snd

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit da98e62).

• +29 new declarations
• −4 removed declarations

-CategoryTheory.CosimplicialObject.comp_app
-CategoryTheory.CosimplicialObject.id_app
-CategoryTheory.CosimplicialObject.instCategory
+Fin.insertNth_last_monotone
+Fin.insertNth_monotone
+Fin.insertNth_zero_monotone
+Fin.prod_exists_lt_lt_of_le_of_le
+Fin.prod_lt_last_last_iff
+Fin.prod_zero_zero_lt_iff
+Fin.strictMono_insertNth
+Fin.strictMono_insertNth_last
+Fin.strictMono_insertNth_zero
+SSet.nonDegenerate_of_app_apply
+SSet.prodStdSimplex.exists_nonDegenerate_max_dim
-SSet.prodStdSimplex.nonDegenerateEquiv₁_snd
+SSet.prodStdSimplex.nonDegenerateEquiv₂_snd
+SSet.prodStdSimplex.objEquiv_apply_symm_apply
+SSet.prodStdSimplex.subcomplex_eq_top_iff
+SSet.prodStdSimplex₁.codimOneSimplex
+SSet.prodStdSimplex₁.codimOneSimplex_coe_fst
+SSet.prodStdSimplex₁.codimOneSimplex_coe_snd
+SSet.prodStdSimplex₁.filtration
+SSet.prodStdSimplex₁.filtration_last
+SSet.prodStdSimplex₁.filtration_monotone
+SSet.prodStdSimplex₁.filtration_zero
+SSet.prodStdSimplex₁.intersectionNondeg
+SSet.prodStdSimplex₁.nonDegenerateEquiv
+SSet.prodStdSimplex₁.nonDegenerateEquiv_fst
+SSet.prodStdSimplex₁.nonDegenerateEquiv_snd
+SSet.prodStdSimplex₁.ofSimplex_le_filtration
+SSet.prodStdSimplex₁.δ_castSucc_nonDegenerateEquiv
+SSet.prodStdSimplex₁.δ_succ_nonDegenerateEquiv
+SSet.stdSimplex.mem_ofSimplex_obj_iff

---

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

Current number	Change	Type (strong)
4529	3	backward.defeqAttrib.useBackward

No changes to weak technical debt.

Current commit da98e621b1
Reference commit c368140668

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology): non-degenerate simplices in Δ[p] ⊗ Δ[q] #41624
• feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone #41617
  By Dependent Issues (🤖). Happy coding!