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

This PR gives one of the main results in the combinatorial approach to (strong) anodyne extensions by Sean Moss,  *Another approach to the Kan-Quillen model structure*.
For a suitable combinatorial data for a subcomplex `A` of a simplicial set `X` (a proper pairing `P` of `A`), it was previously shown that if the ancestrality relation for this pairing `P` is well founded, then there exists a rank function for the pairing #28351. In this PR, we assume that we have such a rank function, and we show that the inclusion of `A` in `X` is a relative cell complex w.r.t. horn inclusions, i.e. it is a transfinite composition of pushouts of coproducts of horn inclusions. The API allows to keep track of which horns were used, so that this theory can be used in order to study anodyne extensions #37321 as well as inner anodyne extensions #37869. In future PRs, pairings for specific subcomplexes of certain simplicial sets shall be constructed, and this will allow the study of stabiliity properties of anodyne extensions (with respect to binary products and with respect to the subdivision functor), and by adjunction, we shall be able to deduce results regarding Kan fibrations of simplicial sets.

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

Author: joelriou

Mathlib.lean

@@ -1514,6 +1514,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.Basic
 public import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
 public import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

@@ -87,6 +87,21 @@ lemma δ_eq_iff (i : Fin (d + 2)) :
   ⟨fun h ↦ (hxy.existsUnique_δ_cast_simplex hd).unique h (hxy.δ_index hd),
     by rintro rfl; apply δ_index⟩
 
+include hxy in
+lemma le : x ≤ y := by
+  have := hxy.δ_index rfl
+  simp only [cast_simplex_rfl] at this
+  rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff,
+    ← this]
+  exact ⟨(SimplexCategory.δ _).op, rfl⟩
+
+include hxy in
+lemma unique (f : ⦋d⦌ ⟶ ⦋d + 1⦌) [Mono f]
+    (hf : X.map f.op (y.cast (by rw [hxy.dim_eq, hd])).simplex = (x.cast hd).simplex) :
+    f = SimplexCategory.δ (hxy.index hd) :=
+  (hxy.cast hd).2.unique ⟨by dsimp; infer_instance, hf⟩
+    ⟨by dsimp; infer_instance, hxy.δ_index hd⟩
+
 end
 
 include hxy in

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean

@@ -134,6 +134,14 @@ lemma ne (x : P.I) (y : P.II) :
   have : x ∈ P.I ∩ P.II := ⟨hx, hy⟩
   simp [P.inter] at this
 
+lemma le [P.IsProper] (x : P.II) :
+    x.1 ≤ (P.p x).1 :=
+  (P.isUniquelyCodimOneFace x).le
+
+lemma lt [P.IsProper] (x : P.II) :
+    x.1 < (P.p x).1 :=
+  lt_of_le_of_ne' (P.le x) (P.ne _ _)
+
 variable {Y : SSet.{u}} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
 
 /-- Given an isomorphism `Y ≅ X` of simplicial sets, a pairing `P` of a subcomplex