feat(AlgebraicTopology): pushout diagrams in the filtration of Δ[p] ⊗ Δ[1]

[joelriou]

---

• depends on: feat(AlgebraicTopology): order relation between simplices of the nerve of a partial order #41656
• depends on: feat(AlgebraicTopology): filtration of Δ[p] ⊗ Δ[1] #41655
• 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 e3589cce46

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne	997	1000	+3 (+0.30%)
Mathlib.AlgebraicTopology.SimplicialSet.Homotopy	1000	1003	+3 (+0.30%)

Import changes for all files

Files	Import difference
14 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.NonsingularColimit Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex	2
6 files Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.Topology.Homotopy.TopCat.ToSSet	3
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.bicartSq
+ filtration.isPushout
+ filtration.ι
+ filtration.ι_ι
+ filtration_last
+ filtration_monotone
+ filtration_zero
+ hom_ext
+ image_le_image_iff
+ insertNth_last_monotone
+ insertNth_monotone
+ insertNth_zero_monotone
+ intersectionNondeg
+ intersectionNondeg_le_intersectionNondeg
+ intersectionNondeg_le_intersectionNondeg'
+ isoNerve_hom_app_obj
+ isoOfRepresentableBy_ofSimplexRepresentableBy_hom
+ mem_range_objEquiv_nonDegenerateEquiv₀_iff
+ mem_range_objEquiv_nonDegenerateEquiv₁_iff
+ nerve_ofSimplex_le_ofSimplex_iff
+ nonDegenerateEquiv
+ nonDegenerateEquiv_fst
+ nonDegenerateEquiv_snd
+ nonDegenerate_of_app_apply
+ objEquiv_apply_symm_apply
+ objEquiv_symm_δ_apply
+ objEquiv_symm_σ_apply
+ ofSimplexRepresentableBy
+ ofSimplexRepresentableBy_id
+ ofSimplex_codimOneSimplex
+ ofSimplex_le_filtration
+ ofSimplex_le_ofSimplex_iff
+ preimage_image
+ preimage_monotone
+ 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
+ range_isoNerve_hom_app_obj
+ strictMono_insertNth
+ strictMono_insertNth_last
+ strictMono_insertNth_zero
+ subcomplex_eq_top_iff
+ toOfSimplex_app_objEquiv_symm
+ yonedaEquiv_isoOfRepresentableBy_hom
+ yonedaEquiv_isoOfRepresentableBy_ofSimplexRepresentableBy_hom
+ yonedaEquiv_symm_comp
+ yonedaEquiv_symm_map
+ δ_castSucc_nonDegenerateEquiv
+ δ_succ_nonDegenerateEquiv
++ mem_ofSimplex_obj_iff
- _root_.SSet.yonedaEquiv_symm_comp
- 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 -- pending)

Computed after the build finishes.

---

Increase in strong tech debt: (relative, absolute) = (4.55, 0.01)

Current number	Change	Type (strong)
502	4	erw
4536	10	backward.defeqAttrib.useBackward
5624	4	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit e3589cce46
Reference commit 5e1cacbae2

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): order relation between simplices of the nerve of a partial order #41656
• feat(AlgebraicTopology): filtration of Δ[p] ⊗ Δ[1] #41655
• 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!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.