feat(AlgebraicTopology): inductive definition of StrictSegal

[gio256]

We provide alternative definitions of SSet.StrictSegal and SSet.Truncated.StrictSegal for comparison with #20668.

Note that the errors in SimplicialSet/Coskeletal.lean (which I have yet to address) are a result of the fact that SSet.StrictSegal no longer defines an inverse to spine X for paths of length zero. This is not a fundamental limitation of the approach here, but the inductive definition does make it more difficult to gloss over the fact that Path₁ is not defined for 0-truncated simplicial sets.

---

[github-actions]

PR summary 8262d3236e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.Path	843	844	+1 (+0.12%)
Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal	849	850	+1 (+0.12%)
Mathlib.AlgebraicTopology.Quasicategory.StrictSegal	852	853	+1 (+0.12%)

Import changes for all files

Files

Import difference

50 files Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplexCategory Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution

1

---

Declarations diff

+ CategoryTheory.Nerve.strictSegal
+ Hom.tr
+ Hom.tr_comp
+ Meta.subscript
+ Path₁
+ hasColimits
+ hasLimits
+ hom_ext
+ incl
+ incl_comp_inclusion
+ instance (C : Type u) [Category.{v} C] :
+ largeCategory
+ spineEquiv_coe_fn
+ spineEquiv_symm_coe_fn
+ spineToDiagonal_def
+ spine_arrow
+ spine_vertex
+ trunc_eq
+ trunc_self
+ trunc_spine
+ truncation_spine
+ uliftFunctor
++ map_arrow
++ map_vertex
++ spineToSimplex
++ spineToSimplex_spine
++ spineToSimplex_spine_apply
++ spine_spineToSimplex
++ spine_spineToSimplex_apply
+++ delabMkNotation
+++ ext'
+++ interval
+++ map
+++ truncation_comp_trunc
++++ trunc
+++- map_interval
++- Path
++- spine
++- spineInjective
++- spineToSimplex_arrow
++- spine_map_subinterval
+-+ StrictSegal
+-+ spineEquiv
+-+ spineToDiagonal
+-+ spine_map_vertex
- Path.ext'
- Path.interval
- Path.map
- Truncated.hasColimits
- Truncated.hasLimits
- Truncated.hom_ext
- Truncated.largeCategory
- Truncated.uliftFunctor
- spineToSimplex_map
- strictSegal
-++ spineToSimplex_edge
-++ spineToSimplex_interval
-++ spineToSimplex_vertex
-++ spine_δ_arrow_eq
-++ spine_δ_arrow_gt
-++ spine_δ_arrow_lt
-++ spine_δ_vertex_ge
-++ spine_δ_vertex_lt

You can run this locally as follows

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

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

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

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
1416	-1	erw

Current commit 8262d3236e
Reference commit 773fd70b27

You can run this locally as

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