IndisputableMonolith.Foundation.SingularSubdivision

   1/-
   2Barycentric subdivision and (toward) the small-simplices theorem for
   3Mathlib's singular homology (Hatcher §2.1, proof of excision, pp. 119–124).
   4
   5## Design
   6
   7Everything possible is done on a purely combinatorial *affine chain* layer:
   8an affine `n`-simplex in a type `α` is a vertex tuple `Fin (n+1) → α`, and an
   9affine `n`-chain is a finitely supported `ℤ`-linear combination of tuples,
  10`AC α n := (Fin (n+1) → α) →₀ ℤ`.  Faces are tuple reindexings along
  11`Fin.succAbove`, the cone with apex `b` is `Fin.cons b`, and the barycentric
  12subdivision `asub` and the chain homotopy `atee` are defined by the classical
  13cone recursions
  14
  15  `S λ = b_λ · S (∂ λ)`,   `T λ = b_λ · (λ − T (∂ λ))`,
  16
  17parametrized by an *abstract* apex function `bary`.  All chain identities
  18(`∂∂ = 0`, the cone identity `∂(b·c) = c − b·∂c`, the chain-map property
  19`∂S = S∂`, the homotopy identity `∂T + T∂ = 1 − S`, and the telescoped
  20iterate identity for `S^k`) hold at this combinatorial level, for *any*
  21apex function (degree 0 needs only `bary 0 w = w 0`).
  22
  23The geometry (the honest barycenter on `stdSimplex`, the realization of a
  24vertex tuple as a continuous affine map, the diameter estimate) enters only
  25in the later stages, and the transport to Mathlib's singular chain complex
  26reuses the `Idx`/`gen`/`gen_d`/`gen_map` normal forms of
  27`IndisputableMonolith.Foundation.SingularPrism`.
  28
  29## Stages (each stage builds green before the next begins)
  30
  31* Stage 1: affine chains, boundary, cone, augmentation; generator normal
  32  forms.
  33* Stage 2: the chain identities: cone identity (positive degrees and
  34  degree 0), `∂∂ = 0`, `ε∂ = 0`.
  35* Stage 3: the barycentric subdivision operator `asub` and the chain-map
  36  property `∂S = S∂`.
  37* Stage 4: the chain homotopy `atee` with `∂T + T∂ = 1 − S`, and the
  38  telescoped homotopy for the iterate `S^k`.
  39* Stage 5a: pushforward `amap` of affine chains along a vertex map and
  40  equivariance of `abnd`/`acone`/`asub`/`atee` under barycenter-preserving
  41  maps.
  42* Stage 5b: geometry on `stdSimplex`: the affine realization `affineMap` of
  43  a vertex tuple, functoriality, vertices, faces, the identity tuple, the
  44  honest barycenter `sbary` and its equivariance `sbary_affineMap`.
  45* Stage 5c: transport to Mathlib's singular chain complex: the singular
  46  subdivision `sdOp X n : C_n(X) ⟶ C_n(X)` and homotopy
  47  `tOp X n : C_n(X) ⟶ C_{n+1}(X)`, the chain-map property `sdOp_comp_bnd`,
  48  the homotopy identities `tOp_chain_homotopy_succ`/`_zero`, naturality
  49  `sdOp_natural`/`tOp_natural`, and the iterates `sdOpIter`/`tOpIter` with
  50  `sdOpIter_comp_bnd` and `tOpIter_chain_homotopy_succ`/`_zero`.
  51* Stage 6: the diameter estimate: support tracking of `asub` through the
  52  cone recursion (`asub_support_bound`), the `n/(n+1)` contraction with the
  53  convex-hull maximum principle, iterates (`asubIter_support_bound`), and
  54  geometric decay (`exists_asubIter_small`).
  55* Stage 7: the small-simplices theorem `exists_sdOpIter_small`: for open
  56  `U ∪ V = X` and any singular simplex, some iterate of the singular
  57  subdivision has every piece landing in `U` or in `V` (Lebesgue number on
  58  the compact metric `Δⁿ`); combined with `gen_comp_sdOpIter` and the
  59  homotopy witness `tOpIter_chain_homotopy_succ`/`_zero`, this is the input
  60  the next layer needs for excision / Mayer-Vietoris.
  61
  62## Frontier (next layer)
  63
  64The two-set small-chains subcomplex `C^{U,V}_*(X)` (chains all of whose
  65generators are `U`-small or `V`-small) and the surjectivity of
  66`H_*(C^{U,V}) → H_*(C)` remain to be packaged: `exists_sdOpIter_small`
  67gives, for each cycle generator, an iterate `k` landing in the subcomplex,
  68and `tOpIter_chain_homotopy_*` gives the homology-class-preserving witness;
  69the remaining work is uniformizing `k` over the finitely many generators of
  70a chain (take the max) and assembling the subcomplex as a `ChainComplex`
  71with the inclusion map, feeding `SingularPair.lean`'s LES machinery toward
  72Mayer-Vietoris and excision.
  73-/
  74import Mathlib.AlgebraicTopology.SingularHomology.Basic
  75import Mathlib.Algebra.Category.ModuleCat.Colimits
  76import Mathlib.Algebra.Category.ModuleCat.Abelian
  77import Mathlib.Analysis.Normed.Module.Convex
  78import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  79import IndisputableMonolith.Foundation.SingularPrism
  80
  81namespace IndisputableMonolith
  82namespace Foundation
  83namespace SingularSubdivision
  84
  85open CategoryTheory Limits AlgebraicTopology Simplicial Opposite
  86
  87/-! ## Stage 1: affine chains, boundary, cone, augmentation -/
  88
  89variable {α β : Type} {n : ℕ}
  90
  91/-- The group of affine `n`-chains in `α`: finitely supported `ℤ`-linear
  92combinations of vertex tuples `Fin (n+1) → α`. -/
  93abbrev AC (α : Type) (n : ℕ) : Type := (Fin (n + 1) → α) →₀ ℤ
  94
  95/-- The affine simplex (generator) attached to a vertex tuple. -/
  96noncomputable def asimplex (w : Fin (n + 1) → α) : AC α n := Finsupp.single w 1
  97
  98/-- Extensionality for linear maps out of `AC α n`: it suffices to agree on
  99generators. -/
 100lemma AC.hom_ext {M : Type*} [AddCommGroup M] [Module ℤ M]
 101    {φ ψ : AC α n →ₗ[ℤ] M} (h : ∀ w, φ (asimplex w) = ψ (asimplex w)) :
 102    φ = ψ := by
 103  refine Finsupp.lhom_ext fun a b => ?_
 104  have hsingle : (Finsupp.single a b : AC α n) = b • asimplex a := by
 105    rw [asimplex, Finsupp.smul_single, smul_eq_mul, mul_one]
 106  rw [hsingle, LinearMap.map_smul, LinearMap.map_smul, h]
 107
 108/-- Evaluation of a `Finsupp.linearCombination`-defined map on a generator. -/
 109lemma lift_asimplex {M : Type*} [AddCommGroup M] [Module ℤ M]
 110    (f : (Fin (n + 1) → α) → M) (w : Fin (n + 1) → α) :
 111    Finsupp.linearCombination ℤ f (asimplex w) = f w := by
 112  rw [asimplex, Finsupp.linearCombination_single, one_smul]
 113
 114/-- The boundary of affine chains, `∂ : AC α (n+1) → AC α n`, the alternating
 115sum of the tuple faces `w ∘ Fin.succAbove i`. -/
 116noncomputable def abnd (n : ℕ) : AC α (n + 1) →ₗ[ℤ] AC α n :=
 117  Finsupp.linearCombination ℤ
 118    (fun w : Fin (n + 2) → α =>
 119      ∑ i : Fin (n + 2), (-1 : ℤ) ^ (i : ℕ) • asimplex (w ∘ i.succAbove))
 120
 121/-- The boundary of a generator is the alternating sum of its faces. -/
 122lemma abnd_asimplex (w : Fin (n + 2) → α) :
 123    abnd n (asimplex w) =
 124      ∑ i : Fin (n + 2), (-1 : ℤ) ^ (i : ℕ) • asimplex (w ∘ i.succAbove) :=
 125  lift_asimplex _ w
 126
 127/-- The cone with apex `b`, `AC α n → AC α (n+1)`: prepend `b` to every
 128vertex tuple. -/
 129noncomputable def acone (b : α) : AC α n →ₗ[ℤ] AC α (n + 1) :=
 130  Finsupp.lmapDomain ℤ ℤ (fun w => Fin.cons b w)
 131
 132/-- The cone of a generator. -/
 133lemma acone_asimplex (b : α) (w : Fin (n + 1) → α) :
 134    acone b (asimplex w) = asimplex (Fin.cons b w) := by
 135  rw [acone, asimplex, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, asimplex]
 136
 137/-- The augmentation `ε : AC α 0 → ℤ` (sum of coefficients). -/
 138noncomputable def eps (α : Type) : AC α 0 →ₗ[ℤ] ℤ :=
 139  Finsupp.linearCombination ℤ (fun _ : Fin 1 → α => (1 : ℤ))
 140
 141lemma eps_asimplex (w : Fin 1 → α) : eps α (asimplex w) = 1 :=
 142  lift_asimplex _ w
 143
 144/-! ### Tuple bookkeeping for cones and faces -/
 145
 146/-- The `0`-th face of a cone is the base tuple. -/
 147lemma cons_comp_succAbove_zero (b : α) (w : Fin (n + 1) → α) :
 148    (Fin.cons b w) ∘ (Fin.succAbove 0) = w := by
 149  funext k
 150  simp only [Function.comp_apply, Fin.zero_succAbove, Fin.cons_succ]
 151
 152/-- The `(j+1)`-th face of a cone is the cone on the `j`-th face. -/
 153lemma cons_comp_succAbove_succ (b : α) (w : Fin (n + 1) → α) (j : Fin (n + 1)) :
 154    (Fin.cons b w) ∘ (Fin.succAbove j.succ) = Fin.cons b (w ∘ j.succAbove) := by
 155  funext k
 156  induction k using Fin.cases with
 157  | zero => simp only [Function.comp_apply, Fin.succ_succAbove_zero, Fin.cons_zero]
 158  | succ k => simp only [Function.comp_apply, Fin.succ_succAbove_succ, Fin.cons_succ]
 159
 160/-! ## Stage 2: the chain identities -/
 161
 162/-- The cone identity in positive degrees: `∂ (b · c) = c − b · (∂ c)`
 163for `c : AC α (n+1)`. -/
 164theorem abnd_comp_acone (b : α) (n : ℕ) :
 165    (abnd (n + 1)).comp (acone b : AC α (n + 1) →ₗ[ℤ] AC α (n + 2)) =
 166      LinearMap.id - (acone b).comp (abnd n) := by
 167  refine AC.hom_ext fun w => ?_
 168  rw [LinearMap.comp_apply, acone_asimplex, abnd_asimplex, Fin.sum_univ_succ,
 169    LinearMap.sub_apply, LinearMap.id_apply, LinearMap.comp_apply, abnd_asimplex,
 170    map_sum, Fin.val_zero, pow_zero, one_smul, cons_comp_succAbove_zero,
 171    sub_eq_add_neg, ← Finset.sum_neg_distrib]
 172  congr 1
 173  refine Finset.sum_congr rfl fun j _ => ?_
 174  rw [map_smul, acone_asimplex, cons_comp_succAbove_succ, Fin.val_succ, pow_succ,
 175    mul_neg_one, neg_smul]
 176
 177/-- The cone identity in degree `0`:
 178`∂ (b · c) = c − ε(c) · [b]` for `c : AC α 0`. -/
 179theorem abnd_comp_acone_zero (b : α) :
 180    (abnd 0).comp (acone b : AC α 0 →ₗ[ℤ] AC α 1) =
 181      LinearMap.id -
 182        (LinearMap.toSpanSingleton ℤ (AC α 0) (asimplex fun _ => b)).comp (eps α) := by
 183  refine AC.hom_ext fun w => ?_
 184  rw [LinearMap.comp_apply, acone_asimplex, abnd_asimplex, Fin.sum_univ_two]
 185  rw [LinearMap.sub_apply, LinearMap.id_apply, LinearMap.comp_apply, eps_asimplex,
 186    LinearMap.toSpanSingleton_apply, one_smul]
 187  have h0 : (Fin.cons b w) ∘ (Fin.succAbove (0 : Fin 2)) = w :=
 188    cons_comp_succAbove_zero b w
 189  have h1 : (Fin.cons b w) ∘ (Fin.succAbove (1 : Fin 2)) = (fun _ => b) := by
 190    funext k
 191    have hk : k = 0 := Subsingleton.elim k 0
 192    subst hk
 193    simp only [Function.comp_apply]
 194    have h : (1 : Fin 2).succAbove (0 : Fin 1) = 0 := rfl
 195    rw [h, Fin.cons_zero]
 196  rw [h0, h1]
 197  simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul, neg_smul]
 198  rw [sub_eq_add_neg]
 199
 200/-- `∂∂ = 0` on affine chains. -/
 201theorem abnd_comp_abnd (n : ℕ) :
 202    (abnd n).comp (abnd (n + 1)) = (0 : AC α (n + 2) →ₗ[ℤ] AC α n) := by
 203  classical
 204  refine AC.hom_ext fun w => ?_
 205  rw [LinearMap.comp_apply, abnd_asimplex, map_sum, LinearMap.zero_apply]
 206  have hexp : ∀ i : Fin (n + 3),
 207      abnd n ((-1 : ℤ) ^ (i : ℕ) • asimplex (w ∘ i.succAbove)) =
 208        ∑ j : Fin (n + 2), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) •
 209          asimplex (w ∘ i.succAbove ∘ j.succAbove) := by
 210    intro i
 211    rw [map_smul, abnd_asimplex, Finset.smul_sum]
 212    refine Finset.sum_congr rfl fun j _ => ?_
 213    rw [smul_smul, ← pow_add]
 214    rfl
 215  simp only [hexp]
 216  rw [← Finset.sum_product', Finset.univ_product_univ]
 217  have hsplit := Finset.sum_filter_add_sum_filter_not
 218    (Finset.univ : Finset (Fin (n + 3) × Fin (n + 2)))
 219    (fun p => (p.2 : ℕ) < (p.1 : ℕ))
 220    (fun p => (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) •
 221      asimplex (w ∘ p.1.succAbove ∘ p.2.succAbove))
 222  rw [← hsplit]
 223  have hcancel : (∑ p ∈ Finset.univ.filter
 224        (fun p : Fin (n + 3) × Fin (n + 2) => (p.2 : ℕ) < (p.1 : ℕ)),
 225        (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) •
 226          asimplex (w ∘ p.1.succAbove ∘ p.2.succAbove)) =
 227      -∑ p ∈ Finset.univ.filter
 228        (fun p : Fin (n + 3) × Fin (n + 2) => ¬ (p.2 : ℕ) < (p.1 : ℕ)),
 229        (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) •
 230          asimplex (w ∘ p.1.succAbove ∘ p.2.succAbove) := by
 231    rw [← Finset.sum_neg_distrib]
 232    refine Finset.sum_bij'
 233      (i := fun p hp => ((⟨(p.2 : ℕ), by
 234          simp only [Finset.mem_filter_univ] at hp
 235          omega⟩ : Fin (n + 3)),
 236        (⟨(p.1 : ℕ) - 1, by
 237          have := p.1.isLt
 238          omega⟩ : Fin (n + 2))))
 239      (j := fun q hq => ((⟨(q.2 : ℕ) + 1, by
 240          have := q.2.isLt
 241          omega⟩ : Fin (n + 3)),
 242        (⟨(q.1 : ℕ), by
 243          simp only [Finset.mem_filter_univ] at hq
 244          have := q.2.isLt
 245          omega⟩ : Fin (n + 2))))
 246      ?_ ?_ ?_ ?_ ?_
 247    · intro p hp
 248      simp only [Finset.mem_filter_univ] at hp ⊢
 249      omega
 250    · intro q hq
 251      simp only [Finset.mem_filter_univ] at hq ⊢
 252      omega
 253    · intro p hp
 254      simp only [Finset.mem_filter_univ] at hp
 255      ext
 256      all_goals (try dsimp only)
 257      all_goals omega
 258    · intro q hq
 259      simp only [Finset.mem_filter_univ] at hq
 260      ext
 261      all_goals (try dsimp only)
 262      all_goals omega
 263    · intro p hp
 264      simp only [Finset.mem_filter_univ] at hp
 265      have htuple : w ∘ p.1.succAbove ∘ p.2.succAbove =
 266          w ∘ (⟨(p.2 : ℕ), by omega⟩ : Fin (n + 3)).succAbove ∘
 267            (⟨(p.1 : ℕ) - 1, by have := p.1.isLt; omega⟩ : Fin (n + 2)).succAbove := by
 268      -- faces commute: δ_i δ_j = δ_j δ_{i-1} for j < i
 269        funext k
 270        apply congrArg w
 271        apply Fin.ext
 272        have hk := k.isLt
 273        simp only [Function.comp_apply, SingularPrism.coe_succAbove]
 274        split_ifs <;> omega
 275      rw [htuple]
 276      have hsign : ((p.1 : ℕ) + (p.2 : ℕ)) =
 277          (((⟨(p.2 : ℕ), by omega⟩ : Fin (n + 3)) : ℕ) +
 278            ((⟨(p.1 : ℕ) - 1, by have := p.1.isLt; omega⟩ : Fin (n + 2)) : ℕ)) + 1 := by
 279        dsimp only
 280        omega
 281      rw [hsign, pow_succ, mul_neg_one, neg_smul]
 282  rw [hcancel, neg_add_cancel]
 283
 284/-- The augmentation kills boundaries: `ε ∘ ∂ = 0`. -/
 285theorem eps_comp_abnd : (eps α).comp (abnd 0) = 0 := by
 286  refine AC.hom_ext fun w => ?_
 287  rw [LinearMap.comp_apply, abnd_asimplex, map_sum, Fin.sum_univ_two,
 288    LinearMap.zero_apply]
 289  simp only [map_smul, eps_asimplex, Fin.val_zero, Fin.val_one, pow_zero, pow_one,
 290    smul_eq_mul, mul_one]
 291  omega
 292
 293/-! ## Stage 3: the barycentric subdivision operator and `∂S = S∂`
 294
 295The subdivision operator is parametrized by an abstract apex function
 296`bary` assigning to every vertex tuple a point (the barycenter, in the
 297geometric realization); all chain identities hold for any such function. -/
 298
 299/-- The barycentric subdivision operator on affine chains, defined by the
 300cone recursion `S(σ) = b_σ · S(∂σ)` on generators (`S = id` in degree 0). -/
 301noncomputable def asub (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 302    ∀ n, AC α n →ₗ[ℤ] AC α n
 303  | 0 => LinearMap.id
 304  | n + 1 => Finsupp.linearCombination ℤ
 305      (fun w : Fin (n + 2) → α =>
 306        acone (bary w) (asub bary n (abnd n (asimplex w))))
 307
 308@[simp] lemma asub_zero (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 309    asub bary 0 = LinearMap.id := rfl
 310
 311lemma asub_asimplex (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (n : ℕ)
 312    (w : Fin (n + 2) → α) :
 313    asub bary (n + 1) (asimplex w) =
 314      acone (bary w) (asub bary n (abnd n (asimplex w))) :=
 315  lift_asimplex _ w
 316
 317/-- The chain-map property of barycentric subdivision: `∂ ∘ S = S ∘ ∂`. -/
 318theorem abnd_comp_asub (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 319    ∀ n, (abnd n).comp (asub bary (n + 1)) = (asub bary n).comp (abnd n)
 320  | 0 => by
 321    refine AC.hom_ext fun w => ?_
 322    rw [LinearMap.comp_apply, LinearMap.comp_apply, asub_asimplex, asub_zero,
 323      LinearMap.id_apply]
 324    have hcone := LinearMap.congr_fun (abnd_comp_acone_zero (bary w) (α := α))
 325      (abnd 0 (asimplex w))
 326    rw [LinearMap.comp_apply, LinearMap.sub_apply, LinearMap.id_apply,
 327      LinearMap.comp_apply] at hcone
 328    rw [hcone]
 329    have heps := LinearMap.congr_fun (eps_comp_abnd (α := α)) (asimplex w)
 330    rw [LinearMap.comp_apply, LinearMap.zero_apply] at heps
 331    rw [heps, map_zero, sub_zero]
 332  | n + 1 => by
 333    have IH := abnd_comp_asub bary n
 334    refine AC.hom_ext fun w => ?_
 335    rw [LinearMap.comp_apply, LinearMap.comp_apply, asub_asimplex]
 336    have hcone := LinearMap.congr_fun (abnd_comp_acone (bary w) n (α := α))
 337      (asub bary (n + 1) (abnd (n + 1) (asimplex w)))
 338    rw [LinearMap.comp_apply, LinearMap.sub_apply, LinearMap.id_apply,
 339      LinearMap.comp_apply] at hcone
 340    rw [hcone]
 341    have hIH := LinearMap.congr_fun IH (abnd (n + 1) (asimplex w))
 342    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hIH
 343    rw [hIH]
 344    have hdd := LinearMap.congr_fun (abnd_comp_abnd n (α := α)) (asimplex w)
 345    rw [LinearMap.comp_apply, LinearMap.zero_apply] at hdd
 346    rw [hdd, map_zero, map_zero, sub_zero]
 347
 348/-! ## Stage 4: the chain homotopy `T` with `∂T + T∂ = id − S`,
 349and the telescoped homotopy for the iterate `S^k` -/
 350
 351/-- The subdivision chain homotopy on affine chains, defined by the cone
 352recursion `T(σ) = b_σ · (σ − T(∂σ))` on generators (`T = 0` in degree 0). -/
 353noncomputable def atee (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 354    ∀ n, AC α n →ₗ[ℤ] AC α (n + 1)
 355  | 0 => 0
 356  | n + 1 => Finsupp.linearCombination ℤ
 357      (fun w : Fin (n + 2) → α =>
 358        acone (bary w) (asimplex w - atee bary n (abnd n (asimplex w))))
 359
 360@[simp] lemma atee_zero (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 361    atee bary 0 = 0 := rfl
 362
 363lemma atee_asimplex (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (n : ℕ)
 364    (w : Fin (n + 2) → α) :
 365    atee bary (n + 1) (asimplex w) =
 366      acone (bary w) (asimplex w - atee bary n (abnd n (asimplex w))) :=
 367  lift_asimplex _ w
 368
 369/-- The chain homotopy identity in degree 0 (trivially, since `T = 0` and
 370`S = id` there): `∂ ∘ T = id − S`. -/
 371theorem abnd_comp_atee_zero (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 372    (abnd 0).comp (atee bary 0) = LinearMap.id - asub bary (0 : ℕ) := by
 373  rw [atee_zero, asub_zero, LinearMap.comp_zero, sub_self]
 374
 375/-- The chain homotopy identity in positive degrees:
 376`∂ ∘ T + T ∘ ∂ = id − S` on `AC α (n+1)` (Hatcher, proof of Prop. 2.21). -/
 377theorem abnd_comp_atee (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) :
 378    ∀ n, (abnd (n + 1)).comp (atee bary (n + 1)) + (atee bary n).comp (abnd n)
 379      = LinearMap.id - asub bary (n + 1)
 380  | 0 => by
 381    refine AC.hom_ext fun w => ?_
 382    rw [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.comp_apply,
 383      LinearMap.sub_apply, LinearMap.id_apply, atee_asimplex, atee_zero,
 384      LinearMap.zero_apply, sub_zero, add_zero, asub_asimplex, asub_zero,
 385      LinearMap.id_apply]
 386    have hcone := LinearMap.congr_fun (abnd_comp_acone (bary w) 0 (α := α))
 387      (asimplex w)
 388    rw [LinearMap.comp_apply, LinearMap.sub_apply, LinearMap.id_apply,
 389      LinearMap.comp_apply] at hcone
 390    rw [hcone]
 391  | n + 1 => by
 392    have IH := abnd_comp_atee bary n
 393    refine AC.hom_ext fun w => ?_
 394    rw [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.comp_apply,
 395      LinearMap.sub_apply, LinearMap.id_apply, atee_asimplex, asub_asimplex]
 396    have hcone := LinearMap.congr_fun (abnd_comp_acone (bary w) (n + 1) (α := α))
 397      (asimplex w - atee bary (n + 1) (abnd (n + 1) (asimplex w)))
 398    rw [LinearMap.comp_apply, LinearMap.sub_apply, LinearMap.id_apply,
 399      LinearMap.comp_apply] at hcone
 400    rw [hcone, map_sub]
 401    -- compute `∂(σ − T∂σ) = S∂σ` from the inductive hypothesis and `∂∂ = 0`
 402    have hIH := LinearMap.congr_fun IH (abnd (n + 1) (asimplex w))
 403    simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.sub_apply,
 404      LinearMap.id_apply] at hIH
 405    have hdd := LinearMap.congr_fun (abnd_comp_abnd n (α := α)) (asimplex w)
 406    rw [LinearMap.comp_apply, LinearMap.zero_apply] at hdd
 407    rw [hdd, map_zero, add_zero] at hIH
 408    rw [hIH, sub_sub_cancel]
 409    abel
 410
 411/-! ### Iteration: `S^k` is chain homotopic to the identity -/
 412
 413/-- The `k`-th iterate of the subdivision operator (as a family of chain
 414endomorphisms). -/
 415noncomputable def asubIter (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α)
 416    (k n : ℕ) : AC α n →ₗ[ℤ] AC α n :=
 417  match k with
 418  | 0 => LinearMap.id
 419  | k + 1 => (asub bary n).comp (asubIter bary k n)
 420
 421@[simp] lemma asubIter_zero (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (n : ℕ) :
 422    asubIter bary 0 n = LinearMap.id := rfl
 423
 424lemma asubIter_succ (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (k n : ℕ) :
 425    asubIter bary (k + 1) n = (asub bary n).comp (asubIter bary k n) := rfl
 426
 427/-- The iterate is a chain map: `∂ ∘ S^k = S^k ∘ ∂`. -/
 428theorem abnd_comp_asubIter (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α)
 429    (k n : ℕ) :
 430    (abnd n).comp (asubIter bary k (n + 1)) = (asubIter bary k n).comp (abnd n) := by
 431  induction k with
 432  | zero => rw [asubIter_zero, asubIter_zero, LinearMap.comp_id, LinearMap.id_comp]
 433  | succ k IH =>
 434      rw [asubIter_succ, asubIter_succ, ← LinearMap.comp_assoc,
 435        abnd_comp_asub, LinearMap.comp_assoc, IH, LinearMap.comp_assoc]
 436
 437/-- The telescoped chain homotopy between `S^k` and the identity:
 438`Tk = T ∘ (1 + S + ⋯ + S^{k−1})`, packaged degreewise by recursion
 439`T_0 = 0`, `T_{k+1} = T + T_k ∘ S`. -/
 440noncomputable def ateeIter (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α)
 441    (k n : ℕ) : AC α n →ₗ[ℤ] AC α (n + 1) :=
 442  match k with
 443  | 0 => 0
 444  | k + 1 => atee bary n + (ateeIter bary k n).comp (asub bary n)
 445
 446@[simp] lemma ateeIter_zero (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (n : ℕ) :
 447    ateeIter bary 0 n = 0 := rfl
 448
 449lemma ateeIter_succ (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (k n : ℕ) :
 450    ateeIter bary (k + 1) n =
 451      atee bary n + (ateeIter bary k n).comp (asub bary n) := rfl
 452
 453/-- The subdivision operator commutes with its own iterates. -/
 454lemma asubIter_comp_asub (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α) (k n : ℕ) :
 455    (asubIter bary k n).comp (asub bary n) = (asub bary n).comp (asubIter bary k n) := by
 456  induction k with
 457  | zero => rw [asubIter_zero, LinearMap.comp_id, LinearMap.id_comp]
 458  | succ k IH =>
 459      rw [asubIter_succ, LinearMap.comp_assoc, IH, ← LinearMap.comp_assoc]
 460
 461/-- The telescoped chain homotopy identity in positive degrees:
 462`∂ ∘ Tk + Tk ∘ ∂ = id − S^k` on `AC α (n+1)`. -/
 463theorem abnd_comp_ateeIter (bary : ∀ {m : ℕ}, (Fin (m + 1) → α) → α)
 464    (k n : ℕ) :
 465    (abnd (n + 1)).comp (ateeIter bary k (n + 1)) +
 466        (ateeIter bary k n).comp (abnd n)
 467      = LinearMap.id - asubIter bary k (n + 1) := by
 468  induction k with
 469  | zero =>
 470      rw [ateeIter_zero, ateeIter_zero, asubIter_zero, LinearMap.comp_zero,
 471        LinearMap.zero_comp, add_zero, sub_self]
 472  | succ k IH =>
 473      rw [ateeIter_succ, ateeIter_succ, asubIter_succ,
 474        LinearMap.comp_add, LinearMap.add_comp]
 475      -- rewrite `Tk S ∂` as `Tk ∂ S` via the chain-map property of `S`
 476      have hswap : ((ateeIter bary k n).comp (asub bary n)).comp (abnd n)
 477          = ((ateeIter bary k n).comp (abnd n)).comp (asub bary (n + 1)) := by
 478        rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← abnd_comp_asub]
 479      rw [hswap]
 480      -- regroup as `(∂T + T∂) + (∂Tk + Tk∂) ∘ S`
 481      have hgroup :
 482          ((abnd (n + 1)).comp (atee bary (n + 1)) +
 483              (abnd (n + 1)).comp ((ateeIter bary k (n + 1)).comp (asub bary (n + 1)))) +
 484            ((atee bary n).comp (abnd n) +
 485              ((ateeIter bary k n).comp (abnd n)).comp (asub bary (n + 1)))
 486          = ((abnd (n + 1)).comp (atee bary (n + 1)) + (atee bary n).comp (abnd n)) +
 487            ((abnd (n + 1)).comp (ateeIter bary k (n + 1)) +
 488              (ateeIter bary k n).comp (abnd n)).comp (asub bary (n + 1)) := by
 489        rw [LinearMap.add_comp, ← LinearMap.comp_assoc]
 490        abel
 491      rw [hgroup, abnd_comp_atee, IH, LinearMap.sub_comp, LinearMap.id_comp,
 492        asubIter_comp_asub]
 493      abel
 494
 495/-! ## Stage 5a: pushforward of affine chains and equivariance
 496
 497Affine chains push forward along any map of point types `f : α → β`
 498(post-composition of vertex tuples).  The pushforward commutes with the
 499boundary and the cone, and, when `f` intertwines the two apex functions
 500(`baryβ (f ∘ w) = f (baryα w)`), with the subdivision operator `asub` and
 501the chain homotopy `atee` as well.  For the geometric stage the map `f`
 502will be an affine map of standard simplices, which sends barycenters to
 503barycenters. -/
 504
 505/-- The pushforward of affine chains along a map of point types. -/
 506noncomputable def amap (f : α → β) (n : ℕ) : AC α n →ₗ[ℤ] AC β n :=
 507  Finsupp.lmapDomain ℤ ℤ (fun w : Fin (n + 1) → α => f ∘ w)
 508
 509lemma amap_asimplex (f : α → β) (n : ℕ) (w : Fin (n + 1) → α) :
 510    amap f n (asimplex w) = asimplex (f ∘ w) := by
 511  rw [amap, asimplex, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, asimplex]
 512
 513/-- The pushforward commutes with the boundary. -/
 514lemma amap_comp_abnd (f : α → β) (n : ℕ) :
 515    (amap f n).comp (abnd n) = (abnd n).comp (amap f (n + 1)) := by
 516  refine AC.hom_ext fun w => ?_
 517  rw [LinearMap.comp_apply, LinearMap.comp_apply, abnd_asimplex, map_sum,
 518    amap_asimplex, abnd_asimplex]
 519  refine Finset.sum_congr rfl fun i _ => ?_
 520  rw [map_smul, amap_asimplex]
 521  rfl
 522
 523/-- The pushforward commutes with the cone (with pushed apex). -/
 524lemma amap_comp_acone (f : α → β) (b : α) (n : ℕ) :
 525    (amap f (n + 1)).comp (acone b : AC α n →ₗ[ℤ] AC α (n + 1)) =
 526      (acone (f b)).comp (amap f n) := by
 527  refine AC.hom_ext fun w => ?_
 528  rw [LinearMap.comp_apply, LinearMap.comp_apply, acone_asimplex, amap_asimplex,
 529    amap_asimplex, acone_asimplex]
 530  congr 1
 531  funext k
 532  induction k using Fin.cases with
 533  | zero => simp only [Function.comp_apply, Fin.cons_zero]
 534  | succ k => simp only [Function.comp_apply, Fin.cons_succ]
 535
 536/-- Equivariance of the subdivision operator: a map intertwining the apex
 537functions intertwines `asub`. -/
 538theorem amap_comp_asub (f : α → β)
 539    (baryα : ∀ {m : ℕ}, (Fin (m + 1) → α) → α)
 540    (baryβ : ∀ {m : ℕ}, (Fin (m + 1) → β) → β)
 541    (hf : ∀ (m : ℕ) (w : Fin (m + 1) → α), baryβ (f ∘ w) = f (baryα w)) :
 542    ∀ n, (amap f n).comp (asub baryα n) = (asub baryβ n).comp (amap f n)
 543  | 0 => by rw [asub_zero, asub_zero, LinearMap.comp_id, LinearMap.id_comp]
 544  | n + 1 => by
 545    have IH := amap_comp_asub f baryα baryβ hf n
 546    refine AC.hom_ext fun w => ?_
 547    rw [LinearMap.comp_apply, LinearMap.comp_apply, asub_asimplex, amap_asimplex,
 548      asub_asimplex]
 549    have hcone := LinearMap.congr_fun (amap_comp_acone f (baryα w) n)
 550      (asub baryα n (abnd n (asimplex w)))
 551    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hcone
 552    rw [hcone, hf]
 553    congr 1
 554    have hIH := LinearMap.congr_fun IH (abnd n (asimplex w))
 555    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hIH
 556    rw [hIH]
 557    congr 1
 558    have hbnd := LinearMap.congr_fun (amap_comp_abnd f n) (asimplex w)
 559    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hbnd
 560    rw [hbnd, amap_asimplex]
 561
 562/-- Equivariance of the subdivision homotopy: a map intertwining the apex
 563functions intertwines `atee`. -/
 564theorem amap_comp_atee (f : α → β)
 565    (baryα : ∀ {m : ℕ}, (Fin (m + 1) → α) → α)
 566    (baryβ : ∀ {m : ℕ}, (Fin (m + 1) → β) → β)
 567    (hf : ∀ (m : ℕ) (w : Fin (m + 1) → α), baryβ (f ∘ w) = f (baryα w)) :
 568    ∀ n, (amap f (n + 1)).comp (atee baryα n) = (atee baryβ n).comp (amap f n)
 569  | 0 => by rw [atee_zero, atee_zero, LinearMap.comp_zero, LinearMap.zero_comp]
 570  | n + 1 => by
 571    have IH := amap_comp_atee f baryα baryβ hf n
 572    refine AC.hom_ext fun w => ?_
 573    rw [LinearMap.comp_apply, LinearMap.comp_apply, atee_asimplex, amap_asimplex,
 574      atee_asimplex]
 575    have hcone := LinearMap.congr_fun (amap_comp_acone f (baryα w) (n + 1))
 576      (asimplex w - atee baryα n (abnd n (asimplex w)))
 577    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hcone
 578    rw [hcone, hf]
 579    congr 1
 580    rw [map_sub, amap_asimplex]
 581    congr 1
 582    have hIH := LinearMap.congr_fun IH (abnd n (asimplex w))
 583    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hIH
 584    rw [hIH]
 585    congr 1
 586    have hbnd := LinearMap.congr_fun (amap_comp_abnd f n) (asimplex w)
 587    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hbnd
 588    rw [hbnd, amap_asimplex]
 589
 590/-! ## Stage 5b: geometry on the standard simplex
 591
 592The affine realization of a vertex tuple `v : Fin (n+1) → Δᵐ` as a
 593continuous map `Δⁿ → Δᵐ` (barycentric-coordinate weighted sum of the
 594vertices), its functoriality, and the honest barycenter `sbary`. -/
 595
 596section Geometry
 597
 598variable {d m k : ℕ}
 599
 600/-- The underlying function of the affine map determined by a vertex tuple:
 601`x ↦ ∑ i, x i • v i` in barycentric coordinates. -/
 602def affineMapFun (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1)))
 603    (x : stdSimplex ℝ (Fin (n + 1))) : Fin (m + 1) → ℝ :=
 604  fun j => ∑ i, x i * v i j
 605
 606lemma affineMapFun_mem (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1)))
 607    (x : stdSimplex ℝ (Fin (n + 1))) :
 608    affineMapFun v x ∈ stdSimplex ℝ (Fin (m + 1)) := by
 609  constructor
 610  · intro j
 611    exact Finset.sum_nonneg fun i _ =>
 612      mul_nonneg (stdSimplex.zero_le x i) (stdSimplex.zero_le (v i) j)
 613  · show ∑ j, ∑ i, x i * v i j = 1
 614    rw [Finset.sum_comm]
 615    calc ∑ i, ∑ j, x i * v i j = ∑ i : Fin (n + 1), x i * 1 := by
 616          refine Finset.sum_congr rfl fun i _ => ?_
 617          rw [← Finset.mul_sum, stdSimplex.sum_eq_one]
 618      _ = 1 := by
 619          simp only [mul_one]
 620          exact stdSimplex.sum_eq_one x
 621
 622lemma continuous_affineMapFun (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1))) :
 623    Continuous (affineMapFun v) := by
 624  refine continuous_pi fun j => continuous_finset_sum _ fun i _ =>
 625    Continuous.mul ?_ continuous_const
 626  exact (continuous_apply i).comp continuous_subtype_val
 627
 628/-- The affine map `Δⁿ → Δᵐ` determined by a vertex tuple
 629`v : Fin (n+1) → Δᵐ`, sending the `i`-th vertex of `Δⁿ` to `v i`. -/
 630noncomputable def affineMap (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1))) :
 631    C(stdSimplex ℝ (Fin (n + 1)), stdSimplex ℝ (Fin (m + 1))) where
 632  toFun x := ⟨affineMapFun v x, affineMapFun_mem v x⟩
 633  continuous_toFun := (continuous_affineMapFun v).subtype_mk _
 634
 635@[simp] lemma affineMap_apply_coe (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1)))
 636    (x : stdSimplex ℝ (Fin (n + 1))) (j : Fin (m + 1)) :
 637    affineMap v x j = ∑ i, x i * v i j := rfl
 638
 639/-- The affine map sends vertices to the prescribed points. -/
 640lemma affineMap_vertex (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1)))
 641    (i : Fin (n + 1)) :
 642    affineMap v (stdSimplex.vertex i) = v i := by
 643  refine stdSimplex.ext ?_
 644  funext j
 645  rw [affineMap_apply_coe, Finset.sum_eq_single i]
 646  · show (Pi.single i 1 : Fin (n + 1) → ℝ) i * v i j = v i j
 647    rw [Pi.single_eq_same, one_mul]
 648  · intro b _ hb
 649    show (Pi.single i 1 : Fin (n + 1) → ℝ) b * v b j = 0
 650    rw [Pi.single_eq_of_ne hb, zero_mul]
 651  · intro h
 652    exact absurd (Finset.mem_univ i) h
 653
 654/-- Functoriality: the composite of affine maps is the affine map of the
 655pushed vertex tuple. -/
 656theorem affineMap_comp (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1)))
 657    (w : Fin (k + 1) → stdSimplex ℝ (Fin (n + 1))) :
 658    (affineMap v).comp (affineMap w) = affineMap (fun i => affineMap v (w i)) := by
 659  refine ContinuousMap.ext fun x => stdSimplex.ext ?_
 660  funext j
 661  show affineMap v (affineMap w x) j = affineMap (fun i => affineMap v (w i)) x j
 662  simp only [affineMap_apply_coe, Finset.sum_mul, Finset.mul_sum]
 663  rw [Finset.sum_comm]
 664  exact Finset.sum_congr rfl fun l _ => Finset.sum_congr rfl fun i _ => by ring
 665
 666/-- The identity vertex tuple. -/
 667noncomputable def idTuple (n : ℕ) : Fin (n + 1) → stdSimplex ℝ (Fin (n + 1)) :=
 668  fun i => stdSimplex.vertex i
 669
 670/-- The affine map of the identity tuple is the identity. -/
 671lemma affineMap_idTuple (n : ℕ) :
 672    affineMap (idTuple n) = ContinuousMap.id (stdSimplex ℝ (Fin (n + 1))) := by
 673  refine ContinuousMap.ext fun x => stdSimplex.ext ?_
 674  funext j
 675  show affineMap (idTuple n) x j = x j
 676  rw [affineMap_apply_coe, Finset.sum_eq_single j]
 677  · show x j * (Pi.single j 1 : Fin (n + 1) → ℝ) j = x j
 678    rw [Pi.single_eq_same, mul_one]
 679  · intro b _ hb
 680    show x b * (Pi.single b 1 : Fin (n + 1) → ℝ) j = 0
 681    rw [Pi.single_eq_of_ne (Ne.symm hb), mul_zero]
 682  · intro h
 683    exact absurd (Finset.mem_univ j) h
 684
 685/-- Composing an affine map with the identity tuple recovers the tuple. -/
 686lemma affineMap_comp_idTuple (v : Fin (n + 1) → stdSimplex ℝ (Fin (m + 1))) :
 687    ⇑(affineMap v) ∘ idTuple n = v :=
 688  funext fun i => affineMap_vertex v i
 689
 690/-- `stdSimplex.map` along a vertex map is the affine map of the
 691corresponding vertex tuple. -/
 692lemma stdSimplex_map_eq_affineMap (g : Fin (n + 1) → Fin (m + 1))
 693    (x : stdSimplex ℝ (Fin (n + 1))) :
 694    stdSimplex.map g x = affineMap (fun i => stdSimplex.vertex (g i)) x := by
 695  refine stdSimplex.ext ?_
 696  funext j
 697  have hL : (stdSimplex.map g x) j = ∑ i with g i = j, x i :=
 698    FunOnFinite.linearMap_apply_apply ℝ ℝ g (⇑x) j
 699  rw [hL]
 700  show ∑ i with g i = j, x i = ∑ i, x i * (Pi.single (g i) 1 : Fin (m + 1) → ℝ) j
 701  rw [Finset.sum_filter]
 702  refine Finset.sum_congr rfl fun i _ => ?_
 703  by_cases h : g i = j
 704  · rw [if_pos h, ← h, Pi.single_eq_same, mul_one]
 705  · rw [if_neg h, Pi.single_eq_of_ne (Ne.symm h), mul_zero]
 706
 707/-- Composing an affine map with a topological face inclusion restricts the
 708vertex tuple along `Fin.succAbove`. -/
 709lemma affineMap_comp_face (v : Fin (n + 2) → stdSimplex ℝ (Fin (d + 1)))
 710    (j : Fin (n + 2)) :
 711    (affineMap v).comp (SingularPrism.face j) =
 712      affineMap (v ∘ j.succAbove) := by
 713  refine ContinuousMap.ext fun x => ?_
 714  rw [ContinuousMap.comp_apply]
 715  show affineMap v (stdSimplex.map j.succAbove x) = _
 716  rw [stdSimplex_map_eq_affineMap j.succAbove x, ← ContinuousMap.comp_apply,
 717    affineMap_comp]
 718  have h : (fun i => affineMap v (stdSimplex.vertex (j.succAbove i))) =
 719      v ∘ j.succAbove := funext fun i => affineMap_vertex v _
 720  rw [h]
 721
 722/-- The barycenter of a vertex tuple in a standard simplex. -/
 723noncomputable def sbary {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))) :
 724    stdSimplex ℝ (Fin (d + 1)) :=
 725  ⟨fun j => ((m : ℝ) + 1)⁻¹ * ∑ i, w i j, by
 726    constructor
 727    · intro j
 728      refine mul_nonneg (inv_nonneg.mpr (by positivity)) ?_
 729      exact Finset.sum_nonneg fun i _ => stdSimplex.zero_le (w i) j
 730    · rw [← Finset.mul_sum, Finset.sum_comm]
 731      have hsum : ∑ i, ∑ j, w i j = ((m : ℝ) + 1) := by
 732        calc ∑ i : Fin (m + 1), ∑ j, w i j = ∑ i : Fin (m + 1), (1 : ℝ) :=
 733              Finset.sum_congr rfl fun i _ => stdSimplex.sum_eq_one (w i)
 734          _ = ((m : ℝ) + 1) := by
 735              rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin,
 736                nsmul_eq_mul, mul_one]
 737              push_cast
 738              ring
 739      rw [hsum, inv_mul_cancel₀ (by positivity)]⟩
 740
 741@[simp] lemma sbary_apply {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1)))
 742    (j : Fin (d + 1)) :
 743    sbary w j = ((m : ℝ) + 1)⁻¹ * ∑ i, w i j := rfl
 744
 745/-- Affine maps send barycenters to barycenters (the intertwining property
 746required by the equivariance lemmas of stage 5a). -/
 747lemma sbary_affineMap (v : Fin (n + 1) → stdSimplex ℝ (Fin (d + 1))) {m : ℕ}
 748    (w : Fin (m + 1) → stdSimplex ℝ (Fin (n + 1))) :
 749    sbary (⇑(affineMap v) ∘ w) = affineMap v (sbary w) := by
 750  refine stdSimplex.ext ?_
 751  funext j
 752  show ((m : ℝ) + 1)⁻¹ * ∑ i, (affineMap v (w i)) j = affineMap v (sbary w) j
 753  simp only [affineMap_apply_coe, sbary_apply, mul_assoc, Finset.sum_mul,
 754    ← Finset.mul_sum]
 755  rw [Finset.sum_comm]
 756
 757end Geometry
 758
 759/-! ## Stage 5c: the singular subdivision operator `sdOp` and homotopy `tOp`
 760
 761Affine chains in `Δⁿ` are evaluated as singular chains of `X` along a
 762singular simplex `σ : Δⁿ → X` (`toChain`); pushing forward the subdivided
 763identity tuple defines the singular barycentric subdivision `sdOp` and its
 764chain homotopy `tOp` on Mathlib's singular chain complex.  All identities
 765transport from the affine layer through the equivariance lemmas of
 766stage 5a. -/
 767
 768section Singular
 769
 770open SingularPrism
 771
 772variable {X Y : TopCat.{0}}
 773
 774/-- Post-composition with a morphism of `ℤ`-modules, as a `ℤ`-linear map on
 775hom groups out of `ℤ`. -/
 776noncomputable def postComp {M N : ModuleCat.{0} ℤ} (g : M ⟶ N) :
 777    (ModuleCat.of ℤ ℤ ⟶ M) →ₗ[ℤ] (ModuleCat.of ℤ ℤ ⟶ N) where
 778  toFun f := f ≫ g
 779  map_add' f₁ f₂ := by rw [Preadditive.add_comp]
 780  map_smul' r f := by rw [RingHom.id_apply, Preadditive.zsmul_comp]
 781
 782/-- `TopCat.toSSetObjEquiv`, retyped so that the domain of the continuous
 783map is literally `stdSimplex ℝ (Fin (m + 1))` (rather than the definitionally
 784equal `Fin ((unop (op ⦋m⦌)).len + 1)` normal form, which blocks rewriting). -/
 785noncomputable def simplexEquiv (X : TopCat.{0}) (m : ℕ) :
 786    Idx X m ≃ C(stdSimplex ℝ (Fin (m + 1)), X) :=
 787  X.toSSetObjEquiv (op ⦋m⦌)
 788
 789/-- Retyped naturality of `simplexEquiv` with respect to face maps. -/
 790lemma simplexEquiv_δ {m : ℕ} (j : Fin (m + 2)) (a : Idx X (m + 1)) :
 791    simplexEquiv X m ((TopCat.toSSet.obj X).δ j a) =
 792      (simplexEquiv X (m + 1) a).comp (face j) :=
 793  toSSetObjEquiv_δ j a
 794
 795/-- Retyped naturality of `simplexEquiv` with respect to continuous maps. -/
 796lemma simplexEquiv_map (f : X ⟶ Y) {m : ℕ} (a : Idx X m) :
 797    simplexEquiv Y m ((TopCat.toSSet.map f).app (op ⦋m⦌) a) =
 798      f.hom.comp (simplexEquiv X m a) :=
 799  toSSetObjEquiv_map f a
 800
 801/-- The singular `m`-simplex obtained by precomposing `σ` with the affine
 802map of a vertex tuple `w` in `Δⁿ`. -/
 803noncomputable def pushSimplex {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) {m : ℕ}
 804    (w : Fin (m + 1) → stdSimplex ℝ (Fin (n + 1))) : Idx X m :=
 805  (simplexEquiv X m).symm (σ.comp (affineMap w))
 806
 807lemma simplexEquiv_pushSimplex {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) {m : ℕ}
 808    (w : Fin (m + 1) → stdSimplex ℝ (Fin (n + 1))) :
 809    simplexEquiv X m (pushSimplex σ w) = σ.comp (affineMap w) :=
 810  Equiv.apply_symm_apply _ _
 811
 812/-- Evaluation of affine chains in `Δⁿ` as singular chains of `X` along a
 813singular simplex `σ : Δⁿ → X`. -/
 814noncomputable def toChain {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) (m : ℕ) :
 815    AC (stdSimplex ℝ (Fin (n + 1))) m →ₗ[ℤ] (ModuleCat.of ℤ ℤ ⟶ Cgrp X m) :=
 816  Finsupp.linearCombination ℤ (fun w => gen X m (pushSimplex σ w))
 817
 818lemma toChain_asimplex {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) (m : ℕ)
 819    (w : Fin (m + 1) → stdSimplex ℝ (Fin (n + 1))) :
 820    toChain σ m (asimplex w) = gen X m (pushSimplex σ w) :=
 821  lift_asimplex _ w
 822
 823/-- Faces of pushed simplices restrict the vertex tuple. -/
 824lemma δ_pushSimplex {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) {m : ℕ}
 825    (w : Fin (m + 2) → stdSimplex ℝ (Fin (n + 1))) (k : Fin (m + 2)) :
 826    (TopCat.toSSet.obj X).δ k (pushSimplex σ w) =
 827      pushSimplex σ (w ∘ k.succAbove) := by
 828  apply (simplexEquiv X m).injective
 829  rw [simplexEquiv_δ, simplexEquiv_pushSimplex, simplexEquiv_pushSimplex,
 830    ContinuousMap.comp_assoc, affineMap_comp_face]
 831
 832/-- The pushed simplex of the identity tuple is the simplex itself. -/
 833lemma pushSimplex_idTuple {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) :
 834    pushSimplex σ (idTuple n) = (simplexEquiv X n).symm σ := by
 835  unfold pushSimplex
 836  rw [affineMap_idTuple, ContinuousMap.comp_id]
 837
 838lemma toChain_asimplex_idTuple {n : ℕ} (s : Idx X n) :
 839    toChain (simplexEquiv X n s) n (asimplex (idTuple n)) = gen X n s := by
 840  rw [toChain_asimplex, pushSimplex_idTuple, Equiv.symm_apply_apply]
 841
 842/-- Any face of a singular simplex is the pushed simplex of a face of the
 843identity tuple. -/
 844lemma δ_eq_pushSimplex {n : ℕ} (s : Idx X (n + 1)) (k : Fin (n + 2)) :
 845    (TopCat.toSSet.obj X).δ k s =
 846      pushSimplex (simplexEquiv X (n + 1) s) (idTuple (n + 1) ∘ k.succAbove) := by
 847  have h : pushSimplex (simplexEquiv X (n + 1) s) (idTuple (n + 1)) = s := by
 848    rw [pushSimplex_idTuple, Equiv.symm_apply_apply]
 849  conv_lhs => rw [← h]
 850  exact δ_pushSimplex _ _ k
 851
 852/-- `toChain` intertwines the affine and the singular boundary. -/
 853lemma toChain_comp_abnd {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) (m : ℕ) :
 854    (postComp (bnd X m)).comp (toChain σ (m + 1)) = (toChain σ m).comp (abnd m) := by
 855  refine AC.hom_ext fun w => ?_
 856  rw [LinearMap.comp_apply, LinearMap.comp_apply, toChain_asimplex]
 857  show gen X (m + 1) (pushSimplex σ w) ≫ bnd X m = toChain σ m (abnd m (asimplex w))
 858  rw [gen_d, abnd_asimplex, map_sum]
 859  refine Finset.sum_congr rfl fun k _ => ?_
 860  rw [map_smul, toChain_asimplex, δ_pushSimplex]
 861
 862/-- `toChain` intertwines post-composition with the induced chain map. -/
 863lemma toChain_comp_chainMap {n : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X))
 864    (f : X ⟶ Y) (m : ℕ) :
 865    (postComp (chainMap f m)).comp (toChain σ m) = toChain (f.hom.comp σ) m := by
 866  refine AC.hom_ext fun w => ?_
 867  rw [LinearMap.comp_apply, toChain_asimplex, toChain_asimplex]
 868  show gen X m (pushSimplex σ w) ≫ chainMap f m =
 869    gen Y m (pushSimplex (f.hom.comp σ) w)
 870  rw [gen_map]
 871  congr 1
 872
 873/-- `toChain` turns the affine pushforward along an affine map into
 874precomposition of the singular simplex. -/
 875lemma toChain_amap {n n' : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X))
 876    (v : Fin (n' + 1) → stdSimplex ℝ (Fin (n + 1))) (m : ℕ) :
 877    (toChain σ m).comp (amap (⇑(affineMap v)) m) = toChain (σ.comp (affineMap v)) m := by
 878  refine AC.hom_ext fun w => ?_
 879  rw [LinearMap.comp_apply, amap_asimplex, toChain_asimplex, toChain_asimplex]
 880  congr 1
 881  apply (simplexEquiv X m).injective
 882  rw [simplexEquiv_pushSimplex, simplexEquiv_pushSimplex, ContinuousMap.comp_assoc,
 883    affineMap_comp]
 884  rfl
 885
 886/-- The barycentric apex function on `Δⁿ`, in the shape expected by
 887`asub`/`atee`. -/
 888noncomputable def baryFn (n : ℕ) :
 889    ∀ {m : ℕ}, (Fin (m + 1) → stdSimplex ℝ (Fin (n + 1))) → stdSimplex ℝ (Fin (n + 1)) :=
 890  fun {_} w => sbary w
 891
 892/-- Generator value of the singular subdivision operator. -/
 893noncomputable def sdGen (X : TopCat.{0}) (n : ℕ) (s : Idx X n) :
 894    ModuleCat.of ℤ ℤ ⟶ Cgrp X n :=
 895  toChain (simplexEquiv X n s) n (asub (baryFn n) n (asimplex (idTuple n)))
 896
 897/-- The singular barycentric subdivision operator `sdOp X : C_n(X) ⟶ C_n(X)`. -/
 898noncomputable def sdOp (X : TopCat.{0}) (n : ℕ) : Cgrp X n ⟶ Cgrp X n :=
 899  Sigma.desc (sdGen X n)
 900
 901lemma gen_sdOp {n : ℕ} (s : Idx X n) : gen X n s ≫ sdOp X n = sdGen X n s :=
 902  Sigma.ι_desc _ _
 903
 904/-- Generator value of the singular subdivision homotopy. -/
 905noncomputable def tGen (X : TopCat.{0}) (n : ℕ) (s : Idx X n) :
 906    ModuleCat.of ℤ ℤ ⟶ Cgrp X (n + 1) :=
 907  toChain (simplexEquiv X n s) (n + 1) (atee (baryFn n) n (asimplex (idTuple n)))
 908
 909/-- The singular subdivision chain homotopy `tOp X : C_n(X) ⟶ C_{n+1}(X)`. -/
 910noncomputable def tOp (X : TopCat.{0}) (n : ℕ) : Cgrp X n ⟶ Cgrp X (n + 1) :=
 911  Sigma.desc (tGen X n)
 912
 913lemma gen_tOp {n : ℕ} (s : Idx X n) : gen X n s ≫ tOp X n = tGen X n s :=
 914  Sigma.ι_desc _ _
 915
 916/-- The heart of the transport: `sdOp` on a pushed generator computes the
 917subdivision of the pushed tuple. -/
 918lemma gen_pushSimplex_comp_sdOp {n n' : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X))
 919    (w : Fin (n' + 1) → stdSimplex ℝ (Fin (n + 1))) :
 920    gen X n' (pushSimplex σ w) ≫ sdOp X n' =
 921      toChain σ n' (asub (baryFn n) n' (asimplex w)) := by
 922  rw [gen_sdOp]
 923  show toChain (simplexEquiv X n' (pushSimplex σ w)) n'
 924      (asub (baryFn n') n' (asimplex (idTuple n'))) = _
 925  rw [simplexEquiv_pushSimplex]
 926  have hL := LinearMap.congr_fun (toChain_amap σ w n')
 927    (asub (baryFn n') n' (asimplex (idTuple n')))
 928  rw [LinearMap.comp_apply] at hL
 929  rw [← hL]
 930  have heq := LinearMap.congr_fun (amap_comp_asub (⇑(affineMap w)) (baryFn n')
 931    (baryFn n) (fun m u => sbary_affineMap w u) n') (asimplex (idTuple n'))
 932  rw [LinearMap.comp_apply, LinearMap.comp_apply] at heq
 933  rw [heq, amap_asimplex, affineMap_comp_idTuple]
 934
 935/-- `tOp` on a pushed generator computes the homotopy of the pushed tuple. -/
 936lemma gen_pushSimplex_comp_tOp {n n' : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X))
 937    (w : Fin (n' + 1) → stdSimplex ℝ (Fin (n + 1))) :
 938    gen X n' (pushSimplex σ w) ≫ tOp X n' =
 939      toChain σ (n' + 1) (atee (baryFn n) n' (asimplex w)) := by
 940  rw [gen_tOp]
 941  show toChain (simplexEquiv X n' (pushSimplex σ w)) (n' + 1)
 942      (atee (baryFn n') n' (asimplex (idTuple n'))) = _
 943  rw [simplexEquiv_pushSimplex]
 944  have hL := LinearMap.congr_fun (toChain_amap σ w (n' + 1))
 945    (atee (baryFn n') n' (asimplex (idTuple n')))
 946  rw [LinearMap.comp_apply] at hL
 947  rw [← hL]
 948  have heq := LinearMap.congr_fun (amap_comp_atee (⇑(affineMap w)) (baryFn n')
 949    (baryFn n) (fun m u => sbary_affineMap w u) n') (asimplex (idTuple n'))
 950  rw [LinearMap.comp_apply, LinearMap.comp_apply] at heq
 951  rw [heq, amap_asimplex, affineMap_comp_idTuple]
 952
 953/-- The singular subdivision operator is a chain map: `∂ ∘ S = S ∘ ∂`. -/
 954theorem sdOp_comp_bnd (X : TopCat.{0}) (n : ℕ) :
 955    sdOp X (n + 1) ≫ bnd X n = bnd X n ≫ sdOp X n := by
 956  apply Sigma.hom_ext
 957  intro s
 958  rw [← Category.assoc, ← Category.assoc, gen_sdOp, gen_d]
 959  have hL : sdGen X (n + 1) s ≫ bnd X n =
 960      toChain (simplexEquiv X (n + 1) s) n
 961        (asub (baryFn (n + 1)) n (abnd n (asimplex (idTuple (n + 1))))) := by
 962    have h := LinearMap.congr_fun
 963      (toChain_comp_abnd (simplexEquiv X (n + 1) s) n)
 964      (asub (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))))
 965    rw [LinearMap.comp_apply, LinearMap.comp_apply] at h
 966    have hcomm := LinearMap.congr_fun (abnd_comp_asub (baryFn (n + 1)) n)
 967      (asimplex (idTuple (n + 1)))
 968    rw [LinearMap.comp_apply, LinearMap.comp_apply] at hcomm
 969    rw [← hcomm]
 970    exact h
 971  rw [hL, abnd_asimplex, map_sum, map_sum, Preadditive.sum_comp]
 972  refine Finset.sum_congr rfl fun k _ => ?_
 973  rw [map_smul, map_smul, Preadditive.zsmul_comp]
 974  congr 1
 975  rw [δ_eq_pushSimplex, gen_pushSimplex_comp_sdOp]
 976
 977/-- In degree `0` the singular subdivision operator is the identity. -/
 978theorem sdOp_zero (X : TopCat.{0}) : sdOp X 0 = 𝟙 (Cgrp X 0) := by
 979  apply Sigma.hom_ext
 980  intro s
 981  rw [Category.comp_id, gen_sdOp]
 982  show toChain (simplexEquiv X 0 s) 0
 983    (asub (baryFn 0) 0 (asimplex (idTuple 0))) = gen X 0 s
 984  rw [asub_zero, LinearMap.id_apply]
 985  exact toChain_asimplex_idTuple s
 986
 987/-- In degree `0` the singular subdivision homotopy vanishes. -/
 988theorem tOp_zero (X : TopCat.{0}) : tOp X 0 = 0 := by
 989  apply Sigma.hom_ext
 990  intro s
 991  rw [Limits.comp_zero, gen_tOp]
 992  show toChain (simplexEquiv X 0 s) 1
 993    (atee (baryFn 0) 0 (asimplex (idTuple 0))) = 0
 994  rw [atee_zero, LinearMap.zero_apply, map_zero]
 995
 996/-- The chain homotopy identity in positive degrees:
 997`∂ ∘ T + T ∘ ∂ = id − S` on the degree-`(n+1)` singular chain group. -/
 998theorem tOp_chain_homotopy_succ (X : TopCat.{0}) (n : ℕ) :
 999    bnd X n ≫ tOp X n + tOp X (n + 1) ≫ bnd X (n + 1) =
1000      𝟙 (Cgrp X (n + 1)) - sdOp X (n + 1) := by
1001  apply Sigma.hom_ext
1002  intro s
1003  rw [Preadditive.comp_add, Preadditive.comp_sub, Category.comp_id]
1004  -- second summand: `T ∘ ∂` transported to `toChain σ (T (∂ id))`
1005  have h2 : gen X (n + 1) s ≫ (bnd X n ≫ tOp X n) =
1006      toChain (simplexEquiv X (n + 1) s) (n + 1)
1007        (atee (baryFn (n + 1)) n (abnd n (asimplex (idTuple (n + 1))))) := by
1008    rw [← Category.assoc, gen_d, Preadditive.sum_comp, abnd_asimplex, map_sum,
1009      map_sum]
1010    refine Finset.sum_congr rfl fun k _ => ?_
1011    rw [Preadditive.zsmul_comp, map_smul, map_smul]
1012    congr 1
1013    rw [δ_eq_pushSimplex, gen_pushSimplex_comp_tOp]
1014  -- first summand: `∂ ∘ T` transported to `toChain σ (∂ (T id))`
1015  have h1 : gen X (n + 1) s ≫ (tOp X (n + 1) ≫ bnd X (n + 1)) =
1016      toChain (simplexEquiv X (n + 1) s) (n + 1)
1017        (abnd (n + 1) (atee (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))))) := by
1018    rw [← Category.assoc, gen_tOp]
1019    have h := LinearMap.congr_fun
1020      (toChain_comp_abnd (simplexEquiv X (n + 1) s) (n + 1))
1021      (atee (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))))
1022    rw [LinearMap.comp_apply, LinearMap.comp_apply] at h
1023    exact h
1024  rw [h2, h1, ← map_add, gen_sdOp]
1025  have hhom := LinearMap.congr_fun (abnd_comp_atee (baryFn (n + 1)) n)
1026    (asimplex (idTuple (n + 1)))
1027  simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.sub_apply,
1028    LinearMap.id_apply] at hhom
1029  have hsum : atee (baryFn (n + 1)) n (abnd n (asimplex (idTuple (n + 1)))) +
1030      abnd (n + 1) (atee (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1)))) =
1031      asimplex (idTuple (n + 1)) -
1032        asub (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))) := by
1033    exact (add_comm _ _).trans hhom
1034  rw [hsum, map_sub, toChain_asimplex_idTuple]
1035  rfl
1036
1037/-- In degree `0`: `∂ ∘ T = id − S` (both sides vanish). -/
1038theorem tOp_chain_homotopy_zero (X : TopCat.{0}) :
1039    tOp X 0 ≫ bnd X 0 = 𝟙 (Cgrp X 0) - sdOp X 0 := by
1040  rw [tOp_zero, sdOp_zero, Limits.zero_comp, sub_self]
1041
1042/-- Naturality of the singular subdivision operator. -/
1043theorem sdOp_natural (f : X ⟶ Y) (n : ℕ) :
1044    chainMap f n ≫ sdOp Y n = sdOp X n ≫ chainMap f n := by
1045  apply Sigma.hom_ext
1046  intro s
1047  rw [← Category.assoc, ← Category.assoc, gen_map, gen_sdOp, gen_sdOp]
1048  have hR := LinearMap.congr_fun
1049    (toChain_comp_chainMap (simplexEquiv X n s) f n)
1050    (asub (baryFn n) n (asimplex (idTuple n)))
1051  rw [LinearMap.comp_apply] at hR
1052  have hL : sdGen Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) s) =
1053      toChain (f.hom.comp (simplexEquiv X n s)) n
1054        (asub (baryFn n) n (asimplex (idTuple n))) := by
1055    show toChain (simplexEquiv Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) s)) n
1056        (asub (baryFn n) n (asimplex (idTuple n))) = _
1057    rw [simplexEquiv_map]
1058  rw [hL, ← hR]
1059  rfl
1060
1061/-- Naturality of the singular subdivision homotopy. -/
1062theorem tOp_natural (f : X ⟶ Y) (n : ℕ) :
1063    chainMap f n ≫ tOp Y n = tOp X n ≫ chainMap f (n + 1) := by
1064  apply Sigma.hom_ext
1065  intro s
1066  rw [← Category.assoc, ← Category.assoc, gen_map, gen_tOp, gen_tOp]
1067  have hR := LinearMap.congr_fun
1068    (toChain_comp_chainMap (simplexEquiv X n s) f (n + 1))
1069    (atee (baryFn n) n (asimplex (idTuple n)))
1070  rw [LinearMap.comp_apply] at hR
1071  have hL : tGen Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) s) =
1072      toChain (f.hom.comp (simplexEquiv X n s)) (n + 1)
1073        (atee (baryFn n) n (asimplex (idTuple n))) := by
1074    show toChain (simplexEquiv Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) s)) (n + 1)
1075        (atee (baryFn n) n (asimplex (idTuple n))) = _
1076    rw [simplexEquiv_map]
1077  rw [hL, ← hR]
1078  rfl
1079
1080/-! ### Iterates of the singular subdivision operator -/
1081
1082/-- The `k`-th iterate of the singular subdivision operator. -/
1083noncomputable def sdOpIter (X : TopCat.{0}) (n : ℕ) : ℕ → (Cgrp X n ⟶ Cgrp X n)
1084  | 0 => 𝟙 _
1085  | k + 1 => sdOpIter X n k ≫ sdOp X n
1086
1087@[simp] lemma sdOpIter_zero (X : TopCat.{0}) (n : ℕ) :
1088    sdOpIter X n 0 = 𝟙 (Cgrp X n) := rfl
1089
1090lemma sdOpIter_succ (X : TopCat.{0}) (n k : ℕ) :
1091    sdOpIter X n (k + 1) = sdOpIter X n k ≫ sdOp X n := rfl
1092
1093/-- The telescoped homotopy for the iterate, `T_{k+1} = T + S ≫ T_k`. -/
1094noncomputable def tOpIter (X : TopCat.{0}) (n : ℕ) : ℕ → (Cgrp X n ⟶ Cgrp X (n + 1))
1095  | 0 => 0
1096  | k + 1 => tOp X n + sdOp X n ≫ tOpIter X n k
1097
1098@[simp] lemma tOpIter_zero (X : TopCat.{0}) (n : ℕ) : tOpIter X n 0 = 0 := rfl
1099
1100lemma tOpIter_succ (X : TopCat.{0}) (n k : ℕ) :
1101    tOpIter X n (k + 1) = tOp X n + sdOp X n ≫ tOpIter X n k := rfl
1102
1103/-- The iterate commutes with `sdOp`. -/
1104lemma sdOpIter_comp_sdOp (X : TopCat.{0}) (n k : ℕ) :
1105    sdOpIter X n k ≫ sdOp X n = sdOp X n ≫ sdOpIter X n k := by
1106  induction k with
1107  | zero => rw [sdOpIter_zero, Category.id_comp, Category.comp_id]
1108  | succ k IH =>
1109      calc sdOpIter X n (k + 1) ≫ sdOp X n
1110          = sdOpIter X n k ≫ sdOp X n ≫ sdOp X n := by
1111            rw [sdOpIter_succ, Category.assoc]
1112        _ = (sdOp X n ≫ sdOpIter X n k) ≫ sdOp X n := by
1113            rw [← IH, Category.assoc]
1114        _ = sdOp X n ≫ sdOpIter X n (k + 1) := by
1115            rw [Category.assoc, sdOpIter_succ]
1116
1117/-- The iterate is a chain map. -/
1118theorem sdOpIter_comp_bnd (X : TopCat.{0}) (n k : ℕ) :
1119    sdOpIter X (n + 1) k ≫ bnd X n = bnd X n ≫ sdOpIter X n k := by
1120  induction k with
1121  | zero => rw [sdOpIter_zero, sdOpIter_zero, Category.id_comp, Category.comp_id]
1122  | succ k IH =>
1123      rw [sdOpIter_succ, sdOpIter_succ, Category.assoc, sdOp_comp_bnd,
1124        ← Category.assoc, IH, Category.assoc]
1125
1126/-- The telescoped chain homotopy identity in positive degrees:
1127`∂ ∘ T_k + T_k ∘ ∂ = id − S^k` on the degree-`(n+1)` singular chain group. -/
1128theorem tOpIter_chain_homotopy_succ (X : TopCat.{0}) (n k : ℕ) :
1129    bnd X n ≫ tOpIter X n k + tOpIter X (n + 1) k ≫ bnd X (n + 1) =
1130      𝟙 (Cgrp X (n + 1)) - sdOpIter X (n + 1) k := by
1131  induction k with
1132  | zero =>
1133      rw [tOpIter_zero, tOpIter_zero, sdOpIter_zero, Limits.comp_zero,
1134        Limits.zero_comp, add_zero, sub_self]
1135  | succ k IH =>
1136      rw [tOpIter_succ, tOpIter_succ, sdOpIter_succ]
1137      have key : bnd X n ≫ (tOp X n + sdOp X n ≫ tOpIter X n k) +
1138          (tOp X (n + 1) + sdOp X (n + 1) ≫ tOpIter X (n + 1) k) ≫ bnd X (n + 1) =
1139          (bnd X n ≫ tOp X n + tOp X (n + 1) ≫ bnd X (n + 1)) +
1140            sdOp X (n + 1) ≫
1141              (bnd X n ≫ tOpIter X n k + tOpIter X (n + 1) k ≫ bnd X (n + 1)) := by
1142        rw [Preadditive.comp_add, Preadditive.add_comp, Preadditive.comp_add,
1143          Category.assoc]
1144        have hmid : bnd X n ≫ sdOp X n ≫ tOpIter X n k =
1145            sdOp X (n + 1) ≫ bnd X n ≫ tOpIter X n k := by
1146          rw [← Category.assoc, ← sdOp_comp_bnd, Category.assoc]
1147        rw [hmid]
1148        abel
1149      rw [key, tOp_chain_homotopy_succ, IH, Preadditive.comp_sub,
1150        Category.comp_id, sdOpIter_comp_sdOp]
1151      abel
1152
1153/-- The telescoped chain homotopy identity in degree `0`:
1154`∂ ∘ T_k = id − S^k` on the degree-`0` singular chain group. -/
1155theorem tOpIter_chain_homotopy_zero (X : TopCat.{0}) (k : ℕ) :
1156    tOpIter X 0 k ≫ bnd X 0 = 𝟙 (Cgrp X 0) - sdOpIter X 0 k := by
1157  induction k with
1158  | zero => rw [tOpIter_zero, sdOpIter_zero, Limits.zero_comp, sub_self]
1159  | succ k IH =>
1160      rw [tOpIter_succ, sdOpIter_succ, Preadditive.add_comp, Category.assoc,
1161        tOp_chain_homotopy_zero, IH, Preadditive.comp_sub, Category.comp_id,
1162        sdOpIter_comp_sdOp]
1163      abel
1164
1165/-- `toChain` intertwines `sdOp` and the affine subdivision. -/
1166lemma toChain_comp_sdOp {n n' : ℕ} (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) :
1167    (postComp (sdOp X n')).comp (toChain σ n') =
1168      (toChain σ n').comp (asub (baryFn n) n') := by
1169  refine AC.hom_ext fun w => ?_
1170  rw [LinearMap.comp_apply, LinearMap.comp_apply, toChain_asimplex]
1171  exact gen_pushSimplex_comp_sdOp σ w
1172
1173/-- The iterated singular subdivision of a generator is the evaluation of the
1174iterated affine subdivision of the identity tuple.  This ties the singular
1175operator to the affine support geometry of stage 6. -/
1176theorem gen_comp_sdOpIter {n : ℕ} (s : Idx X n) (k : ℕ) :
1177    gen X n s ≫ sdOpIter X n k =
1178      toChain (simplexEquiv X n s) n
1179        (asubIter (baryFn n) k n (asimplex (idTuple n))) := by
1180  induction k with
1181  | zero =>
1182      rw [sdOpIter_zero, Category.comp_id, asubIter_zero, LinearMap.id_apply,
1183        toChain_asimplex_idTuple]
1184  | succ k IH =>
1185      rw [sdOpIter_succ, ← Category.assoc, IH, asubIter_succ, LinearMap.comp_apply]
1186      have h := LinearMap.congr_fun
1187        (toChain_comp_sdOp (X := X) (n' := n) (simplexEquiv X n s))
1188        (asubIter (baryFn n) k n (asimplex (idTuple n)))
1189      rw [LinearMap.comp_apply, LinearMap.comp_apply] at h
1190      exact h
1191
1192end Singular
1193
1194/-! ## Stage 6: the diameter estimate for barycentric subdivision
1195
1196We track the `Finsupp` support of the affine subdivision operator through its
1197cone recursion.  The two invariants: every vertex of every piece lies in the
1198convex hull (in the ambient coordinate space) of the original vertex tuple,
1199and the pairwise vertex distances contract by the factor `n / (n + 1)`.
1200Iterating gives geometric decay of piece diameters.  The ambient metric is
1201the sup metric on `Fin (d + 1) → ℝ`, whose subtype metric induces the
1202topology of `SimplexCategory.toTop` on `stdSimplex ℝ (Fin (d + 1))`. -/
1203
1204section SupportTracking
1205
1206variable {α : Type}
1207
1208/-- Transport of a support predicate through a linear operator on affine
1209chains: if `T` maps every generator satisfying `P` to a chain supported on
1210tuples satisfying `Q`, the same holds for arbitrary chains supported on `P`. -/
1211lemma support_transport {n m : ℕ} (T : AC α n →ₗ[ℤ] AC α m)
1212    {P : (Fin (n + 1) → α) → Prop} {Q : (Fin (m + 1) → α) → Prop}
1213    (hT : ∀ w, P w → ∀ u ∈ (T (asimplex w)).support, Q u)
1214    (c : AC α n) (hc : ∀ w ∈ c.support, P w) :
1215    ∀ u ∈ (T c).support, Q u := by
1216  intro u hu
1217  have hrep : T c = ∑ w ∈ c.support, T (Finsupp.single w (c w)) := by
1218    conv_lhs => rw [← Finsupp.sum_single c]
1219    rw [Finsupp.sum, map_sum]
1220  rw [hrep] at hu
1221  obtain ⟨w, hw, hu'⟩ := Finsupp.mem_support_finset_sum u hu
1222  have hsingle : (Finsupp.single w (c w) : AC α n) = (c w) • asimplex w := by
1223    rw [asimplex, Finsupp.smul_single, smul_eq_mul, mul_one]
1224  rw [hsingle, map_smul] at hu'
1225  exact hT w (hc w hw) u (Finsupp.support_smul hu')
1226
1227/-- The support of the boundary of a generator consists of faces. -/
1228lemma support_abnd_asimplex {n : ℕ} (w : Fin (n + 2) → α) :
1229    ∀ v ∈ (abnd n (asimplex w)).support, ∃ j : Fin (n + 2), v = w ∘ j.succAbove := by
1230  intro v hv
1231  rw [abnd_asimplex] at hv
1232  obtain ⟨j, _, hv'⟩ := Finsupp.mem_support_finset_sum v hv
1233  have hmem := Finsupp.support_smul hv'
1234  rw [asimplex] at hmem
1235  have hsingle := Finsupp.support_single_subset hmem
1236  rw [Finset.mem_singleton] at hsingle
1237  exact ⟨j, hsingle⟩
1238
1239/-- The support of a cone consists of cones over the original support. -/
1240lemma support_acone {n : ℕ} (b : α) (c : AC α n) :
1241    ∀ u ∈ (acone b c).support, ∃ v ∈ c.support, u = Fin.cons b v := by
1242  classical
1243  intro u hu
1244  rw [acone, Finsupp.lmapDomain_apply] at hu
1245  obtain ⟨v, hv, huv⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hu)
1246  exact ⟨v, hv, huv.symm⟩
1247
1248end SupportTracking
1249
1250section Diameter
1251
1252variable {d : ℕ}
1253
1254@[simp] lemma baryFn_apply {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))) :
1255    baryFn d w = sbary w := rfl
1256
1257/-- The convex hull, in the ambient coordinate space, of a vertex tuple in
1258the standard simplex. -/
1259def hullOf {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))) :
1260    Set (Fin (d + 1) → ℝ) :=
1261  convexHull ℝ (Set.range fun i => ((w i : Fin (d + 1) → ℝ)))
1262
1263lemma coe_mem_hullOf {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1)))
1264    (i : Fin (m + 1)) : ((w i : Fin (d + 1) → ℝ)) ∈ hullOf w :=
1265  subset_convexHull ℝ _ ⟨i, rfl⟩
1266
1267/-- Hull monotonicity from a coordinatewise membership hypothesis. -/
1268lemma hullOf_subset {m m' : ℕ} {w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))}
1269    {v : Fin (m' + 1) → stdSimplex ℝ (Fin (d + 1))}
1270    (h : ∀ i, ((v i : Fin (d + 1) → ℝ)) ∈ hullOf w) : hullOf v ⊆ hullOf w :=
1271  convexHull_min (by rintro x ⟨i, rfl⟩; exact h i) (convex_convexHull ℝ _)
1272
1273/-- The barycenter as an explicit convex combination in the ambient space. -/
1274lemma coe_sbary {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))) :
1275    ((sbary w : Fin (d + 1) → ℝ)) =
1276      ∑ i, ((m : ℝ) + 1)⁻¹ • ((w i : Fin (d + 1) → ℝ)) := by
1277  funext j
1278  rw [Finset.sum_apply]
1279  simp only [Pi.smul_apply, smul_eq_mul]
1280  rw [← Finset.mul_sum]
1281  rfl
1282
1283lemma sbary_mem_hullOf {m : ℕ} (w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))) :
1284    ((sbary w : Fin (d + 1) → ℝ)) ∈ hullOf w := by
1285  rw [coe_sbary]
1286  refine (convex_convexHull ℝ _).sum_mem (fun i _ => by positivity) ?_
1287    (fun i _ => coe_mem_hullOf w i)
1288  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
1289  push_cast
1290  rw [mul_inv_cancel₀ (by positivity)]
1291
1292/-- Two points of the hull of a tuple with pairwise distances `≤ D` are
1293themselves at distance `≤ D` (maximum principle for the convex `dist`). -/
1294lemma dist_le_of_mem_hullOf {m : ℕ} {w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))}
1295    {D : ℝ} (hw : ∀ i j, dist (w i) (w j) ≤ D)
1296    {x y : Fin (d + 1) → ℝ} (hx : x ∈ hullOf w) (hy : y ∈ hullOf w) :
1297    dist x y ≤ D := by
1298  obtain ⟨x', ⟨i, rfl⟩, hx'⟩ := convexHull_exists_dist_ge hx y
1299  obtain ⟨y', ⟨j, rfl⟩, hy'⟩ := convexHull_exists_dist_ge hy ((w i : Fin (d + 1) → ℝ))
1300  calc dist x y ≤ dist ((w i : Fin (d + 1) → ℝ)) y := hx'
1301    _ = dist y ((w i : Fin (d + 1) → ℝ)) := dist_comm _ _
1302    _ ≤ dist ((w j : Fin (d + 1) → ℝ)) ((w i : Fin (d + 1) → ℝ)) := hy'
1303    _ = dist (w j) (w i) := (Subtype.dist_eq _ _).symm
1304    _ ≤ D := hw j i
1305
1306/-- Key metric estimate: the barycenter of an `m`-tuple with pairwise
1307distances `≤ D` is within `m/(m+1) · D` of every point of the tuple's hull. -/
1308lemma dist_sbary_le {m : ℕ} {w : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))}
1309    {D : ℝ} (hw : ∀ i j, dist (w i) (w j) ≤ D)
1310    {x : Fin (d + 1) → ℝ} (hx : x ∈ hullOf w) :
1311    dist ((sbary w : Fin (d + 1) → ℝ)) x ≤ ((m : ℝ) / (m + 1)) * D := by
1312  obtain ⟨x', ⟨j, rfl⟩, hx'⟩ :=
1313    convexHull_exists_dist_ge hx ((sbary w : Fin (d + 1) → ℝ))
1314  rw [dist_comm] at hx'
1315  refine hx'.trans ?_
1316  show dist ((w j : Fin (d + 1) → ℝ)) ((sbary w : Fin (d + 1) → ℝ)) ≤ _
1317  rw [dist_comm, dist_eq_norm]
1318  have hrep : ((sbary w : Fin (d + 1) → ℝ)) - (w j : Fin (d + 1) → ℝ) =
1319      ∑ i, ((m : ℝ) + 1)⁻¹ •
1320        (((w i : Fin (d + 1) → ℝ)) - ((w j : Fin (d + 1) → ℝ))) := by
1321    funext j'
1322    rw [Pi.sub_apply, Finset.sum_apply]
1323    simp only [Pi.smul_apply, Pi.sub_apply, smul_eq_mul, mul_sub]
1324    rw [Finset.sum_sub_distrib]
1325    have h1 : ∑ i : Fin (m + 1), ((m : ℝ) + 1)⁻¹ * (w i) j' = sbary w j' := by
1326      rw [sbary_apply, Finset.mul_sum]
1327    have h2 : ∑ _i : Fin (m + 1), ((m : ℝ) + 1)⁻¹ * (w j) j' = (w j) j' := by
1328      rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
1329      push_cast
1330      rw [← mul_assoc, mul_inv_cancel₀ (by positivity), one_mul]
1331    rw [h1, h2]
1332  rw [hrep]
1333  calc ‖∑ i, ((m : ℝ) + 1)⁻¹ •
1334        (((w i : Fin (d + 1) → ℝ)) - ((w j : Fin (d + 1) → ℝ)))‖
1335      ≤ ∑ i, ‖((m : ℝ) + 1)⁻¹ •
1336        (((w i : Fin (d + 1) → ℝ)) - ((w j : Fin (d + 1) → ℝ)))‖ :=
1337        norm_sum_le _ _
1338    _ = ∑ i, ((m : ℝ) + 1)⁻¹ *
1339        ‖((w i : Fin (d + 1) → ℝ)) - ((w j : Fin (d + 1) → ℝ))‖ := by
1340        refine Finset.sum_congr rfl fun i _ => ?_
1341        rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (by positivity)]
1342    _ ≤ ((m : ℝ) / (m + 1)) * D := ?_
1343  rw [← Finset.add_sum_erase _ _ (Finset.mem_univ j), sub_self, norm_zero,
1344    mul_zero, zero_add]
1345  have hterm : ∀ i ∈ Finset.univ.erase j,
1346      ((m : ℝ) + 1)⁻¹ * ‖((w i : Fin (d + 1) → ℝ)) - ((w j : Fin (d + 1) → ℝ))‖ ≤
1347        ((m : ℝ) + 1)⁻¹ * D := by
1348    intro i _
1349    refine mul_le_mul_of_nonneg_left ?_ (by positivity)
1350    rw [← dist_eq_norm]
1351    exact hw i j
1352  calc ∑ i ∈ Finset.univ.erase j, ((m : ℝ) + 1)⁻¹ *
1353        ‖((w i : Fin (d + 1) → ℝ)) - ((w j : Fin (d + 1) → ℝ))‖
1354      ≤ (Finset.univ.erase j).card • (((m : ℝ) + 1)⁻¹ * D) :=
1355        Finset.sum_le_card_nsmul _ _ _ hterm
1356    _ = ((m : ℝ) / (m + 1)) * D := by
1357        rw [Finset.card_erase_of_mem (Finset.mem_univ j), Finset.card_univ,
1358          Fintype.card_fin, nsmul_eq_mul, div_eq_mul_inv]
1359        push_cast
1360        ring
1361
1362/-- The contraction ratio is monotone in the degree. -/
1363lemma ratio_mono (n : ℕ) : ((n : ℝ) / (n + 1)) ≤ (((n : ℝ) + 1) / ((n : ℝ) + 2)) := by
1364  rw [div_le_div_iff₀ (by positivity) (by positivity)]
1365  nlinarith [sq_nonneg ((n : ℝ))]
1366
1367/-- **Stage 6 main estimate.** Every piece of the barycentric subdivision of
1368an affine simplex has vertices in the hull of the original tuple, with
1369pairwise distances contracted by the factor `n / (n + 1)`. -/
1370theorem asub_support_bound :
1371    ∀ (n : ℕ) (w : Fin (n + 1) → stdSimplex ℝ (Fin (d + 1))) (D : ℝ), 0 ≤ D →
1372      (∀ i j, dist (w i) (w j) ≤ D) →
1373      ∀ u ∈ ((asub (baryFn d) n) (asimplex w)).support,
1374        (∀ i j, dist (u i) (u j) ≤ ((n : ℝ) / (n + 1)) * D) ∧
1375          ∀ i, ((u i : Fin (d + 1) → ℝ)) ∈ hullOf w
1376  | 0, w, D, hD, hw => by
1377      intro u hu
1378      rw [asub_zero, LinearMap.id_apply, asimplex] at hu
1379      have hmem := Finsupp.support_single_subset hu
1380      rw [Finset.mem_singleton] at hmem
1381      subst hmem
1382      refine ⟨fun i j => ?_, fun i => coe_mem_hullOf u i⟩
1383      have hij : i = j := Fin.ext (by omega)
1384      subst hij
1385      rw [dist_self]
1386      positivity
1387  | n + 1, w, D, hD, hw => by
1388      intro u hu
1389      rw [asub_asimplex] at hu
1390      obtain ⟨v, hv, huv⟩ := support_acone _ _ u hu
1391      subst huv
1392      have hmid : ∀ v' ∈ ((asub (baryFn d) n) (abnd n (asimplex w))).support,
1393          (∀ i j, dist (v' i) (v' j) ≤ ((n : ℝ) / (n + 1)) * D) ∧
1394            ∀ i, ((v' i : Fin (d + 1) → ℝ)) ∈ hullOf w := by
1395        refine support_transport _
1396          (P := fun v' => ∃ j : Fin (n + 2), v' = w ∘ j.succAbove) ?_ _
1397          (support_abnd_asimplex w)
1398        rintro v' ⟨j, rfl⟩ u' hu'
1399        obtain ⟨h1, h2⟩ := asub_support_bound n (w ∘ j.succAbove) D hD
1400          (fun i i' => hw _ _) u' hu'
1401        exact ⟨h1, fun i => hullOf_subset
1402          (fun i' => coe_mem_hullOf w (j.succAbove i')) (h2 i)⟩
1403      obtain ⟨h1, h2⟩ := hmid v hv
1404      have hr : ((n : ℝ) / (n + 1)) * D ≤ (((n + 1 : ℕ) : ℝ) / ((n + 1 : ℕ) + 1)) * D := by
1405        refine mul_le_mul_of_nonneg_right ?_ hD
1406        push_cast
1407        have h := ratio_mono n
1408        rwa [show ((n : ℝ) + 2) = ((n : ℝ) + 1 + 1) by ring] at h
1409      have happx : ∀ i' : Fin (n + 1),
1410          dist (baryFn d w) (v i') ≤ (((n + 1 : ℕ) : ℝ) / ((n + 1 : ℕ) + 1)) * D := by
1411        intro i'
1412        rw [baryFn_apply, Subtype.dist_eq]
1413        have hdist := dist_sbary_le (w := w) hw (h2 i')
1414        refine hdist.trans (le_of_eq ?_)
1415        push_cast
1416        ring
1417      refine ⟨fun i j => ?_, fun i => ?_⟩
1418      · refine Fin.cases ?_ (fun i' => ?_) i
1419        · refine Fin.cases ?_ (fun j' => ?_) j
1420          · rw [Fin.cons_zero, dist_self]
1421            positivity
1422          · rw [Fin.cons_zero, Fin.cons_succ]
1423            exact happx j'
1424        · refine Fin.cases ?_ (fun j' => ?_) j
1425          · rw [Fin.cons_succ, Fin.cons_zero, dist_comm]
1426            exact happx i'
1427          · rw [Fin.cons_succ, Fin.cons_succ]
1428            exact (h1 i' j').trans hr
1429      · refine Fin.cases ?_ (fun i' => ?_) i
1430        · rw [Fin.cons_zero, baryFn_apply]
1431          exact sbary_mem_hullOf w
1432        · rw [Fin.cons_succ]
1433          exact h2 i'
1434
1435/-- Iterated version: `k`-fold subdivision contracts pairwise distances by
1436`(n/(n+1))^k`, keeping all vertices in the hull of the original tuple. -/
1437theorem asubIter_support_bound (k : ℕ) :
1438    ∀ (n : ℕ) (w : Fin (n + 1) → stdSimplex ℝ (Fin (d + 1))) (D : ℝ), 0 ≤ D →
1439      (∀ i j, dist (w i) (w j) ≤ D) →
1440      ∀ u ∈ ((asubIter (baryFn d) k n) (asimplex w)).support,
1441        (∀ i j, dist (u i) (u j) ≤ ((n : ℝ) / (n + 1)) ^ k * D) ∧
1442          ∀ i, ((u i : Fin (d + 1) → ℝ)) ∈ hullOf w := by
1443  induction k with
1444  | zero =>
1445      intro n w D hD hw u hu
1446      rw [asubIter_zero, LinearMap.id_apply, asimplex] at hu
1447      have hmem := Finsupp.support_single_subset hu
1448      rw [Finset.mem_singleton] at hmem
1449      subst hmem
1450      exact ⟨fun i j => by rw [pow_zero, one_mul]; exact hw i j,
1451        fun i => coe_mem_hullOf u i⟩
1452  | succ k IH =>
1453      intro n w D hD hw u hu
1454      rw [asubIter_succ, LinearMap.comp_apply] at hu
1455      refine support_transport (asub (baryFn d) n)
1456        (P := fun v => (∀ i j, dist (v i) (v j) ≤ ((n : ℝ) / (n + 1)) ^ k * D) ∧
1457          ∀ i, ((v i : Fin (d + 1) → ℝ)) ∈ hullOf w)
1458        (Q := fun u => (∀ i j, dist (u i) (u j) ≤ ((n : ℝ) / (n + 1)) ^ (k + 1) * D) ∧
1459          ∀ i, ((u i : Fin (d + 1) → ℝ)) ∈ hullOf w) ?_ _
1460        (IH n w D hD hw) u hu
1461      rintro v ⟨hv1, hv2⟩ u' hu'
1462      obtain ⟨h1, h2⟩ := asub_support_bound n v (((n : ℝ) / (n + 1)) ^ k * D)
1463        (by positivity) hv1 u' hu'
1464      refine ⟨fun i j => ?_, fun i => hullOf_subset hv2 (h2 i)⟩
1465      calc dist (u' i) (u' j)
1466          ≤ ((n : ℝ) / (n + 1)) * (((n : ℝ) / (n + 1)) ^ k * D) := h1 i j
1467        _ = ((n : ℝ) / (n + 1)) ^ (k + 1) * D := by ring
1468
1469/-- Any two points of the standard simplex are at sup-distance `≤ 1`. -/
1470lemma stdSimplex_dist_le_one (x y : stdSimplex ℝ (Fin (d + 1))) : dist x y ≤ 1 := by
1471  rw [Subtype.dist_eq, dist_pi_le_iff zero_le_one]
1472  intro j
1473  rw [Real.dist_eq, abs_sub_le_iff]
1474  have hx := mem_Icc_of_mem_stdSimplex x.2 j
1475  have hy := mem_Icc_of_mem_stdSimplex y.2 j
1476  constructor
1477  · linarith [hx.2, hy.1]
1478  · linarith [hy.2, hx.1]
1479
1480/-- **Stage 6 payoff.** The pieces of the iterated barycentric subdivision of
1481any affine simplex in the standard simplex become uniformly small. -/
1482theorem exists_asubIter_small (n : ℕ) (w : Fin (n + 1) → stdSimplex ℝ (Fin (d + 1)))
1483    {ε : ℝ} (hε : 0 < ε) :
1484    ∃ k, ∀ u ∈ ((asubIter (baryFn d) k n) (asimplex w)).support,
1485      ∀ i j, dist (u i) (u j) < ε := by
1486  have hlt : ((n : ℝ) / (n + 1)) < 1 := by
1487    rw [div_lt_one (by positivity)]
1488    linarith
1489  obtain ⟨k, hk⟩ := exists_pow_lt_of_lt_one hε hlt
1490  refine ⟨k, fun u hu i j => ?_⟩
1491  have hbound := (asubIter_support_bound k n w 1 zero_le_one
1492    (fun i j => stdSimplex_dist_le_one _ _) u hu).1 i j
1493  calc dist (u i) (u j) ≤ ((n : ℝ) / (n + 1)) ^ k * 1 := hbound
1494    _ = ((n : ℝ) / (n + 1)) ^ k := mul_one _
1495    _ < ε := hk
1496
1497end Diameter
1498
1499/-! ## Stage 7: the small-simplices theorem
1500
1501For an open cover `U ∪ V = X` and a singular simplex `σ`, the Lebesgue
1502number of the preimage cover `σ⁻¹U, σ⁻¹V` of the compact metric `Δⁿ`
1503together with the stage 6 decay yields an iterate `k` of the singular
1504subdivision all of whose pieces land in `U` or in `V`.  By
1505`gen_comp_sdOpIter`, the pieces of `sdOpIter X n k` on the generator of `σ`
1506are exactly the `pushSimplex σ u` for `u` in the support of the iterated
1507affine subdivision of the identity tuple, so smallness is stated over that
1508support.  The chain-homotopy witness relating `sdOpIter X n k` to the
1509identity is `tOpIter_chain_homotopy_succ` / `tOpIter_chain_homotopy_zero`. -/
1510
1511section SmallSimplices
1512
1513open SingularPrism
1514
1515variable {X : TopCat.{0}}
1516
1517/-- The affine map of a tuple lands in the tuple's hull. -/
1518lemma affineMap_mem_hullOf {d m : ℕ} (u : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1)))
1519    (x : stdSimplex ℝ (Fin (m + 1))) :
1520    ((affineMap u x : Fin (d + 1) → ℝ)) ∈ hullOf u := by
1521  have hrep : ((affineMap u x : Fin (d + 1) → ℝ)) =
1522      ∑ i, x i • ((u i : Fin (d + 1) → ℝ)) := by
1523    funext j
1524    rw [Finset.sum_apply]
1525    simp only [Pi.smul_apply, smul_eq_mul]
1526    exact affineMap_apply_coe u x j
1527  rw [hrep]
1528  exact (convex_convexHull ℝ _).sum_mem (fun i _ => stdSimplex.zero_le x i)
1529    (stdSimplex.sum_eq_one x) (fun i _ => coe_mem_hullOf u i)
1530
1531/-- Every point of an affine piece is within the piece's vertex spread of
1532its zeroth vertex. -/
1533lemma dist_affineMap_le {d m : ℕ} {u : Fin (m + 1) → stdSimplex ℝ (Fin (d + 1))}
1534    {D : ℝ} (hu : ∀ i j, dist (u i) (u j) ≤ D) (x : stdSimplex ℝ (Fin (m + 1))) :
1535    dist (affineMap u x) (u 0) ≤ D :=
1536  dist_le_of_mem_hullOf hu (affineMap_mem_hullOf u x) (coe_mem_hullOf u 0)
1537
1538/-- **Stage 7: the small-simplices theorem.** For open sets `U, V` covering
1539`X` and any singular `n`-simplex `s`, there is an iterate `k` such that
1540every piece of `sdOpIter X n k` applied to the generator of `s` (i.e. every
1541`pushSimplex σ u` with `u` in the support of the iterated affine
1542subdivision, per `gen_comp_sdOpIter`) has range contained in `U` or in `V`. -/
1543theorem exists_sdOpIter_small {n : ℕ} (U V : Set X) (hU : IsOpen U) (hV : IsOpen V)
1544    (hUV : U ∪ V = Set.univ) (s : Idx X n) :
1545    ∃ k, ∀ u ∈ ((asubIter (baryFn n) k n) (asimplex (idTuple n))).support,
1546      Set.range ⇑(simplexEquiv X n (pushSimplex (simplexEquiv X n s) u)) ⊆ U ∨
1547        Set.range ⇑(simplexEquiv X n (pushSimplex (simplexEquiv X n s) u)) ⊆ V := by
1548  set σ := simplexEquiv X n s with hσ
1549  haveI : CompactSpace (stdSimplex ℝ (Fin (n + 1))) :=
1550    isCompact_iff_compactSpace.mp (isCompact_stdSimplex _)
1551  have hcover : (Set.univ : Set (stdSimplex ℝ (Fin (n + 1)))) ⊆
1552      ⋃ b : Bool, (if b then ⇑σ ⁻¹' U else ⇑σ ⁻¹' V) := by
1553    intro x _
1554    have hmem : σ x ∈ U ∪ V := by rw [hUV]; trivial
1555    rcases hmem with h | h
1556    · exact Set.mem_iUnion.mpr ⟨true, h⟩
1557    · exact Set.mem_iUnion.mpr ⟨false, h⟩
1558  have hopen : ∀ b : Bool, IsOpen (if b then ⇑σ ⁻¹' U else ⇑σ ⁻¹' V) := by
1559    intro b
1560    cases b
1561    · exact hV.preimage σ.continuous
1562    · exact hU.preimage σ.continuous
1563  obtain ⟨δ, hδ, hball⟩ := lebesgue_number_lemma_of_metric isCompact_univ hopen hcover
1564  obtain ⟨k, hk⟩ := exists_asubIter_small n (idTuple n) (half_pos hδ)
1565  refine ⟨k, fun u hu => ?_⟩
1566  obtain ⟨b, hb⟩ := hball (u 0) (Set.mem_univ _)
1567  have himg : Set.range ⇑(σ.comp (affineMap u)) ⊆
1568      (if b then U else V) := by
1569    rintro y ⟨x, rfl⟩
1570    have hdist : dist (affineMap u x) (u 0) < δ := by
1571      have hle := dist_affineMap_le (fun i j => (hk u hu i j).le) x
1572      linarith
1573    have hxball : affineMap u x ∈ Metric.ball (u 0) δ := Metric.mem_ball.mpr hdist
1574    have hpre := hb hxball
1575    cases b
1576    · exact hpre
1577    · exact hpre
1578  rw [simplexEquiv_pushSimplex]
1579  cases b
1580  · exact Or.inr himg
1581  · exact Or.inl himg
1582
1583end SmallSimplices
1584
1585end SingularSubdivision
1586end Foundation
1587end IndisputableMonolith
1588