IndisputableMonolith.Foundation.SingularMayerVietoris

   1/-
   2Mayer-Vietoris for Mathlib's singular homology (with `ℤ` coefficients).
   3
   4Layer 4 of the excision spine (layer 1: `SingularPrism`, homotopy invariance;
   5layer 2: `SingularPair`, the LES of a pair; layer 3: `SingularSubdivision`,
   6barycentric subdivision and the small-simplices theorem).
   7
   8## Contents (staged)
   9
  10* Stage 1: for `U V : Set X`, the small-chains subcomplex `SSC U V` of the
  11  singular chain complex `SC X`, generated in each degree by the singular
  12  simplices whose range lies in `U` or in `V`; the degreewise split-mono
  13  inclusion `smallι : SSC U V ⟶ SC X`.
  14* Stage 2: the small-chains theorem (Hatcher, Prop 2.21): for open `U, V`
  15  covering `X` the inclusion induces an isomorphism on homology in every
  16  degree (`smallι_isIso_homologyMap`, `smallChainsHomologyIso`), via the
  17  subdivision operators and the telescoped homotopies of
  18  `SingularSubdivision`.
  19* Stage 3: the Mayer-Vietoris short exact sequence of chain complexes
  20  `0 ⟶ C_*(U ∩ V) ⟶ C_*(U) ⊞ C_*(V) ⟶ C^{U,V}_*(X) ⟶ 0` (`mvSES`,
  21  `mvSES_shortExact`; no openness/covering hypotheses needed).  Left map
  22  `x ↦ (i_* x, −j_* x)` (`mvα`), right map `(a, b) ↦ k_* a + l_* b`
  23  (`mvβ`); degreewise exactness by coordinate tracking on the free basis
  24  (`coordAt`, `suppOf`, `mv_middle_exact`).
  25* Stage 4: the honest Mayer-Vietoris long exact sequence on Mathlib
  26  singular homology of the spaces, with `H_n(SSC)` transported to `H_n(X)`
  27  across the Stage-2 isomorphism and `H_n(C(U) ⊞ C(V))` split by additivity
  28  of the homology functor (`homologyBiprodIso`):
  29  `⋯ → H_n(U ∩ V) → H_n(U) ⊞ H_n(V) → H_n(X) → H_{n−1}(U ∩ V) → ⋯`.
  30  Maps `mvPair` (from the space-level inclusions `U ∩ V ↪ U, V`), `mvSum`
  31  (from `U, V ↪ X`), connecting map `mvδ`; exactness `mv_exact₁/₂/₃`;
  32  degree-0 tail `mvSum_epi_zero`; sanity lock `mvSum_epi_of_left_univ`
  33  (for `U = univ` the sum map is epi in every degree, since its first
  34  component comes from the homeomorphism `univ ≃ X`).
  35
  36## Frontier (layer 5, not yet formalized)
  37
  38* `H_*(Sⁿ)` by Mayer-Vietoris induction: cover `Sⁿ` by two open
  39  hemispheres `U, V` (each contractible, `U ∩ V ≃ Sⁿ⁻¹` up to homotopy),
  40  use layer-1 homotopy invariance to evaluate the `H_*(U)`, `H_*(V)` spots
  41  and this file's `mv_exact₁/₂/₃` + `mvδ` to walk the induction.  Missing
  42  ingredients: `H_*(pt)` (a direct computation on the singular complex of
  43  a point), homotopy equivalences between the hemispheres/pt and
  44  `U ∩ V`/`Sⁿ⁻¹`, and the two-space case split in degree `0`
  45  (`mvSum_epi_zero` supplies the tail).
  46
  47## Instance-diamond note (load-bearing)
  48
  49For `R = ℤ` every `ModuleCat ℤ` carrier has two `Module ℤ` instances
  50(`isModule` and `AddCommGroup.toIntModule`), propositionally but not
  51definitionally equal, and synthesis prefers the generic one. This file
  52deprioritizes `AddCommGroup.toIntModule` and `SubNegMonoid.toZSMul` locally;
  53any continuation working elementwise in these chain groups must keep those
  54two local-attribute lines.
  55-/
  56import Mathlib.Algebra.Homology.HomologicalComplexAbelian
  57import Mathlib.Algebra.Homology.HomologicalComplexBiprod
  58import Mathlib.Algebra.Homology.HomologySequence
  59import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
  60import Mathlib.Algebra.Category.ModuleCat.Products
  61import Mathlib.Algebra.Category.ModuleCat.Biproducts
  62import IndisputableMonolith.Foundation.SingularPrism
  63import IndisputableMonolith.Foundation.SingularPair
  64import IndisputableMonolith.Foundation.SingularSubdivision
  65
  66namespace IndisputableMonolith
  67namespace Foundation
  68namespace SingularMayerVietoris
  69
  70open CategoryTheory Category Limits AlgebraicTopology Simplicial Opposite
  71open SingularPrism SingularSubdivision
  72
  73attribute [local instance 10] Classical.decEq
  74
  75/- For `R = ℤ` every carrier has two `Module ℤ` instances: the canonical one
  76recorded in the `ModuleCat` structure and the generic
  77`AddCommGroup.toIntModule`. They are propositionally but not definitionally
  78equal, and instance synthesis prefers the generic one, which breaks
  79elementwise reasoning. Deprioritizing the generic instance restores the
  80canonical one everywhere in this file. -/
  81attribute [local instance 0] AddCommGroup.toIntModule
  82attribute [local instance 0] SubNegMonoid.toZSMul
  83
  84/-! ## Stage 1: the small-chains subcomplex -/
  85
  86variable {X : TopCat.{0}}
  87
  88/-- A singular `n`-simplex of `X` is *small* (relative to the pair of subsets
  89`U, V`) when its range lies in `U` or in `V`. -/
  90def Small (U V : Set X) {n : ℕ} (s : Idx X n) : Prop :=
  91  Set.range ⇑(simplexEquiv X n s) ⊆ U ∨ Set.range ⇑(simplexEquiv X n s) ⊆ V
  92
  93/-- Faces of small simplices are small. -/
  94lemma Small.δ {U V : Set X} {n : ℕ} {s : Idx X (n + 1)} (hs : Small U V s)
  95    (k : Fin (n + 2)) : Small U V ((TopCat.toSSet.obj X).δ k s) := by
  96  have hrange : Set.range ⇑(simplexEquiv X n ((TopCat.toSSet.obj X).δ k s)) ⊆
  97      Set.range ⇑(simplexEquiv X (n + 1) s) := by
  98    rw [simplexEquiv_δ, ContinuousMap.coe_comp]
  99    exact Set.range_comp_subset_range _ _
 100  rcases hs with h | h
 101  · exact Or.inl (hrange.trans h)
 102  · exact Or.inr (hrange.trans h)
 103
 104variable (U V : Set X)
 105
 106/-- The index type of the degree-`n` small chain group: small singular
 107`n`-simplices. -/
 108def SIdx (n : ℕ) : Type := { s : Idx X n // Small U V s }
 109
 110/-- The degree-`n` small chain group: the free `ℤ`-module on the small
 111singular `n`-simplices, presented as a coproduct. -/
 112noncomputable abbrev sCgrp (n : ℕ) : ModuleCat.{0} ℤ :=
 113  ∐ fun _ : SIdx U V n => ModuleCat.of ℤ ℤ
 114
 115/-- The generator of the small chain group attached to a small simplex. -/
 116noncomputable def sgen (n : ℕ) (t : SIdx U V n) : ModuleCat.of ℤ ℤ ⟶ sCgrp U V n :=
 117  Sigma.ι (fun _ : SIdx U V n => ModuleCat.of ℤ ℤ) t
 118
 119/-- The degree-`n` inclusion of the small chain group into the singular
 120chain group. -/
 121noncomputable def sInc (n : ℕ) : sCgrp U V n ⟶ Cgrp X n :=
 122  Sigma.desc fun t => gen X n t.1
 123
 124lemma sgen_sInc {n : ℕ} (t : SIdx U V n) :
 125    sgen U V n t ≫ sInc U V n = gen X n t.1 :=
 126  Sigma.ι_desc _ _
 127
 128open Classical in
 129/-- The retraction of the degree-`n` inclusion: a small simplex goes to its
 130small generator, everything else goes to `0`. -/
 131noncomputable def sRet (n : ℕ) : Cgrp X n ⟶ sCgrp U V n :=
 132  Sigma.desc fun s =>
 133    if h : Small U V s then sgen U V n ⟨s, h⟩ else 0
 134
 135lemma sInc_comp_sRet (n : ℕ) : sInc U V n ≫ sRet U V n = 𝟙 (sCgrp U V n) := by
 136  apply Sigma.hom_ext
 137  intro t
 138  show sgen U V n t ≫ sInc U V n ≫ sRet U V n = sgen U V n t ≫ 𝟙 (sCgrp U V n)
 139  rw [Category.comp_id, ← assoc, sgen_sInc]
 140  show Sigma.ι (fun _ : Idx X n => ModuleCat.of ℤ ℤ) t.1 ≫ sRet U V n = sgen U V n t
 141  unfold sRet
 142  rw [Sigma.ι_desc, dif_pos t.2]
 143  congr 1
 144
 145/-- The degree-`n` inclusion is a (split) monomorphism. -/
 146lemma sInc_mono (n : ℕ) : Mono (sInc U V n) :=
 147  mono_of_mono_fac (sInc_comp_sRet U V n)
 148
 149/-- The boundary of the small chain complex: the alternating sum of faces,
 150which are small by `Small.δ`. -/
 151noncomputable def sBnd (n : ℕ) : sCgrp U V (n + 1) ⟶ sCgrp U V n :=
 152  Sigma.desc fun t => ∑ k : Fin (n + 2),
 153    (-1 : ℤ) ^ (k : ℕ) • sgen U V n ⟨(TopCat.toSSet.obj X).δ k t.1, t.2.δ k⟩
 154
 155lemma sgen_sBnd {n : ℕ} (t : SIdx U V (n + 1)) :
 156    sgen U V (n + 1) t ≫ sBnd U V n = ∑ k : Fin (n + 2),
 157      (-1 : ℤ) ^ (k : ℕ) • sgen U V n ⟨(TopCat.toSSet.obj X).δ k t.1, t.2.δ k⟩ :=
 158  Sigma.ι_desc _ _
 159
 160/-- The inclusion intertwines the small boundary and the singular boundary. -/
 161lemma sBnd_comp_sInc (n : ℕ) :
 162    sBnd U V n ≫ sInc U V n = sInc U V (n + 1) ≫ bnd X n := by
 163  apply Sigma.hom_ext
 164  intro t
 165  rw [← assoc, ← assoc]
 166  show (sgen U V (n + 1) t ≫ sBnd U V n) ≫ sInc U V n =
 167    (sgen U V (n + 1) t ≫ sInc U V (n + 1)) ≫ bnd X n
 168  rw [sgen_sBnd, sgen_sInc, gen_d, Preadditive.sum_comp]
 169  refine Finset.sum_congr rfl fun k _ => ?_
 170  rw [Preadditive.zsmul_comp]
 171  congr 1
 172  exact sgen_sInc U V _
 173
 174/-- The small boundary squares to zero. -/
 175lemma sBnd_comp_sBnd (n : ℕ) : sBnd U V (n + 1) ≫ sBnd U V n = 0 := by
 176  have := sInc_mono U V n
 177  rw [← cancel_mono (sInc U V n), zero_comp, assoc, sBnd_comp_sInc,
 178    ← assoc, sBnd_comp_sInc, assoc]
 179  show sInc U V (n + 2) ≫ (SC X).d (n + 2) (n + 1) ≫ (SC X).d (n + 1) n = 0
 180  rw [HomologicalComplex.d_comp_d, comp_zero]
 181
 182/-- **Stage 1.** The small-chains subcomplex `C^{U,V}_*(X)`: the chain
 183complex of chains generated by singular simplices landing in `U` or in
 184`V`. -/
 185noncomputable def SSC : ChainComplex (ModuleCat.{0} ℤ) ℕ :=
 186  ChainComplex.of (sCgrp U V) (sBnd U V) (sBnd_comp_sBnd U V)
 187
 188@[simp] lemma SSC_X (n : ℕ) : (SSC U V).X n = sCgrp U V n := rfl
 189
 190lemma SSC_d (n : ℕ) : (SSC U V).d (n + 1) n = sBnd U V n :=
 191  ChainComplex.of_d _ _ _ _
 192
 193/-- The inclusion of the small-chains subcomplex into the singular chain
 194complex, as a chain map. -/
 195noncomputable def smallι : SSC U V ⟶ SC X where
 196  f n := sInc U V n
 197  comm' := by
 198    rintro i j (rfl : j + 1 = i)
 199    rw [SSC_d]
 200    exact (sBnd_comp_sInc U V j).symm
 201
 202@[simp] lemma smallι_f (n : ℕ) : (smallι U V).f n = sInc U V n := rfl
 203
 204/-- The inclusion of the small-chains subcomplex is a monomorphism of chain
 205complexes. -/
 206lemma smallι_mono : Mono (smallι U V) :=
 207  HomologicalComplex.mono_of_mono_f _ fun n => sInc_mono U V n
 208
 209/-! ## Stage 2 toolkit A: elements of free coproducts of copies of `ℤ` -/
 210
 211section Elements
 212
 213/-- Elementwise `ℤ`-linearity of a `ModuleCat` morphism (stated through the
 214underlying linear map, to avoid instance-resolution issues on carriers). -/
 215lemma mapSmul {M N : ModuleCat.{0} ℤ} (φ : M ⟶ N) (c : ℤ) (x : M) :
 216    φ (c • x) = c • φ x :=
 217  φ.hom.map_smul c x
 218
 219lemma zeroApp {M N : ModuleCat.{0} ℤ} (x : M) : (0 : M ⟶ N) x = 0 := by
 220  show (0 : M ⟶ N).hom x = 0
 221  rw [ModuleCat.hom_zero]
 222  rfl
 223
 224/-- Evaluation at `1 : ℤ` of morphisms out of `ℤ`, as a linear map. -/
 225noncomputable def ev1 {M : ModuleCat.{0} ℤ} : (ModuleCat.of ℤ ℤ ⟶ M) →ₗ[ℤ] M where
 226  toFun f := f (1 : ℤ)
 227  map_add' _ _ := rfl
 228  map_smul' _ _ := rfl
 229
 230@[simp] lemma ev1_apply {M : ModuleCat.{0} ℤ} (f : ModuleCat.of ℤ ℤ ⟶ M) :
 231    ev1 f = f (1 : ℤ) := rfl
 232
 233variable {κ : Type}
 234
 235/-- The generating element of the free `ℤ`-module `∐_κ ℤ` attached to an
 236index. -/
 237noncomputable def unitOf (i : κ) : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ) :=
 238  Sigma.ι (fun _ : κ => ModuleCat.of ℤ ℤ) i (1 : ℤ)
 239
 240lemma comp_unitOf {M : ModuleCat.{0} ℤ}
 241    (φ : (∐ fun _ : κ => ModuleCat.of ℤ ℤ) ⟶ M) (i : κ) :
 242    φ (unitOf i) = ev1 (Sigma.ι (fun _ : κ => ModuleCat.of ℤ ℤ) i ≫ φ) := by
 243  rw [ev1_apply, ModuleCat.comp_apply]
 244  rfl
 245
 246/-- The generating elements span the free module `∐_κ ℤ`. -/
 247lemma span_unitOf_eq_top :
 248    Submodule.span ℤ (Set.range (unitOf (κ := κ))) = ⊤ := by
 249  rw [Submodule.eq_top_iff']
 250  intro z
 251  set e := ModuleCat.coprodIsoDirectSum (fun _ : κ => ModuleCat.of ℤ ℤ) with he
 252  have h1 : e.inv (e.hom z) = z := by
 253    rw [← ModuleCat.comp_apply, e.hom_inv_id, ModuleCat.id_apply]
 254  have h2 : e.hom z =
 255      ∑ i ∈ (e.hom z).support, DirectSum.lof ℤ κ (fun _ => ℤ) i ((e.hom z) i) := by
 256    conv_lhs => rw [← DirectSum.sum_support_of (e.hom z)]
 257    refine Finset.sum_congr rfl fun i _ => ?_
 258    rw [DirectSum.lof_eq_of]
 259  have h3 : z = ∑ i ∈ (e.hom z).support, ((e.hom z) i) • unitOf i := by
 260    conv_lhs => rw [← h1]
 261    conv_lhs => rw [h2]
 262    rw [map_sum]
 263    refine Finset.sum_congr rfl fun i _ => ?_
 264    have h4 : DirectSum.lof ℤ κ (fun _ => ℤ) i ((e.hom z) i) =
 265        ((e.hom z) i) • DirectSum.lof ℤ κ (fun _ => ℤ) i (1 : ℤ) := by
 266      rw [← map_smul, smul_eq_mul, mul_one]
 267    rw [h4, mapSmul]
 268    congr 1
 269    rw [he]
 270    exact ModuleCat.lof_coprodIsoDirectSum_inv_apply
 271      (fun _ : κ => ModuleCat.of ℤ ℤ) i (1 : ℤ)
 272  rw [h3]
 273  exact Submodule.sum_mem _ fun i _ =>
 274    Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
 275
 276/-- Induction principle: to prove a property of all elements of `∐_κ ℤ`
 277closed under `0`, `+`, `ℤ • ·`, it suffices to prove it for the generating
 278elements. -/
 279lemma freeInduction {p : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ) → Prop}
 280    (unit : ∀ i : κ, p (unitOf i)) (zero : p 0)
 281    (add : ∀ x y, p x → p y → p (x + y))
 282    (smulz : ∀ (c : ℤ) (x), p x → p (c • x))
 283    (z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) : p z := by
 284  have hz : z ∈ Submodule.span ℤ (Set.range (unitOf (κ := κ))) := by
 285    rw [span_unitOf_eq_top]; trivial
 286  refine Submodule.span_induction ?_ zero (fun x y _ _ hx hy => add x y hx hy)
 287    (fun c x _ hx => smulz c x hx) hz
 288  rintro _ ⟨i, rfl⟩
 289  exact unit i
 290
 291end Elements
 292
 293/-! ## Stage 2 toolkit B: the small span and support tracking -/
 294
 295section SmallSpan
 296
 297/-- The generating element of the singular chain group attached to a
 298singular simplex. -/
 299noncomputable def genUnit (X : TopCat.{0}) (n : ℕ) (s : Idx X n) : Cgrp X n :=
 300  unitOf (κ := Idx X n) s
 301
 302lemma genUnit_eq (X : TopCat.{0}) (n : ℕ) (s : Idx X n) :
 303    genUnit X n s = gen X n s (1 : ℤ) := rfl
 304
 305/-- The submodule of small chains inside the singular chain group. -/
 306noncomputable def smallSpan (U V : Set X) (n : ℕ) : Submodule ℤ (Cgrp X n) :=
 307  Submodule.span ℤ {z | ∃ s : Idx X n, Small U V s ∧ z = genUnit X n s}
 308
 309lemma genUnit_mem_smallSpan {U V : Set X} {n : ℕ} {s : Idx X n}
 310    (hs : Small U V s) : genUnit X n s ∈ smallSpan U V n :=
 311  Submodule.subset_span ⟨s, hs, rfl⟩
 312
 313/-- The generating element of the small chain group attached to a small
 314simplex. -/
 315noncomputable def sUnit (U V : Set X) (n : ℕ) (t : SIdx U V n) : ↥(sCgrp U V n) :=
 316  unitOf (κ := SIdx U V n) t
 317
 318lemma sInc_sUnit {U V : Set X} {n : ℕ} (t : SIdx U V n) :
 319    sInc U V n (sUnit U V n t) = genUnit X n t.1 := by
 320  show sInc U V n (unitOf t) = genUnit X n t.1
 321  rw [comp_unitOf]
 322  have h2 : Sigma.ι (fun _ : SIdx U V n => ModuleCat.of ℤ ℤ) t ≫ sInc U V n =
 323      gen X n t.1 := sgen_sInc U V t
 324  rw [h2]
 325  rfl
 326
 327/-- Elementwise injectivity of the degree-`n` inclusion. -/
 328lemma sInc_injective (U V : Set X) (n : ℕ) :
 329    Function.Injective (sInc U V n) := by
 330  intro a b hab
 331  have h := congrArg (sRet U V n) hab
 332  rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply, sInc_comp_sRet,
 333    ModuleCat.id_apply, ModuleCat.id_apply] at h
 334  exact h
 335
 336/-- The inclusion maps small chains into the small span. -/
 337lemma sInc_mem_smallSpan (U V : Set X) (n : ℕ) (z' : ↥(sCgrp U V n)) :
 338    sInc U V n z' ∈ smallSpan U V n := by
 339  induction z' using freeInduction with
 340  | unit t =>
 341      have h : sInc U V n (sUnit U V n t) = genUnit X n t.1 := sInc_sUnit t
 342      rw [show (unitOf t : ↥(sCgrp U V n)) = sUnit U V n t from rfl, h]
 343      exact genUnit_mem_smallSpan t.2
 344  | zero => rw [map_zero]; exact Submodule.zero_mem _
 345  | add x y hx hy => rw [map_add]; exact Submodule.add_mem _ hx hy
 346  | smulz c x hx => rw [mapSmul]; exact Submodule.smul_mem _ _ hx
 347
 348/-- Membership of small chains in the range of the inclusion. -/
 349lemma exists_sInc_eq {U V : Set X} {n : ℕ} {z : Cgrp X n}
 350    (hz : z ∈ smallSpan U V n) : ∃ z' : ↥(sCgrp U V n), sInc U V n z' = z := by
 351  refine Submodule.span_induction ?_ ?_ ?_ ?_ hz
 352  · rintro _ ⟨s, hs, rfl⟩
 353    exact ⟨sUnit U V n ⟨s, hs⟩, sInc_sUnit ⟨s, hs⟩⟩
 354  · exact ⟨0, map_zero _⟩
 355  · rintro x y _ _ ⟨a, ha⟩ ⟨b, hb⟩
 356    exact ⟨a + b, by rw [map_add, ha, hb]⟩
 357  · rintro c x _ ⟨a, ha⟩
 358    exact ⟨c • a, by rw [mapSmul, ha]⟩
 359
 360/-- Evaluation of an affine chain along `σ` lands in the small span as soon
 361as every support piece pushes to a small simplex. -/
 362lemma toChain_one_mem_smallSpan {U V : Set X} {n m : ℕ}
 363    (σ : C(stdSimplex ℝ (Fin (n + 1)), X)) (c : AC (stdSimplex ℝ (Fin (n + 1))) m)
 364    (h : ∀ w ∈ c.support, Small U V (pushSimplex σ w)) :
 365    ev1 (toChain σ m c) ∈ smallSpan U V m := by
 366  rw [toChain, Finsupp.linearCombination_apply, Finsupp.sum, map_sum]
 367  refine Submodule.sum_mem _ fun w hw => ?_
 368  rw [map_zsmul]
 369  exact zsmul_mem (genUnit_mem_smallSpan (h w hw)) _
 370
 371/-- Pushing a simplex along an affine piece keeps it inside a small
 372simplex's range: smallness is inherited. -/
 373lemma small_pushSimplex {U V : Set X} {n m : ℕ} {s : Idx X n}
 374    (hs : Small U V s) (w : Fin (m + 1) → stdSimplex ℝ (Fin (n + 1))) :
 375    Small U V (pushSimplex (simplexEquiv X n s) w) := by
 376  have hrange : Set.range ⇑(simplexEquiv X m (pushSimplex (simplexEquiv X n s) w)) ⊆
 377      Set.range ⇑(simplexEquiv X n s) := by
 378    rw [simplexEquiv_pushSimplex, ContinuousMap.coe_comp]
 379    exact Set.range_comp_subset_range _ _
 380  rcases hs with h | h
 381  · exact Or.inl (hrange.trans h)
 382  · exact Or.inr (hrange.trans h)
 383
 384/-- The singular subdivision operator preserves the small span. -/
 385lemma sdOp_mem_smallSpan {U V : Set X} {n : ℕ} {z : Cgrp X n}
 386    (hz : z ∈ smallSpan U V n) : sdOp X n z ∈ smallSpan U V n := by
 387  refine Submodule.span_induction ?_ ?_ ?_ ?_ hz
 388  · rintro _ ⟨s, hs, rfl⟩
 389    rw [genUnit_eq, ← ModuleCat.comp_apply, gen_sdOp]
 390    show ev1 (toChain (simplexEquiv X n s) n
 391      (asub (baryFn n) n (asimplex (idTuple n)))) ∈ smallSpan U V n
 392    exact toChain_one_mem_smallSpan _ _ fun w _ => small_pushSimplex hs w
 393  · rw [map_zero]; exact Submodule.zero_mem _
 394  · intro x y _ _ hx hy
 395    rw [map_add]; exact Submodule.add_mem _ hx hy
 396  · intro c x _ hx
 397    rw [mapSmul]; exact Submodule.smul_mem _ _ hx
 398
 399/-- The subdivision homotopy maps the small span into the small span one
 400degree up. -/
 401lemma tOp_mem_smallSpan {U V : Set X} {n : ℕ} {z : Cgrp X n}
 402    (hz : z ∈ smallSpan U V n) : tOp X n z ∈ smallSpan U V (n + 1) := by
 403  refine Submodule.span_induction ?_ ?_ ?_ ?_ hz
 404  · rintro _ ⟨s, hs, rfl⟩
 405    rw [genUnit_eq, ← ModuleCat.comp_apply, gen_tOp]
 406    show ev1 (toChain (simplexEquiv X n s) (n + 1)
 407      (atee (baryFn n) n (asimplex (idTuple n)))) ∈ smallSpan U V (n + 1)
 408    exact toChain_one_mem_smallSpan _ _ fun w _ => small_pushSimplex hs w
 409  · rw [map_zero]; exact Submodule.zero_mem _
 410  · intro x y _ _ hx hy
 411    rw [map_add]; exact Submodule.add_mem _ hx hy
 412  · intro c x _ hx
 413    rw [mapSmul]; exact Submodule.smul_mem _ _ hx
 414
 415/-- Iterated subdivision preserves the small span. -/
 416lemma sdOpIter_mem_smallSpan {U V : Set X} {n : ℕ} (k : ℕ) {z : Cgrp X n}
 417    (hz : z ∈ smallSpan U V n) : sdOpIter X n k z ∈ smallSpan U V n := by
 418  induction k with
 419  | zero => rw [sdOpIter_zero, ModuleCat.id_apply]; exact hz
 420  | succ k IH =>
 421      rw [sdOpIter_succ, ModuleCat.comp_apply]
 422      exact sdOp_mem_smallSpan IH
 423
 424/-- The telescoped homotopy maps the small span into the small span one
 425degree up. -/
 426lemma tOpIter_mem_smallSpan {U V : Set X} {n : ℕ} :
 427    ∀ (k : ℕ) {z : Cgrp X n}, z ∈ smallSpan U V n →
 428      tOpIter X n k z ∈ smallSpan U V (n + 1)
 429  | 0, z, _ => by
 430      rw [tOpIter_zero]
 431      show (0 : Cgrp X n ⟶ Cgrp X (n + 1)) z ∈ _
 432      rw [zeroApp]
 433      exact Submodule.zero_mem _
 434  | k + 1, z, hz => by
 435      rw [tOpIter_succ]
 436      show (tOp X n + sdOp X n ≫ tOpIter X n k) z ∈ _
 437      have hadd : (tOp X n + sdOp X n ≫ tOpIter X n k) z =
 438          tOp X n z + (sdOp X n ≫ tOpIter X n k) z := rfl
 439      rw [hadd, ModuleCat.comp_apply]
 440      exact Submodule.add_mem _ (tOp_mem_smallSpan hz)
 441        (tOpIter_mem_smallSpan k (sdOp_mem_smallSpan hz))
 442
 443/-- Additivity of the subdivision iterate. -/
 444lemma sdOpIter_add (X : TopCat.{0}) (n a b : ℕ) :
 445    sdOpIter X n (a + b) = sdOpIter X n a ≫ sdOpIter X n b := by
 446  induction b with
 447  | zero => rw [Nat.add_zero, sdOpIter_zero, Category.comp_id]
 448  | succ b IH =>
 449      rw [show a + (b + 1) = (a + b) + 1 from rfl, sdOpIter_succ, IH,
 450        sdOpIter_succ, Category.assoc]
 451
 452/-- **Uniform smallness.** For open `U, V` covering `X`, every singular
 453chain admits an iterate of the subdivision landing in the small span. -/
 454lemma exists_sdOpIter_mem_smallSpan {U V : Set X} (hU : IsOpen U) (hV : IsOpen V)
 455    (hUV : U ∪ V = Set.univ) {n : ℕ} (z : Cgrp X n) :
 456    ∃ k, sdOpIter X n k z ∈ smallSpan U V n := by
 457  induction z using freeInduction with
 458  | unit s =>
 459      obtain ⟨k, hk⟩ := exists_sdOpIter_small U V hU hV hUV s
 460      refine ⟨k, ?_⟩
 461      have h1 : sdOpIter X n k (unitOf s) = ev1 (gen X n s ≫ sdOpIter X n k) := by
 462        rw [show unitOf (κ := Idx X n) s = genUnit X n s from rfl, genUnit_eq,
 463          ← ModuleCat.comp_apply]
 464        rfl
 465      rw [h1, gen_comp_sdOpIter]
 466      exact toChain_one_mem_smallSpan _ _ fun w hw => hk w hw
 467  | zero => exact ⟨0, by rw [map_zero]; exact Submodule.zero_mem _⟩
 468  | add x y hx hy =>
 469      obtain ⟨k₁, h₁⟩ := hx
 470      obtain ⟨k₂, h₂⟩ := hy
 471      refine ⟨k₁ + k₂, ?_⟩
 472      rw [map_add]
 473      refine Submodule.add_mem _ ?_ ?_
 474      · rw [sdOpIter_add, ModuleCat.comp_apply]
 475        exact sdOpIter_mem_smallSpan k₂ h₁
 476      · rw [Nat.add_comm k₁ k₂, sdOpIter_add, ModuleCat.comp_apply]
 477        exact sdOpIter_mem_smallSpan k₁ h₂
 478  | smulz c x hx =>
 479      obtain ⟨k, hk⟩ := hx
 480      exact ⟨k, by rw [mapSmul]; exact Submodule.smul_mem _ _ hk⟩
 481
 482/-- Elementwise telescoped homotopy identity in positive degrees, on
 483cycles. -/
 484lemma sub_sdOpIter_eq_bnd_succ {n k : ℕ} (z : Cgrp X (n + 1))
 485    (hz : bnd X n z = 0) :
 486    z - sdOpIter X (n + 1) k z = bnd X (n + 1) (tOpIter X (n + 1) k z) := by
 487  have h := congrArg (fun f : Cgrp X (n + 1) ⟶ Cgrp X (n + 1) => f z)
 488    (tOpIter_chain_homotopy_succ X n k)
 489  have h1 : (bnd X n ≫ tOpIter X n k + tOpIter X (n + 1) k ≫ bnd X (n + 1)) z =
 490      tOpIter X n k (bnd X n z) + bnd X (n + 1) (tOpIter X (n + 1) k z) := by
 491    show (bnd X n ≫ tOpIter X n k) z + (tOpIter X (n + 1) k ≫ bnd X (n + 1)) z = _
 492    rw [ModuleCat.comp_apply, ModuleCat.comp_apply]
 493  have h2 : (𝟙 (Cgrp X (n + 1)) - sdOpIter X (n + 1) k) z =
 494      z - sdOpIter X (n + 1) k z := by
 495    show (𝟙 (Cgrp X (n + 1))) z - sdOpIter X (n + 1) k z = _
 496    rw [ModuleCat.id_apply]
 497  simp only [h1, h2] at h
 498  rw [hz, map_zero, zero_add] at h
 499  exact h.symm
 500
 501/-- Elementwise telescoped homotopy identity in degree `0`. -/
 502lemma sub_sdOpIter_eq_bnd_zero {k : ℕ} (z : Cgrp X 0) :
 503    z - sdOpIter X 0 k z = bnd X 0 (tOpIter X 0 k z) := by
 504  have h := congrArg (fun f : Cgrp X 0 ⟶ Cgrp X 0 => f z)
 505    (tOpIter_chain_homotopy_zero X k)
 506  have h1 : (tOpIter X 0 k ≫ bnd X 0) z = bnd X 0 (tOpIter X 0 k z) :=
 507    ModuleCat.comp_apply _ _ _
 508  have h2 : (𝟙 (Cgrp X 0) - sdOpIter X 0 k) z = z - sdOpIter X 0 k z := by
 509    show (𝟙 (Cgrp X 0)) z - sdOpIter X 0 k z = _
 510    rw [ModuleCat.id_apply]
 511  simp only [h1, h2] at h
 512  exact h.symm
 513
 514/-- Elementwise chain-map property of the subdivision iterate. -/
 515lemma sdOpIter_bnd_elem {n k : ℕ} (w : Cgrp X (n + 1)) :
 516    bnd X n (sdOpIter X (n + 1) k w) = sdOpIter X n k (bnd X n w) := by
 517  have h := congrArg (fun f : Cgrp X (n + 1) ⟶ Cgrp X n => f w)
 518    (sdOpIter_comp_bnd X n k)
 519  simpa only [ModuleCat.comp_apply] using h
 520
 521/-- Elementwise telescoped homotopy identity in every degree, on
 522boundaries. -/
 523lemma sub_sdOpIter_eq_bnd_of_boundary {n : ℕ} (k : ℕ) (z : Cgrp X n)
 524    (w : Cgrp X (n + 1)) (hw : z = bnd X n w) :
 525    z - sdOpIter X n k z = bnd X n (tOpIter X n k z) := by
 526  cases n with
 527  | zero => exact sub_sdOpIter_eq_bnd_zero z
 528  | succ m =>
 529      refine sub_sdOpIter_eq_bnd_succ z ?_
 530      rw [hw, ← ModuleCat.comp_apply]
 531      have hdd : bnd X (m + 1) ≫ bnd X m = 0 := by
 532        show (SC X).d (m + 2) (m + 1) ≫ (SC X).d (m + 1) m = 0
 533        exact HomologicalComplex.d_comp_d _ _ _ _
 534      rw [hdd]
 535      exact zeroApp w
 536
 537end SmallSpan
 538
 539/-! ## Stage 2 toolkit C: a concrete homology-isomorphism criterion for
 540short complexes of `ℤ`-modules -/
 541
 542section HomologyCriterion
 543
 544open ShortComplex
 545
 546variable {S T : ShortComplex (ModuleCat.{0} ℤ)}
 547
 548lemma τ₂_maps_ker (ψ : S ⟶ T) : ∀ x ∈ LinearMap.ker S.g.hom,
 549    ψ.τ₂ x ∈ LinearMap.ker T.g.hom := by
 550  intro x hx
 551  rw [LinearMap.mem_ker] at hx ⊢
 552  have h := congrArg (fun f : S.X₂ ⟶ T.X₃ => f x) ψ.comm₂₃
 553  simp only [ModuleCat.comp_apply] at h
 554  show T.g (ψ.τ₂ x) = 0
 555  rw [h, show S.g x = (0 : S.X₃) from hx, map_zero]
 556
 557/-- The induced map on concrete cycles. -/
 558noncomputable def kerMap (ψ : S ⟶ T) :
 559    ↥(LinearMap.ker S.g.hom) →ₗ[ℤ] ↥(LinearMap.ker T.g.hom) :=
 560  LinearMap.restrict ψ.τ₂.hom (τ₂_maps_ker ψ)
 561
 562@[simp] lemma kerMap_coe (ψ : S ⟶ T) (x : ↥(LinearMap.ker S.g.hom)) :
 563    (kerMap ψ x : T.X₂) = ψ.τ₂ (x : S.X₂) := rfl
 564
 565lemma kerMap_range_le (ψ : S ⟶ T) :
 566    LinearMap.range S.moduleCatToCycles ≤
 567      (LinearMap.range T.moduleCatToCycles).comap (kerMap ψ) := by
 568  rintro _ ⟨a, rfl⟩
 569  refine ⟨ψ.τ₁ a, ?_⟩
 570  apply Subtype.ext
 571  show T.f (ψ.τ₁ a) = ψ.τ₂ (S.f a)
 572  have h := congrArg (fun f : S.X₁ ⟶ T.X₂ => f a) ψ.comm₁₂
 573  simpa only [ModuleCat.comp_apply] using h
 574
 575/-- The induced map on concrete homology. -/
 576noncomputable def quotMap (ψ : S ⟶ T) :
 577    (↥(LinearMap.ker S.g.hom) ⧸ LinearMap.range S.moduleCatToCycles) →ₗ[ℤ]
 578      (↥(LinearMap.ker T.g.hom) ⧸ LinearMap.range T.moduleCatToCycles) :=
 579  Submodule.mapQ _ _ (kerMap ψ) (kerMap_range_le ψ)
 580
 581/-- The concrete left-homology map data for `ψ` relative to the
 582`moduleCat` left homology data on both sides. -/
 583noncomputable def lhMapData (ψ : S ⟶ T) :
 584    LeftHomologyMapData ψ S.moduleCatLeftHomologyData T.moduleCatLeftHomologyData where
 585  φK := ModuleCat.ofHom (kerMap ψ)
 586  φH := ModuleCat.ofHom (quotMap ψ)
 587  commi := by
 588    refine ModuleCat.hom_ext (LinearMap.ext fun x => ?_)
 589    rfl
 590  commf' := by
 591    refine ModuleCat.hom_ext (LinearMap.ext fun a => ?_)
 592    apply Subtype.ext
 593    show ψ.τ₂ (S.f a) = T.f (ψ.τ₁ a)
 594    have h := congrArg (fun f : S.X₁ ⟶ T.X₂ => f a) ψ.comm₁₂
 595    simpa only [ModuleCat.comp_apply] using h.symm
 596  commπ := by
 597    refine ModuleCat.hom_ext (LinearMap.ext fun x => ?_)
 598    show quotMap ψ (Submodule.Quotient.mk x) = Submodule.Quotient.mk (kerMap ψ x)
 599    rfl
 600
 601lemma quotMap_surjective (ψ : S ⟶ T)
 602    (hsurj : ∀ y : T.X₂, T.g y = 0 →
 603      ∃ (x : S.X₂) (w : T.X₁), S.g x = 0 ∧ ψ.τ₂ x = y + T.f w) :
 604    Function.Surjective (quotMap ψ) := by
 605  intro q
 606  obtain ⟨⟨y, hy⟩, rfl⟩ :=
 607    Submodule.mkQ_surjective (LinearMap.range T.moduleCatToCycles) q
 608  obtain ⟨x, w, hgx, hx⟩ := hsurj y (LinearMap.mem_ker.mp hy)
 609  refine ⟨Submodule.Quotient.mk ⟨x, LinearMap.mem_ker.mpr hgx⟩, ?_⟩
 610  show quotMap ψ (Submodule.Quotient.mk _) =
 611    Submodule.Quotient.mk (⟨y, hy⟩ : ↥(LinearMap.ker T.g.hom))
 612  rw [quotMap, Submodule.mapQ_apply]
 613  refine (Submodule.Quotient.eq _).mpr ⟨w, ?_⟩
 614  apply Subtype.ext
 615  show T.f w = ψ.τ₂ x - y
 616  rw [hx]
 617  abel
 618
 619lemma quotMap_injective (ψ : S ⟶ T)
 620    (hinj : ∀ x : S.X₂, S.g x = 0 → (∃ w : T.X₁, ψ.τ₂ x = T.f w) →
 621      ∃ v : S.X₁, x = S.f v) :
 622    Function.Injective (quotMap ψ) := by
 623  rw [injective_iff_map_eq_zero]
 624  intro q hq
 625  obtain ⟨⟨x, hx⟩, rfl⟩ :=
 626    Submodule.mkQ_surjective (LinearMap.range S.moduleCatToCycles) q
 627  have hq' : Submodule.Quotient.mk (p := LinearMap.range T.moduleCatToCycles)
 628      (kerMap ψ ⟨x, hx⟩) = 0 := by
 629    rw [← Submodule.mapQ_apply (LinearMap.range S.moduleCatToCycles)
 630      (h := kerMap_range_le ψ)]
 631    exact hq
 632  rw [Submodule.Quotient.mk_eq_zero] at hq'
 633  replace hq := hq'
 634  obtain ⟨w, hw⟩ := hq
 635  have hw' : ψ.τ₂ x = T.f w := by
 636    have := congrArg (Subtype.val) hw
 637    exact this.symm
 638  obtain ⟨v, hv⟩ := hinj x (LinearMap.mem_ker.mp hx) ⟨w, hw'⟩
 639  show Submodule.Quotient.mk (⟨x, hx⟩ : ↥(LinearMap.ker S.g.hom)) = 0
 640  rw [Submodule.Quotient.mk_eq_zero]
 641  exact ⟨v, Subtype.ext (by simpa using hv.symm)⟩
 642
 643/-- **The concrete criterion.** A morphism of short complexes of
 644`ℤ`-modules induces an isomorphism on homology as soon as the two
 645elementwise conditions hold. -/
 646lemma isIso_homologyMap_of_elementwise (ψ : S ⟶ T)
 647    (hsurj : ∀ y : T.X₂, T.g y = 0 →
 648      ∃ (x : S.X₂) (w : T.X₁), S.g x = 0 ∧ ψ.τ₂ x = y + T.f w)
 649    (hinj : ∀ x : S.X₂, S.g x = 0 → (∃ w : T.X₁, ψ.τ₂ x = T.f w) →
 650      ∃ v : S.X₁, x = S.f v) :
 651    IsIso (ShortComplex.homologyMap ψ) := by
 652  rw [(lhMapData ψ).homologyMap_eq]
 653  have hbij : Function.Bijective (quotMap ψ) :=
 654    ⟨quotMap_injective ψ hinj, quotMap_surjective ψ hsurj⟩
 655  have hiso : IsIso (lhMapData ψ).φH := by
 656    show IsIso (ModuleCat.ofHom (quotMap ψ))
 657    have hmono : Mono (ModuleCat.ofHom (quotMap ψ)) :=
 658      (ModuleCat.mono_iff_injective _).mpr hbij.1
 659    have hepi : Epi (ModuleCat.ofHom (quotMap ψ)) :=
 660      (ModuleCat.epi_iff_surjective _).mpr hbij.2
 661    exact isIso_of_mono_of_epi _
 662  infer_instance
 663
 664lemma epi_homologyMap_of_elementwise (ψ : S ⟶ T)
 665    (hsurj : ∀ y : T.X₂, T.g y = 0 →
 666      ∃ (x : S.X₂) (w : T.X₁), S.g x = 0 ∧ ψ.τ₂ x = y + T.f w) :
 667    Epi (ShortComplex.homologyMap ψ) := by
 668  rw [(lhMapData ψ).homologyMap_eq]
 669  have hepi : Epi (lhMapData ψ).φH := by
 670    show Epi (ModuleCat.ofHom (quotMap ψ))
 671    exact (ModuleCat.epi_iff_surjective _).mpr (quotMap_surjective ψ hsurj)
 672  apply epi_comp
 673end HomologyCriterion
 674
 675/-! ## Stage 2 toolkit D: chain-complex wrappers for the criterion -/
 676
 677section ChainCriterion
 678
 679variable {K L : ChainComplex (ModuleCat.{0} ℤ) ℕ}
 680
 681/-- Transport of `IsIso` on `homologyMap` through the honest-index short
 682complex functor `shortComplexFunctor'`. -/
 683lemma isIso_homologyMap_of_sc' (φ : K ⟶ L) (i j k : ℕ)
 684    (hi : (ComplexShape.down ℕ).prev j = i) (hk : (ComplexShape.down ℕ).next j = k)
 685    (h : IsIso (ShortComplex.homologyMap
 686      ((HomologicalComplex.shortComplexFunctor' (ModuleCat.{0} ℤ)
 687        (ComplexShape.down ℕ) i j k).map φ))) :
 688    IsIso (HomologicalComplex.homologyMap φ j) := by
 689  set e := HomologicalComplex.natIsoSc' (ModuleCat.{0} ℤ) (ComplexShape.down ℕ)
 690    i j k hi hk with he
 691  have hnat := e.hom.naturality φ
 692  have hcomm : (HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
 693      (ComplexShape.down ℕ) j).map φ =
 694      e.hom.app K ≫ (HomologicalComplex.shortComplexFunctor' (ModuleCat.{0} ℤ)
 695        (ComplexShape.down ℕ) i j k).map φ ≫ e.inv.app L := by
 696    rw [← Category.assoc, ← hnat, Category.assoc, Iso.hom_inv_id_app,
 697      Category.comp_id]
 698  have h1 : IsIso (ShortComplex.homologyMap (e.hom.app K)) :=
 699    (inferInstance : IsIso (ShortComplex.homologyMapIso (e.app K)).hom)
 700  have h2 : IsIso (ShortComplex.homologyMap (e.inv.app L)) :=
 701    (inferInstance : IsIso (ShortComplex.homologyMapIso (e.app L)).inv)
 702  show IsIso (ShortComplex.homologyMap
 703    ((HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
 704      (ComplexShape.down ℕ) j).map φ))
 705  rw [hcomm, ShortComplex.homologyMap_comp, ShortComplex.homologyMap_comp]
 706  infer_instance
 707
 708/-- Transport of `Epi` on `homologyMap` through the honest-index short
 709complex functor. -/
 710lemma epi_homologyMap_of_sc' (φ : K ⟶ L) (i j k : ℕ)
 711    (hi : (ComplexShape.down ℕ).prev j = i) (hk : (ComplexShape.down ℕ).next j = k)
 712    (h : Epi (ShortComplex.homologyMap
 713      ((HomologicalComplex.shortComplexFunctor' (ModuleCat.{0} ℤ)
 714        (ComplexShape.down ℕ) i j k).map φ))) :
 715    Epi (HomologicalComplex.homologyMap φ j) := by
 716  set e := HomologicalComplex.natIsoSc' (ModuleCat.{0} ℤ) (ComplexShape.down ℕ)
 717    i j k hi hk with he
 718  have hnat := e.hom.naturality φ
 719  have hcomm : (HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
 720      (ComplexShape.down ℕ) j).map φ =
 721      e.hom.app K ≫ (HomologicalComplex.shortComplexFunctor' (ModuleCat.{0} ℤ)
 722        (ComplexShape.down ℕ) i j k).map φ ≫ e.inv.app L := by
 723    rw [← Category.assoc, ← hnat, Category.assoc, Iso.hom_inv_id_app,
 724      Category.comp_id]
 725  have h1 : IsIso (ShortComplex.homologyMap (e.hom.app K)) :=
 726    (inferInstance : IsIso (ShortComplex.homologyMapIso (e.app K)).hom)
 727  have h2 : IsIso (ShortComplex.homologyMap (e.inv.app L)) :=
 728    (inferInstance : IsIso (ShortComplex.homologyMapIso (e.app L)).inv)
 729  show Epi (ShortComplex.homologyMap
 730    ((HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
 731      (ComplexShape.down ℕ) j).map φ))
 732  rw [hcomm, ShortComplex.homologyMap_comp, ShortComplex.homologyMap_comp]
 733  exact epi_comp _ _
 734
 735/-- Criterion for `homologyMap` in positive degree, with honest indices. -/
 736lemma isIso_homologyMap_chain_succ (φ : K ⟶ L) (n : ℕ)
 737    (hsurj : ∀ y : L.X (n + 1), L.d (n + 1) n y = 0 →
 738      ∃ (x : K.X (n + 1)) (w : L.X (n + 2)),
 739        K.d (n + 1) n x = 0 ∧ φ.f (n + 1) x = y + L.d (n + 2) (n + 1) w)
 740    (hinj : ∀ x : K.X (n + 1), K.d (n + 1) n x = 0 →
 741      (∃ w : L.X (n + 2), φ.f (n + 1) x = L.d (n + 2) (n + 1) w) →
 742      ∃ v : K.X (n + 2), x = K.d (n + 2) (n + 1) v) :
 743    IsIso (HomologicalComplex.homologyMap φ (n + 1)) := by
 744  refine isIso_homologyMap_of_sc' φ (n + 2) (n + 1) n
 745    (ChainComplex.prev ℕ (n + 1)) (ChainComplex.next_nat_succ n) ?_
 746  exact isIso_homologyMap_of_elementwise _ hsurj hinj
 747
 748/-- Criterion for `homologyMap` in degree `0`, with honest indices. -/
 749lemma isIso_homologyMap_chain_zero (φ : K ⟶ L)
 750    (hsurj : ∀ y : L.X 0,
 751      ∃ (x : K.X 0) (w : L.X 1), φ.f 0 x = y + L.d 1 0 w)
 752    (hinj : ∀ x : K.X 0, (∃ w : L.X 1, φ.f 0 x = L.d 1 0 w) →
 753      ∃ v : K.X 1, x = K.d 1 0 v) :
 754    IsIso (HomologicalComplex.homologyMap φ 0) := by
 755  have hdK : K.d 0 0 = 0 := K.shape 0 0 (by simp [ComplexShape.down_Rel])
 756  refine isIso_homologyMap_of_sc' φ 1 0 0
 757    (ChainComplex.prev ℕ 0) ChainComplex.next_nat_zero ?_
 758  refine isIso_homologyMap_of_elementwise _ ?_ ?_
 759  · intro y _
 760    obtain ⟨x, w, hx⟩ := hsurj y
 761    refine ⟨x, w, ?_, hx⟩
 762    show (K.d 0 0) x = 0
 763    rw [hdK]
 764    exact zeroApp x
 765  · intro x _ hx
 766    exact hinj x hx
 767
 768/-- Epi criterion for `homologyMap` in degree `0`. -/
 769lemma epi_homologyMap_chain_zero (φ : K ⟶ L)
 770    (hsurj : ∀ y : L.X 0,
 771      ∃ (x : K.X 0) (w : L.X 1), φ.f 0 x = y + L.d 1 0 w) :
 772    Epi (HomologicalComplex.homologyMap φ 0) := by
 773  have hdK : K.d 0 0 = 0 := K.shape 0 0 (by simp [ComplexShape.down_Rel])
 774  refine epi_homologyMap_of_sc' φ 1 0 0
 775    (ChainComplex.prev ℕ 0) ChainComplex.next_nat_zero ?_
 776  refine epi_homologyMap_of_elementwise _ ?_
 777  intro y _
 778  obtain ⟨x, w, hx⟩ := hsurj y
 779  refine ⟨x, w, ?_, hx⟩
 780  show (K.d 0 0) x = 0
 781  rw [hdK]
 782  exact zeroApp x
 783
 784end ChainCriterion
 785
 786/-! ## Stage 2: the small-chains theorem (Hatcher, Prop 2.21) -/
 787
 788section SmallChainsTheorem
 789
 790variable {U V : Set X}
 791
 792/-- Surjectivity input in positive degrees. -/
 793lemma small_surj_succ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
 794    (n : ℕ) (y : Cgrp X (n + 1)) (hy : bnd X n y = 0) :
 795    ∃ (x : ↥(sCgrp U V (n + 1))) (w : Cgrp X (n + 2)),
 796      sBnd U V n x = 0 ∧ sInc U V (n + 1) x = y + bnd X (n + 1) w := by
 797  obtain ⟨k, hk⟩ := exists_sdOpIter_mem_smallSpan hU hV hUV y
 798  obtain ⟨x, hx⟩ := exists_sInc_eq hk
 799  refine ⟨x, -(tOpIter X (n + 1) k y), ?_, ?_⟩
 800  · -- x is a cycle in the small complex
 801    apply sInc_injective U V n
 802    have h1 : sInc U V n (sBnd U V n x) = bnd X n (sInc U V (n + 1) x) := by
 803      rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply, sBnd_comp_sInc]
 804    rw [h1, hx, sdOpIter_bnd_elem, hy, map_zero, map_zero]
 805  · rw [hx, map_neg]
 806    have h2 := sub_sdOpIter_eq_bnd_succ (k := k) y hy
 807    have : sdOpIter X (n + 1) k y = y - bnd X (n + 1) (tOpIter X (n + 1) k y) := by
 808      rw [← h2]; abel
 809    rw [this]; abel
 810
 811/-- Injectivity input in every degree `n` (with boundary from degree
 812`n + 1`). -/
 813lemma small_inj (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
 814    (n : ℕ) (x : ↥(sCgrp U V n)) (w : Cgrp X (n + 1))
 815    (hw : sInc U V n x = bnd X n w) :
 816    ∃ v : ↥(sCgrp U V (n + 1)), x = sBnd U V n v := by
 817  set z := sInc U V n x with hz
 818  have hzsmall : z ∈ smallSpan U V n := sInc_mem_smallSpan U V n x
 819  obtain ⟨k, hks⟩ := exists_sdOpIter_mem_smallSpan hU hV hUV w
 820  -- the corrected chain c := T_k z + sd^k w is small and has boundary z
 821  have hsd : sdOpIter X n k z = bnd X n (sdOpIter X (n + 1) k w) := by
 822    rw [sdOpIter_bnd_elem, hw]
 823  have hcorr : z - sdOpIter X n k z = bnd X n (tOpIter X n k z) :=
 824    sub_sdOpIter_eq_bnd_of_boundary k z w hw
 825  have hzbnd : z = bnd X n (tOpIter X n k z + sdOpIter X (n + 1) k w) := by
 826    rw [map_add, ← hcorr, ← hsd]
 827    abel
 828  have hcsmall : tOpIter X n k z + sdOpIter X (n + 1) k w ∈ smallSpan U V (n + 1) :=
 829    Submodule.add_mem _ (tOpIter_mem_smallSpan k hzsmall) hks
 830  obtain ⟨v, hv⟩ := exists_sInc_eq hcsmall
 831  refine ⟨v, ?_⟩
 832  apply sInc_injective U V n
 833  have h1 : sInc U V n (sBnd U V n v) = bnd X n (sInc U V (n + 1) v) := by
 834    rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply, sBnd_comp_sInc]
 835  rw [h1, hv, ← hzbnd, hz]
 836
 837/-- **Stage 2: the small-chains theorem.** For open `U, V` covering `X`,
 838the inclusion of the small-chains subcomplex induces an isomorphism on
 839homology in every degree. -/
 840theorem smallι_isIso_homologyMap (hU : IsOpen U) (hV : IsOpen V)
 841    (hUV : U ∪ V = Set.univ) (n : ℕ) :
 842    IsIso (HomologicalComplex.homologyMap (smallι U V) n) := by
 843  match n with
 844  | 0 =>
 845      refine isIso_homologyMap_chain_zero (smallι U V) ?_ ?_
 846      · intro y
 847        obtain ⟨k, hk⟩ := exists_sdOpIter_mem_smallSpan hU hV hUV y
 848        obtain ⟨x, hx⟩ := exists_sInc_eq hk
 849        refine ⟨x, -(tOpIter X 0 k y), ?_⟩
 850        let y' : ↥(Cgrp X 0) := y
 851        have hx' : sInc U V 0 x = sdOpIter X 0 k y' := hx
 852        have h2 := sub_sdOpIter_eq_bnd_zero (k := k) y'
 853        have h3 : sInc U V 0 x = y' + bnd X 0 (-(tOpIter X 0 k y')) := by
 854          rw [hx', map_neg]
 855          have h4 : sdOpIter X 0 k y' = y' - bnd X 0 (tOpIter X 0 k y') := by
 856            rw [← h2]; abel
 857          rw [h4]; abel
 858        exact h3
 859      · intro x hx
 860        obtain ⟨w, hw⟩ := hx
 861        have hw' : sInc U V 0 x = bnd X 0 w := hw
 862        obtain ⟨v, hv⟩ := small_inj hU hV hUV 0 x w hw'
 863        refine ⟨v, ?_⟩
 864        show x = (SSC U V).d 1 0 v
 865        rw [SSC_d]
 866        exact hv
 867  | n + 1 =>
 868      refine isIso_homologyMap_chain_succ (smallι U V) n ?_ ?_
 869      · intro y hy
 870        obtain ⟨x, w, h1, h2⟩ := small_surj_succ hU hV hUV n y hy
 871        refine ⟨x, w, ?_, h2⟩
 872        show (SSC U V).d (n + 1) n x = 0
 873        rw [SSC_d]
 874        exact h1
 875      · intro x hx hw
 876        obtain ⟨w, hw'⟩ := hw
 877        obtain ⟨v, hv⟩ := small_inj hU hV hUV (n + 1) x w hw'
 878        refine ⟨v, ?_⟩
 879        show x = (SSC U V).d (n + 2) (n + 1) v
 880        rw [SSC_d]
 881        exact hv
 882
 883/-- The small-chains homology isomorphism `H_n(C^{U,V}) ≅ H_n(X)`. -/
 884noncomputable def smallChainsHomologyIso (hU : IsOpen U) (hV : IsOpen V)
 885    (hUV : U ∪ V = Set.univ) (n : ℕ) :
 886    (SSC U V).homology n ≅ (SC X).homology n :=
 887  have := smallι_isIso_homologyMap hU hV hUV n
 888  asIso (HomologicalComplex.homologyMap (smallι U V) n)
 889
 890end SmallChainsTheorem
 891
 892/-! ## Stage 3 toolkit A: coordinates on free coproducts of copies of `ℤ` -/
 893
 894section Coordinates
 895
 896variable {κ κ' : Type}
 897
 898/-- The coordinate of an element of `∐_κ ℤ` at an index, through the
 899direct-sum presentation. -/
 900noncomputable def coordAt (i : κ) (z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) : ℤ :=
 901  (ModuleCat.coprodIsoDirectSum (fun _ : κ => ModuleCat.of ℤ ℤ)).hom z i
 902
 903lemma coordAt_unitOf (i j : κ) :
 904    coordAt j (unitOf i) = if i = j then 1 else 0 := by
 905  unfold coordAt unitOf
 906  rw [← ModuleCat.comp_apply, ModuleCat.ι_coprodIsoDirectSum_hom]
 907  show (DirectSum.lof ℤ κ (fun _ => ℤ) i (1 : ℤ)) j = _
 908  by_cases h : i = j
 909  · subst h
 910    rw [if_pos rfl, DirectSum.lof_eq_of, DirectSum.of_eq_same]
 911  · rw [if_neg h, DirectSum.lof_eq_of, DirectSum.of_eq_of_ne _ _ _ (Ne.symm h)]
 912
 913lemma coordAt_zero (i : κ) :
 914    coordAt i (0 : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) = 0 := by
 915  unfold coordAt
 916  rw [map_zero]
 917  exact DFinsupp.zero_apply i
 918
 919lemma coordAt_add (j : κ) (x y : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) :
 920    coordAt j (x + y) = coordAt j x + coordAt j y := by
 921  unfold coordAt
 922  rw [map_add]
 923  exact DFinsupp.add_apply _ _ _
 924
 925lemma coordAt_smul (j : κ) (c : ℤ) (x : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) :
 926    coordAt j (c • x) = c • coordAt j x := by
 927  unfold coordAt
 928  rw [mapSmul]
 929  exact DFinsupp.smul_apply _ _ _
 930
 931/-- The support of an element of `∐_κ ℤ`. -/
 932noncomputable def suppOf (z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) : Finset κ :=
 933  ((ModuleCat.coprodIsoDirectSum (fun _ : κ => ModuleCat.of ℤ ℤ)).hom z).support
 934
 935lemma mem_suppOf_iff {i : κ} {z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)} :
 936    i ∈ suppOf z ↔ coordAt i z ≠ 0 := by
 937  unfold suppOf coordAt
 938  exact DFinsupp.mem_support_iff
 939
 940/-- Every element of `∐_κ ℤ` is the (finite) sum of its coordinates times
 941the generating elements. -/
 942lemma sum_coordAt_smul_unitOf (z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) :
 943    z = ∑ i ∈ suppOf z, coordAt i z • unitOf i := by
 944  unfold suppOf coordAt
 945  set e := ModuleCat.coprodIsoDirectSum (fun _ : κ => ModuleCat.of ℤ ℤ) with he
 946  have h1 : e.inv (e.hom z) = z := by
 947    rw [← ModuleCat.comp_apply, e.hom_inv_id, ModuleCat.id_apply]
 948  have h2 : e.hom z =
 949      ∑ i ∈ (e.hom z).support, DirectSum.lof ℤ κ (fun _ => ℤ) i ((e.hom z) i) := by
 950    conv_lhs => rw [← DirectSum.sum_support_of (e.hom z)]
 951    refine Finset.sum_congr rfl fun i _ => ?_
 952    rw [DirectSum.lof_eq_of]
 953  have h3 : z = ∑ i ∈ (e.hom z).support, ((e.hom z) i) • unitOf i := by
 954    conv_lhs => rw [← h1]
 955    conv_lhs => rw [h2]
 956    rw [map_sum]
 957    refine Finset.sum_congr rfl fun i _ => ?_
 958    have h4 : DirectSum.lof ℤ κ (fun _ => ℤ) i ((e.hom z) i) =
 959        ((e.hom z) i) • DirectSum.lof ℤ κ (fun _ => ℤ) i (1 : ℤ) := by
 960      rw [← map_smul, smul_eq_mul, mul_one]
 961    rw [h4, mapSmul]
 962    congr 1
 963    rw [he]
 964    exact ModuleCat.lof_coprodIsoDirectSum_inv_apply
 965      (fun _ : κ => ModuleCat.of ℤ ℤ) i (1 : ℤ)
 966  exact h3
 967
 968/-- Coordinate tracking through a basis-index map: at an index in the image
 969of an injective index map, the coordinate of the image chain is the source
 970coordinate. -/
 971lemma coordAt_map_eq {ψ : κ → κ'} (hψ : Function.Injective ψ)
 972    {F : (∐ fun _ : κ => ModuleCat.of ℤ ℤ) ⟶ (∐ fun _ : κ' => ModuleCat.of ℤ ℤ)}
 973    (hF : ∀ i, F (unitOf i) = unitOf (ψ i)) (i : κ)
 974    (z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) :
 975    coordAt (ψ i) (F z) = coordAt i z := by
 976  induction z using freeInduction with
 977  | unit i' =>
 978      rw [hF, coordAt_unitOf, coordAt_unitOf]
 979      exact if_congr hψ.eq_iff rfl rfl
 980  | zero => rw [map_zero, coordAt_zero, coordAt_zero]
 981  | add x y hx hy => rw [map_add, coordAt_add, coordAt_add, hx, hy]
 982  | smulz c x hx => rw [mapSmul, coordAt_smul, coordAt_smul, hx]
 983
 984/-- Coordinate tracking through a basis-index map: at an index outside the
 985image of the index map, the coordinate of any image chain vanishes. -/
 986lemma coordAt_map_notMem {ψ : κ → κ'}
 987    {F : (∐ fun _ : κ => ModuleCat.of ℤ ℤ) ⟶ (∐ fun _ : κ' => ModuleCat.of ℤ ℤ)}
 988    (hF : ∀ i, F (unitOf i) = unitOf (ψ i)) {t : κ'} (ht : ∀ i, ψ i ≠ t)
 989    (z : ↥(∐ fun _ : κ => ModuleCat.of ℤ ℤ)) :
 990    coordAt t (F z) = 0 := by
 991  induction z using freeInduction with
 992  | unit i' =>
 993      rw [hF, coordAt_unitOf]
 994      exact if_neg (ht i')
 995  | zero => rw [map_zero, coordAt_zero]
 996  | add x y hx hy => rw [map_add, coordAt_add, hx, hy, add_zero]
 997  | smulz c x hx => rw [mapSmul, coordAt_smul, hx, smul_zero]
 998
 999end Coordinates
1000
1001/-! ## Stage 3 toolkit B: elements of binary biproducts of `ℤ`-modules -/
1002
1003section BiprodElements
1004
1005variable {A B : ModuleCat.{0} ℤ}
1006
1007lemma addApp {M N : ModuleCat.{0} ℤ} (f g : M ⟶ N) (x : M) :
1008    (f + g) x = f x + g x := by
1009  show (f + g).hom x = f.hom x + g.hom x
1010  rw [ModuleCat.hom_add]
1011  rfl
1012
1013lemma negApp {M N : ModuleCat.{0} ℤ} (f : M ⟶ N) (x : M) :
1014    (-f) x = -(f x) := by
1015  show (-f).hom x = -(f.hom x)
1016  rw [ModuleCat.hom_neg]
1017  rfl
1018
1019/-- Elementwise decomposition of an element of a binary biproduct into its
1020two components. -/
1021lemma biprod_decomp (z : ↥(A ⊞ B)) :
1022    z = (biprod.inl : A ⟶ A ⊞ B) ((biprod.fst : A ⊞ B ⟶ A) z) +
1023        (biprod.inr : B ⟶ A ⊞ B) ((biprod.snd : A ⊞ B ⟶ B) z) := by
1024  have h := congrArg
1025    (fun f : A ⊞ B ⟶ A ⊞ B => f z) (biprod.total (X := A) (Y := B))
1026  have h1 : (biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr :
1027      A ⊞ B ⟶ A ⊞ B) z =
1028      (biprod.inl : A ⟶ A ⊞ B) ((biprod.fst : A ⊞ B ⟶ A) z) +
1029        (biprod.inr : B ⟶ A ⊞ B) ((biprod.snd : A ⊞ B ⟶ B) z) := by
1030    rw [addApp, ModuleCat.comp_apply, ModuleCat.comp_apply]
1031  have h2 : (𝟙 (A ⊞ B) : A ⊞ B ⟶ A ⊞ B) z = z := ModuleCat.id_apply _ _
1032  simp only [h1, h2] at h
1033  exact h.symm
1034
1035/-- Elementwise extensionality in a binary biproduct. -/
1036lemma biprod_elem_ext {z w : ↥(A ⊞ B)}
1037    (h1 : (biprod.fst : A ⊞ B ⟶ A) z = (biprod.fst : A ⊞ B ⟶ A) w)
1038    (h2 : (biprod.snd : A ⊞ B ⟶ B) z = (biprod.snd : A ⊞ B ⟶ B) w) :
1039    z = w := by
1040  rw [biprod_decomp z, biprod_decomp w, h1, h2]
1041
1042/-- Elementwise formula for `biprod.desc`. -/
1043lemma descApp {M : ModuleCat.{0} ℤ} (u : A ⟶ M) (v : B ⟶ M) (z : ↥(A ⊞ B)) :
1044    biprod.desc u v z =
1045      u ((biprod.fst : A ⊞ B ⟶ A) z) + v ((biprod.snd : A ⊞ B ⟶ B) z) := by
1046  have h1 : biprod.desc u v
1047      ((biprod.inl : A ⟶ A ⊞ B) ((biprod.fst : A ⊞ B ⟶ A) z)) =
1048      u ((biprod.fst : A ⊞ B ⟶ A) z) := by
1049    rw [← ModuleCat.comp_apply, biprod.inl_desc]
1050  have h2 : biprod.desc u v
1051      ((biprod.inr : B ⟶ A ⊞ B) ((biprod.snd : A ⊞ B ⟶ B) z)) =
1052      v ((biprod.snd : A ⊞ B ⟶ B) z) := by
1053    rw [← ModuleCat.comp_apply, biprod.inr_desc]
1054  conv_lhs => rw [biprod_decomp z]
1055  rw [map_add, h1, h2]
1056
1057/-- Elementwise first component of `biprod.lift`. -/
1058lemma fst_liftApp {M : ModuleCat.{0} ℤ} (f : M ⟶ A) (g : M ⟶ B) (x : M) :
1059    (biprod.fst : A ⊞ B ⟶ A) (biprod.lift f g x) = f x := by
1060  rw [← ModuleCat.comp_apply, biprod.lift_fst]
1061
1062/-- Elementwise second component of `biprod.lift`. -/
1063lemma snd_liftApp {M : ModuleCat.{0} ℤ} (f : M ⟶ A) (g : M ⟶ B) (x : M) :
1064    (biprod.snd : A ⊞ B ⟶ B) (biprod.lift f g x) = g x := by
1065  rw [← ModuleCat.comp_apply, biprod.lift_snd]
1066
1067end BiprodElements
1068
1069/-! ## Stage 3 toolkit C: subspaces and simplex lifting -/
1070
1071section Subspaces
1072
1073/-- The `X`-simplex underlying a singular simplex of the subspace `W`. -/
1074noncomputable def pushIdx (W : Set X) {n : ℕ} (a : Idx (TopCat.of W) n) :
1075    Idx X n :=
1076  (TopCat.toSSet.map (SingularPair.subInc X W)).app (op ⦋n⦌) a
1077
1078lemma pushIdx_injective (W : Set X) (n : ℕ) :
1079    Function.Injective (pushIdx (X := X) W (n := n)) :=
1080  SingularPair.toSSet_map_app_injective (SingularPair.subInc X W)
1081    (SingularPair.subInc_injective X W) n
1082
1083lemma range_pushIdx (W : Set X) {n : ℕ} (a : Idx (TopCat.of W) n) :
1084    Set.range ⇑(simplexEquiv X n (pushIdx W a)) ⊆ W := by
1085  unfold pushIdx
1086  rw [simplexEquiv_map, ContinuousMap.coe_comp]
1087  rintro x ⟨t, rfl⟩
1088  exact ((simplexEquiv (TopCat.of W) n a) t).2
1089
1090/-- Lift a singular simplex of `X` whose range lies in `W` to a singular
1091simplex of the subspace `W`. -/
1092noncomputable def liftIdx (W : Set X) {n : ℕ} (s : Idx X n)
1093    (h : Set.range ⇑(simplexEquiv X n s) ⊆ W) : Idx (TopCat.of W) n :=
1094  (simplexEquiv (TopCat.of W) n).symm
1095    ⟨fun t => ⟨simplexEquiv X n s t, h ⟨t, rfl⟩⟩,
1096      (map_continuous (simplexEquiv X n s)).subtype_mk _⟩
1097
1098lemma pushIdx_liftIdx (W : Set X) {n : ℕ} (s : Idx X n)
1099    (h : Set.range ⇑(simplexEquiv X n s) ⊆ W) :
1100    pushIdx W (liftIdx W s h) = s := by
1101  apply (simplexEquiv X n).injective
1102  unfold pushIdx liftIdx
1103  rw [simplexEquiv_map, Equiv.apply_symm_apply]
1104  ext t
1105  rfl
1106
1107/-- The inclusion between nested subspaces of `X`, as a `TopCat`
1108morphism. -/
1109noncomputable def subIncl {W W' : Set X} (h : W ⊆ W') :
1110    TopCat.of W ⟶ TopCat.of W' :=
1111  TopCat.ofHom ⟨Set.inclusion h, continuous_inclusion h⟩
1112
1113lemma subIncl_comp_subInc {W W' : Set X} (h : W ⊆ W') :
1114    subIncl h ≫ SingularPair.subInc X W' = SingularPair.subInc X W := by
1115  ext x
1116  rfl
1117
1118lemma pushIdx_subIncl {W W' : Set X} (h : W ⊆ W') {n : ℕ}
1119    (a : Idx (TopCat.of W) n) :
1120    pushIdx W' ((TopCat.toSSet.map (subIncl h)).app (op ⦋n⦌) a) = pushIdx W a := by
1121  have h1 : (TopCat.toSSet.map (subIncl h ≫ SingularPair.subInc X W')).app
1122      (op ⦋n⦌) a =
1123      (TopCat.toSSet.map (SingularPair.subInc X W')).app (op ⦋n⦌)
1124        ((TopCat.toSSet.map (subIncl h)).app (op ⦋n⦌) a) := by
1125    rw [Functor.map_comp]
1126    rfl
1127  rw [pushIdx, ← h1, subIncl_comp_subInc, pushIdx]
1128
1129/-- Elementwise action of a chain map on generating elements. -/
1130lemma chainMap_unitOf {A B : TopCat.{0}} (f : A ⟶ B) {n : ℕ} (s : Idx A n) :
1131    chainMap f n (unitOf s) =
1132      unitOf ((TopCat.toSSet.map f).app (op ⦋n⦌) s) := by
1133  rw [comp_unitOf]
1134  have h : Sigma.ι (fun _ : Idx A n => ModuleCat.of ℤ ℤ) s ≫ chainMap f n =
1135      gen B n ((TopCat.toSSet.map f).app (op ⦋n⦌) s) := gen_map f n s
1136  rw [h, ev1_apply]
1137  rfl
1138
1139/-- Elementwise injectivity of the chain map of an injective continuous
1140map. -/
1141lemma chainMap_injective {A : TopCat.{0}} (f : A ⟶ X)
1142    (hf : Function.Injective f.hom) (n : ℕ) :
1143    Function.Injective (chainMap f n) := by
1144  intro a b hab
1145  have h := congrArg (SingularPair.genRetract f n) hab
1146  rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply,
1147    SingularPair.chainMap_comp_genRetract f hf n,
1148    ModuleCat.id_apply, ModuleCat.id_apply] at h
1149  exact h
1150
1151end Subspaces
1152
1153/-! ## Stage 3 toolkit D: the factor maps into the small subcomplex -/
1154
1155section MVMaps
1156
1157lemma small_pushIdx_left {n : ℕ} (a : Idx (TopCat.of U) n) :
1158    Small U V (pushIdx U a) := Or.inl (range_pushIdx U a)
1159
1160lemma small_pushIdx_right {n : ℕ} (a : Idx (TopCat.of V) n) :
1161    Small U V (pushIdx V a) := Or.inr (range_pushIdx V a)
1162
1163/-- The index map from `U`-simplices to small simplices. -/
1164noncomputable def uIdx {n : ℕ} (a : Idx (TopCat.of U) n) : SIdx U V n :=
1165  ⟨pushIdx U a, small_pushIdx_left U V a⟩
1166
1167/-- The index map from `V`-simplices to small simplices. -/
1168noncomputable def vIdx {n : ℕ} (a : Idx (TopCat.of V) n) : SIdx U V n :=
1169  ⟨pushIdx V a, small_pushIdx_right U V a⟩
1170
1171lemma uIdx_injective (n : ℕ) : Function.Injective (uIdx U V (n := n)) :=
1172  fun _ _ hab => pushIdx_injective U n (congrArg Subtype.val hab)
1173
1174lemma vIdx_injective (n : ℕ) : Function.Injective (vIdx U V (n := n)) :=
1175  fun _ _ hab => pushIdx_injective V n (congrArg Subtype.val hab)
1176
1177/-- The degree-`n` chain map `C_n(U) ⟶ C_n^{U,V}`. -/
1178noncomputable def uInc (n : ℕ) : Cgrp (TopCat.of U) n ⟶ sCgrp U V n :=
1179  Sigma.desc fun a => sgen U V n (uIdx U V a)
1180
1181/-- The degree-`n` chain map `C_n(V) ⟶ C_n^{U,V}`. -/
1182noncomputable def vInc (n : ℕ) : Cgrp (TopCat.of V) n ⟶ sCgrp U V n :=
1183  Sigma.desc fun a => sgen U V n (vIdx U V a)
1184
1185lemma gen_uInc {n : ℕ} (a : Idx (TopCat.of U) n) :
1186    gen (TopCat.of U) n a ≫ uInc U V n = sgen U V n (uIdx U V a) :=
1187  Sigma.ι_desc _ _
1188
1189lemma gen_vInc {n : ℕ} (a : Idx (TopCat.of V) n) :
1190    gen (TopCat.of V) n a ≫ vInc U V n = sgen U V n (vIdx U V a) :=
1191  Sigma.ι_desc _ _
1192
1193lemma uInc_unitOf {n : ℕ} (a : Idx (TopCat.of U) n) :
1194    uInc U V n (unitOf a) = unitOf (uIdx U V a) := by
1195  rw [comp_unitOf]
1196  have h : Sigma.ι (fun _ : Idx (TopCat.of U) n => ModuleCat.of ℤ ℤ) a ≫
1197      uInc U V n = sgen U V n (uIdx U V a) := gen_uInc U V a
1198  rw [h, ev1_apply]
1199  rfl
1200
1201lemma vInc_unitOf {n : ℕ} (a : Idx (TopCat.of V) n) :
1202    vInc U V n (unitOf a) = unitOf (vIdx U V a) := by
1203  rw [comp_unitOf]
1204  have h : Sigma.ι (fun _ : Idx (TopCat.of V) n => ModuleCat.of ℤ ℤ) a ≫
1205      vInc U V n = sgen U V n (vIdx U V a) := gen_vInc U V a
1206  rw [h, ev1_apply]
1207  rfl
1208
1209lemma uInc_comp_sInc (n : ℕ) :
1210    uInc U V n ≫ sInc U V n = chainMap (SingularPair.subInc X U) n := by
1211  apply Sigma.hom_ext
1212  intro a
1213  rw [← assoc]
1214  rw [show Sigma.ι (fun _ : Idx (TopCat.of U) n => ModuleCat.of ℤ ℤ) a ≫
1215    uInc U V n = sgen U V n (uIdx U V a) from gen_uInc U V a]
1216  rw [sgen_sInc, gen_map]
1217  rfl
1218
1219lemma vInc_comp_sInc (n : ℕ) :
1220    vInc U V n ≫ sInc U V n = chainMap (SingularPair.subInc X V) n := by
1221  apply Sigma.hom_ext
1222  intro a
1223  rw [← assoc]
1224  rw [show Sigma.ι (fun _ : Idx (TopCat.of V) n => ModuleCat.of ℤ ℤ) a ≫
1225    vInc U V n = sgen U V n (vIdx U V a) from gen_vInc U V a]
1226  rw [sgen_sInc, gen_map]
1227  rfl
1228
1229
1230lemma uInc_injective (n : ℕ) : Function.Injective (uInc U V n) := by
1231  intro a b hab
1232  have h := congrArg (sInc U V n) hab
1233  rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply, uInc_comp_sInc] at h
1234  exact chainMap_injective (SingularPair.subInc X U)
1235    (SingularPair.subInc_injective X U) n h
1236
1237lemma vInc_injective (n : ℕ) : Function.Injective (vInc U V n) := by
1238  intro a b hab
1239  have h := congrArg (sInc U V n) hab
1240  rw [← ModuleCat.comp_apply, ← ModuleCat.comp_apply, vInc_comp_sInc] at h
1241  exact chainMap_injective (SingularPair.subInc X V)
1242    (SingularPair.subInc_injective X V) n h
1243
1244lemma uInc_comm (n : ℕ) :
1245    uInc U V (n + 1) ≫ sBnd U V n = bnd (TopCat.of U) n ≫ uInc U V n := by
1246  have := sInc_mono U V n
1247  rw [← cancel_mono (sInc U V n), assoc, assoc, sBnd_comp_sInc, uInc_comp_sInc,
1248    ← assoc, uInc_comp_sInc]
1249  exact HomologicalComplex.Hom.comm (sChainMap (SingularPair.subInc X U)) (n + 1) n
1250
1251lemma vInc_comm (n : ℕ) :
1252    vInc U V (n + 1) ≫ sBnd U V n = bnd (TopCat.of V) n ≫ vInc U V n := by
1253  have := sInc_mono U V n
1254  rw [← cancel_mono (sInc U V n), assoc, assoc, sBnd_comp_sInc, vInc_comp_sInc,
1255    ← assoc, vInc_comp_sInc]
1256  exact HomologicalComplex.Hom.comm (sChainMap (SingularPair.subInc X V)) (n + 1) n
1257
1258/-- The chain map `C_*(U) ⟶ C^{U,V}_*(X)`: a simplex of `U` is small. -/
1259noncomputable def smallU : SC (TopCat.of U) ⟶ SSC U V where
1260  f n := uInc U V n
1261  comm' := by
1262    rintro i j (rfl : j + 1 = i)
1263    rw [SSC_d]
1264    exact uInc_comm U V j
1265
1266/-- The chain map `C_*(V) ⟶ C^{U,V}_*(X)`: a simplex of `V` is small. -/
1267noncomputable def smallV : SC (TopCat.of V) ⟶ SSC U V where
1268  f n := vInc U V n
1269  comm' := by
1270    rintro i j (rfl : j + 1 = i)
1271    rw [SSC_d]
1272    exact vInc_comm U V j
1273
1274@[simp] lemma smallU_f (n : ℕ) : (smallU U V).f n = uInc U V n := rfl
1275@[simp] lemma smallV_f (n : ℕ) : (smallV U V).f n = vInc U V n := rfl
1276
1277lemma smallU_comp_smallι :
1278    smallU U V ≫ smallι U V = sChainMap (SingularPair.subInc X U) := by
1279  apply HomologicalComplex.hom_ext
1280  intro n
1281  exact uInc_comp_sInc U V n
1282
1283lemma smallV_comp_smallι :
1284    smallV U V ≫ smallι U V = sChainMap (SingularPair.subInc X V) := by
1285  apply HomologicalComplex.hom_ext
1286  intro n
1287  exact vInc_comp_sInc U V n
1288
1289/-- The space-level inclusion `U ∩ V ↪ U`. -/
1290noncomputable def mvInclU : TopCat.of (U ∩ V : Set X) ⟶ TopCat.of U :=
1291  subIncl Set.inter_subset_left
1292
1293/-- The space-level inclusion `U ∩ V ↪ V`. -/
1294noncomputable def mvInclV : TopCat.of (U ∩ V : Set X) ⟶ TopCat.of V :=
1295  subIncl Set.inter_subset_right
1296
1297lemma pushIdx_mvInclU {n : ℕ} (a : Idx (TopCat.of (U ∩ V : Set X)) n) :
1298    pushIdx U ((TopCat.toSSet.map (mvInclU U V)).app (op ⦋n⦌) a) =
1299      pushIdx (U ∩ V : Set X) a :=
1300  pushIdx_subIncl Set.inter_subset_left a
1301
1302lemma pushIdx_mvInclV {n : ℕ} (a : Idx (TopCat.of (U ∩ V : Set X)) n) :
1303    pushIdx V ((TopCat.toSSet.map (mvInclV U V)).app (op ⦋n⦌) a) =
1304      pushIdx (U ∩ V : Set X) a :=
1305  pushIdx_subIncl Set.inter_subset_right a
1306
1307/-- Both routes `C_n(U ∩ V) ⟶ C_n^{U,V}` agree: through `U` and through
1308`V` a simplex of the intersection lands on the same small generator. -/
1309lemma inclU_uInc_eq_inclV_vInc (n : ℕ) :
1310    chainMap (mvInclU U V) n ≫ uInc U V n =
1311      chainMap (mvInclV U V) n ≫ vInc U V n := by
1312  apply Sigma.hom_ext
1313  intro a
1314  rw [← assoc]
1315  rw [show Sigma.ι (fun _ : Idx (TopCat.of (U ∩ V : Set X)) n =>
1316      ModuleCat.of ℤ ℤ) a ≫ chainMap (mvInclU U V) n =
1317      gen (TopCat.of U) n ((TopCat.toSSet.map (mvInclU U V)).app (op ⦋n⦌) a)
1318    from gen_map (mvInclU U V) n a]
1319  rw [gen_uInc, ← assoc]
1320  rw [show Sigma.ι (fun _ : Idx (TopCat.of (U ∩ V : Set X)) n =>
1321      ModuleCat.of ℤ ℤ) a ≫ chainMap (mvInclV U V) n =
1322      gen (TopCat.of V) n ((TopCat.toSSet.map (mvInclV U V)).app (op ⦋n⦌) a)
1323    from gen_map (mvInclV U V) n a]
1324  rw [gen_vInc]
1325  congr 1
1326
1327lemma sChainMap_inclU_smallU_eq :
1328    sChainMap (mvInclU U V) ≫ smallU U V =
1329      sChainMap (mvInclV U V) ≫ smallV U V := by
1330  apply HomologicalComplex.hom_ext
1331  intro n
1332  exact inclU_uInc_eq_inclV_vInc U V n
1333
1334end MVMaps
1335
1336/-! ## Stage 3: the Mayer-Vietoris short exact sequence -/
1337
1338section MVSES
1339
1340/-- The left map `x ↦ (i_* x, −j_* x)` of the Mayer-Vietoris sequence. -/
1341noncomputable def mvα :
1342    SC (TopCat.of (U ∩ V : Set X)) ⟶ SC (TopCat.of U) ⊞ SC (TopCat.of V) :=
1343  biprod.lift (sChainMap (mvInclU U V)) (-(sChainMap (mvInclV U V)))
1344
1345/-- The right map `(a, b) ↦ k_* a + l_* b` into the small subcomplex. -/
1346noncomputable def mvβ :
1347    SC (TopCat.of U) ⊞ SC (TopCat.of V) ⟶ SSC U V :=
1348  biprod.desc (smallU U V) (smallV U V)
1349
1350lemma mvα_comp_mvβ : mvα U V ≫ mvβ U V = 0 := by
1351  rw [mvα, mvβ, biprod.lift_desc, sChainMap_inclU_smallU_eq,
1352    Preadditive.neg_comp]
1353  exact add_neg_cancel _
1354
1355/-- **Stage 3.** The Mayer-Vietoris short complex of chain complexes
1356`0 ⟶ C_*(U ∩ V) ⟶ C_*(U) ⊞ C_*(V) ⟶ C^{U,V}_*(X) ⟶ 0`. -/
1357noncomputable def mvSES : ShortComplex (ChainComplex (ModuleCat.{0} ℤ) ℕ) :=
1358  ShortComplex.mk (mvα U V) (mvβ U V) (mvα_comp_mvβ U V)
1359
1360lemma mvαβ_degreewise_zero (n : ℕ) :
1361    biprod.lift (chainMap (mvInclU U V) n) (-(chainMap (mvInclV U V) n)) ≫
1362      biprod.desc (uInc U V n) (vInc U V n) = 0 := by
1363  rw [biprod.lift_desc, inclU_uInc_eq_inclV_vInc, Preadditive.neg_comp]
1364  exact add_neg_cancel _
1365
1366/-- The degree-`n` concrete Mayer-Vietoris short complex of `ℤ`-modules. -/
1367noncomputable def mvSESdeg (n : ℕ) : ShortComplex (ModuleCat.{0} ℤ) :=
1368  ShortComplex.mk
1369    (biprod.lift (chainMap (mvInclU U V) n) (-(chainMap (mvInclV U V) n)))
1370    (biprod.desc (uInc U V n) (vInc U V n))
1371    (mvαβ_degreewise_zero U V n)
1372
1373lemma mvSESdeg_mono (n : ℕ) : Mono (mvSESdeg U V n).f := by
1374  show Mono (biprod.lift (chainMap (mvInclU U V) n) (-(chainMap (mvInclV U V) n)))
1375  haveI h1 : Mono (chainMap (mvInclU U V) n) :=
1376    SingularPair.chainMap_mono _
1377      (fun a b hab => Set.inclusion_injective Set.inter_subset_left hab) n
1378  exact mono_of_mono_fac (biprod.lift_fst _ _)
1379
1380lemma mvSESdeg_epi (n : ℕ) : Epi (mvSESdeg U V n).g := by
1381  show Epi (biprod.desc (uInc U V n) (vInc U V n))
1382  rw [ModuleCat.epi_iff_surjective]
1383  intro y
1384  induction y using freeInduction with
1385  | unit t =>
1386      rcases t.2 with h | h
1387      · refine ⟨(biprod.inl : Cgrp (TopCat.of U) n ⟶ _)
1388          (unitOf (liftIdx U t.1 h)), ?_⟩
1389        rw [← ModuleCat.comp_apply, biprod.inl_desc, uInc_unitOf]
1390        congr 1
1391      · refine ⟨(biprod.inr : Cgrp (TopCat.of V) n ⟶ _)
1392          (unitOf (liftIdx V t.1 h)), ?_⟩
1393        rw [← ModuleCat.comp_apply, biprod.inr_desc, vInc_unitOf]
1394        congr 1
1395  | zero => exact ⟨0, map_zero _⟩
1396  | add x y hx hy =>
1397      obtain ⟨a, ha⟩ := hx
1398      obtain ⟨b, hb⟩ := hy
1399      exact ⟨a + b, by rw [map_add, ha, hb]⟩
1400  | smulz c x hx =>
1401      obtain ⟨a, ha⟩ := hx
1402      exact ⟨c • a, by rw [mapSmul, ha]⟩
1403
1404/-- The heart of the Mayer-Vietoris exactness: a pair of chains on `U` and
1405`V` whose images in the small complex cancel comes from a chain on
1406`U ∩ V`. -/
1407lemma mv_middle_exact (n : ℕ) {a : ↥(Cgrp (TopCat.of U) n)}
1408    {b : ↥(Cgrp (TopCat.of V) n)}
1409    (hab : uInc U V n a + vInc U V n b = 0) :
1410    ∃ x : ↥(Cgrp (TopCat.of (U ∩ V : Set X)) n),
1411      chainMap (mvInclU U V) n x = a ∧ chainMap (mvInclV U V) n x = -b := by
1412  classical
1413  have hsupp : ∀ i ∈ suppOf a,
1414      Set.range ⇑(simplexEquiv X n (pushIdx U i)) ⊆ U ∩ V := by
1415    intro i hi
1416    by_cases hmem : ∃ j : Idx (TopCat.of V) n, vIdx U V j = uIdx U V i
1417    · obtain ⟨j, hj⟩ := hmem
1418      have hUV : pushIdx V j = pushIdx U i := congrArg Subtype.val hj
1419      intro x hx
1420      refine ⟨range_pushIdx U i hx, ?_⟩
1421      rw [← hUV] at hx
1422      exact range_pushIdx V j hx
1423    · exfalso
1424      have hne : coordAt i a ≠ 0 := mem_suppOf_iff.mp hi
1425      have h1 : coordAt (uIdx U V i) (uInc U V n a) = coordAt i a :=
1426        coordAt_map_eq (uIdx_injective U V n) (uInc_unitOf U V) i a
1427      have h2 : coordAt (uIdx U V i) (vInc U V n b) = 0 :=
1428        coordAt_map_notMem (vInc_unitOf U V) (fun j hj => hmem ⟨j, hj⟩) b
1429      have h3 : coordAt (uIdx U V i) (uInc U V n a) +
1430          coordAt (uIdx U V i) (vInc U V n b) = 0 := by
1431        rw [← coordAt_add, hab, coordAt_zero]
1432      rw [h1, h2, add_zero] at h3
1433      exact hne h3
1434  set x : ↥(Cgrp (TopCat.of (U ∩ V : Set X)) n) :=
1435    ∑ i ∈ (suppOf a).attach,
1436      coordAt i.1 a • unitOf (liftIdx (U ∩ V : Set X) (pushIdx U i.1)
1437        (hsupp i.1 i.2)) with hxdef
1438  have hterm : ∀ i ∈ (suppOf a).attach,
1439      chainMap (mvInclU U V) n (coordAt i.1 a •
1440        unitOf (liftIdx (U ∩ V : Set X) (pushIdx U i.1) (hsupp i.1 i.2))) =
1441        coordAt i.1 a • unitOf i.1 := by
1442    intro i _
1443    have hidx : (TopCat.toSSet.map (mvInclU U V)).app (op ⦋n⦌)
1444        (liftIdx (U ∩ V : Set X) (pushIdx U i.1) (hsupp i.1 i.2)) = i.1 := by
1445      apply pushIdx_injective U n
1446      rw [pushIdx_mvInclU, pushIdx_liftIdx]
1447    rw [mapSmul, chainMap_unitOf, hidx]
1448  have hxU : chainMap (mvInclU U V) n x = a := by
1449    calc chainMap (mvInclU U V) n x
1450        = ∑ i ∈ (suppOf a).attach, coordAt i.1 a • unitOf i.1 := by
1451          rw [hxdef, map_sum]
1452          exact Finset.sum_congr rfl hterm
1453      _ = ∑ i ∈ suppOf a, coordAt i a • unitOf i :=
1454          Finset.sum_attach (suppOf a) (fun i => coordAt i a • unitOf i)
1455      _ = a := (sum_coordAt_smul_unitOf a).symm
1456  have hxV : vInc U V n (chainMap (mvInclV U V) n x) = uInc U V n a := by
1457    rw [← ModuleCat.comp_apply, ← inclU_uInc_eq_inclV_vInc,
1458      ModuleCat.comp_apply, hxU]
1459  refine ⟨x, hxU, ?_⟩
1460  apply vInc_injective U V n
1461  rw [map_neg, hxV]
1462  exact eq_neg_of_add_eq_zero_left hab
1463
1464lemma mvSESdeg_exact (n : ℕ) : (mvSESdeg U V n).Exact := by
1465  rw [ShortComplex.moduleCat_exact_iff]
1466  intro z hz
1467  have hz' : uInc U V n
1468      ((biprod.fst : Cgrp (TopCat.of U) n ⊞ Cgrp (TopCat.of V) n ⟶ _) z) +
1469      vInc U V n
1470      ((biprod.snd : Cgrp (TopCat.of U) n ⊞ Cgrp (TopCat.of V) n ⟶ _) z) = 0 := by
1471    rw [← descApp]
1472    exact hz
1473  obtain ⟨x, hxU, hxV⟩ := mv_middle_exact U V n hz'
1474  refine ⟨x, ?_⟩
1475  apply biprod_elem_ext
1476  · rw [show (mvSESdeg U V n).f x = biprod.lift (chainMap (mvInclU U V) n)
1477      (-(chainMap (mvInclV U V) n)) x from rfl, fst_liftApp]
1478    exact hxU
1479  · rw [show (mvSESdeg U V n).f x = biprod.lift (chainMap (mvInclU U V) n)
1480      (-(chainMap (mvInclV U V) n)) x from rfl, snd_liftApp, negApp, hxV,
1481      neg_neg]
1482
1483lemma mvSESdeg_shortExact (n : ℕ) : (mvSESdeg U V n).ShortExact where
1484  exact := mvSESdeg_exact U V n
1485  mono_f := mvSESdeg_mono U V n
1486  epi_g := mvSESdeg_epi U V n
1487
1488lemma mvα_f_compat (n : ℕ) :
1489    (mvα U V).f n ≫
1490      (HomologicalComplex.biprodXIso (SC (TopCat.of U)) (SC (TopCat.of V)) n).hom =
1491      biprod.lift (chainMap (mvInclU U V) n) (-(chainMap (mvInclV U V) n)) := by
1492  have hf : mvα U V ≫ biprod.fst = sChainMap (mvInclU U V) := biprod.lift_fst _ _
1493  have hs : mvα U V ≫ biprod.snd = -(sChainMap (mvInclV U V)) := biprod.lift_snd _ _
1494  apply biprod.hom_ext
1495  · rw [assoc, HomologicalComplex.biprodXIso_hom_fst,
1496      ← HomologicalComplex.comp_f, hf]
1497    exact (biprod.lift_fst _ _).symm
1498  · rw [assoc, HomologicalComplex.biprodXIso_hom_snd,
1499      ← HomologicalComplex.comp_f, hs, HomologicalComplex.neg_f_apply]
1500    exact (biprod.lift_snd _ _).symm
1501
1502lemma mvβ_f_compat (n : ℕ) :
1503    (HomologicalComplex.biprodXIso (SC (TopCat.of U)) (SC (TopCat.of V)) n).inv ≫
1504      (mvβ U V).f n = biprod.desc (uInc U V n) (vInc U V n) := by
1505  have hu : (biprod.inl : SC (TopCat.of U) ⟶ _) ≫ mvβ U V = smallU U V :=
1506    biprod.inl_desc _ _
1507  have hv : (biprod.inr : SC (TopCat.of V) ⟶ _) ≫ mvβ U V = smallV U V :=
1508    biprod.inr_desc _ _
1509  apply biprod.hom_ext'
1510  · rw [← assoc, HomologicalComplex.inl_biprodXIso_inv, biprod.inl_desc,
1511      ← HomologicalComplex.comp_f, hu, smallU_f]
1512  · rw [← assoc, HomologicalComplex.inr_biprodXIso_inv, biprod.inr_desc,
1513      ← HomologicalComplex.comp_f, hv, smallV_f]
1514
1515/-- Degreewise, the Mayer-Vietoris short complex is isomorphic to the
1516concrete short complex of `ℤ`-modules. -/
1517noncomputable def mvSESdegIso (n : ℕ) :
1518    mvSESdeg U V n ≅ (mvSES U V).map
1519      (HomologicalComplex.eval (ModuleCat.{0} ℤ) (ComplexShape.down ℕ) n) := by
1520  refine ShortComplex.isoMk (Iso.refl _)
1521    (HomologicalComplex.biprodXIso (SC (TopCat.of U)) (SC (TopCat.of V)) n).symm
1522    (Iso.refl _) ?_ ?_
1523  · show (Iso.refl _).hom ≫ (mvα U V).f n =
1524      biprod.lift (chainMap (mvInclU U V) n) (-(chainMap (mvInclV U V) n)) ≫
1525        (HomologicalComplex.biprodXIso (SC (TopCat.of U)) (SC (TopCat.of V)) n).inv
1526    rw [Iso.refl_hom, id_comp, ← mvα_f_compat, assoc, Iso.hom_inv_id, comp_id]
1527  · show (HomologicalComplex.biprodXIso (SC (TopCat.of U))
1528      (SC (TopCat.of V)) n).inv ≫ (mvβ U V).f n =
1529      biprod.desc (uInc U V n) (vInc U V n) ≫ (Iso.refl _).hom
1530    rw [Iso.refl_hom, comp_id, mvβ_f_compat]
1531
1532lemma mvSES_degreewise_shortExact (n : ℕ) :
1533    ((mvSES U V).map
1534      (HomologicalComplex.eval (ModuleCat.{0} ℤ) (ComplexShape.down ℕ) n)).ShortExact :=
1535  ShortComplex.shortExact_of_iso (mvSESdegIso U V n) (mvSESdeg_shortExact U V n)
1536
1537/-- **Stage 3.** The Mayer-Vietoris sequence
1538`0 ⟶ C_*(U ∩ V) ⟶ C_*(U) ⊞ C_*(V) ⟶ C^{U,V}_*(X) ⟶ 0` is a short exact
1539sequence of chain complexes (no openness or covering hypotheses needed). -/
1540theorem mvSES_shortExact : (mvSES U V).ShortExact :=
1541  HomologicalComplex.shortExact_of_degreewise_shortExact _
1542    (mvSES_degreewise_shortExact U V)
1543
1544end MVSES
1545
1546/-! ## Stage 4: the Mayer-Vietoris long exact sequence -/
1547
1548section MVLES
1549
1550attribute [local instance] Limits.preservesBinaryBiproducts_of_preservesBiproducts
1551
1552/-- The degree-`n` homology functor on chain complexes of `ℤ`-modules. -/
1553noncomputable abbrev HF (n : ℕ) :
1554    ChainComplex (ModuleCat.{0} ℤ) ℕ ⥤ ModuleCat.{0} ℤ :=
1555  HomologicalComplex.homologyFunctor (ModuleCat.{0} ℤ) (ComplexShape.down ℕ) n
1556
1557/-- Additivity of homology: `H_n(C_*(U) ⊞ C_*(V)) ≅ H_n(U) ⊞ H_n(V)`. -/
1558noncomputable def homologyBiprodIso (n : ℕ) :
1559    (SC (TopCat.of U) ⊞ SC (TopCat.of V)).homology n ≅
1560      (SC (TopCat.of U)).homology n ⊞ (SC (TopCat.of V)).homology n :=
1561  (HF n).mapBiprod (SC (TopCat.of U)) (SC (TopCat.of V))
1562
1563/-- The Mayer-Vietoris pair map
1564`H_n(U ∩ V) ⟶ H_n(U) ⊞ H_n(V)`, `[c] ↦ ([i_* c], −[j_* c])`, induced by the
1565space-level inclusions `U ∩ V ↪ U` and `U ∩ V ↪ V`. -/
1566noncomputable def mvPair (n : ℕ) :
1567    (SC (TopCat.of (U ∩ V : Set X))).homology n ⟶
1568      (SC (TopCat.of U)).homology n ⊞ (SC (TopCat.of V)).homology n :=
1569  biprod.lift (HomologicalComplex.homologyMap (sChainMap (mvInclU U V)) n)
1570    (-(HomologicalComplex.homologyMap (sChainMap (mvInclV U V)) n))
1571
1572/-- The Mayer-Vietoris sum map `H_n(U) ⊞ H_n(V) ⟶ H_n(X)`,
1573`([a], [b]) ↦ [k_* a] + [l_* b]`, induced by the space-level inclusions
1574`U ↪ X` and `V ↪ X`. -/
1575noncomputable def mvSum (n : ℕ) :
1576    (SC (TopCat.of U)).homology n ⊞ (SC (TopCat.of V)).homology n ⟶
1577      (SC X).homology n :=
1578  biprod.desc
1579    (HomologicalComplex.homologyMap (sChainMap (SingularPair.subInc X U)) n)
1580    (HomologicalComplex.homologyMap (sChainMap (SingularPair.subInc X V)) n)
1581
1582variable {U V}
1583
1584/-- **The Mayer-Vietoris connecting homomorphism**
1585`∂ : H_{n+1}(X) ⟶ H_n(U ∩ V)`, transported across the small-chains
1586isomorphism of Stage 2. -/
1587noncomputable def mvδ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1588    (n : ℕ) :
1589    (SC X).homology (n + 1) ⟶ (SC (TopCat.of (U ∩ V : Set X))).homology n :=
1590  (smallChainsHomologyIso hU hV hUV (n + 1)).inv ≫
1591    (mvSES_shortExact U V).δ (n + 1) n (ComplexShape.down_mk _ _ rfl)
1592
1593lemma smallIso_hom (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1594    (n : ℕ) :
1595    (smallChainsHomologyIso hU hV hUV n).hom =
1596      HomologicalComplex.homologyMap (smallι U V) n := rfl
1597
1598variable (U V)
1599
1600lemma homologyMap_mvα_compat (n : ℕ) :
1601    HomologicalComplex.homologyMap (mvα U V) n ≫ (homologyBiprodIso U V n).hom =
1602      mvPair U V n := by
1603  have h := Limits.biprod.map_lift_mapBiprod (HF n)
1604    (SC (TopCat.of U)) (SC (TopCat.of V))
1605    (sChainMap (mvInclU U V)) (-(sChainMap (mvInclV U V)))
1606  rw [Functor.map_neg] at h
1607  exact h
1608
1609lemma mvPair_eq (n : ℕ) :
1610    mvPair U V n = HomologicalComplex.homologyMap (mvα U V) n ≫
1611      (homologyBiprodIso U V n).hom :=
1612  (homologyMap_mvα_compat U V n).symm
1613
1614lemma homologyMap_mvβ_compat (n : ℕ) :
1615    (homologyBiprodIso U V n).inv ≫
1616      HomologicalComplex.homologyMap (mvβ U V) n ≫
1617        HomologicalComplex.homologyMap (smallι U V) n = mvSum U V n := by
1618  have h := Limits.biprod.mapBiprod_inv_map_desc (HF n)
1619    (SC (TopCat.of U)) (SC (TopCat.of V)) (smallU U V) (smallV U V)
1620  have h2 : (homologyBiprodIso U V n).inv ≫
1621      HomologicalComplex.homologyMap (mvβ U V) n =
1622      biprod.desc ((HF n).map (smallU U V)) ((HF n).map (smallV U V)) := h
1623  rw [← assoc, h2]
1624  apply biprod.hom_ext'
1625  · rw [← assoc, biprod.inl_desc]
1626    have h3 : (biprod.inl :
1627        (SC (TopCat.of U)).homology n ⟶ _) ≫ mvSum U V n =
1628        HomologicalComplex.homologyMap
1629          (sChainMap (SingularPair.subInc X U)) n := biprod.inl_desc _ _
1630    rw [h3, ← smallU_comp_smallι]
1631    exact ((HF n).map_comp _ _).symm
1632  · rw [← assoc, biprod.inr_desc]
1633    have h3 : (biprod.inr :
1634        (SC (TopCat.of V)).homology n ⟶ _) ≫ mvSum U V n =
1635        HomologicalComplex.homologyMap
1636          (sChainMap (SingularPair.subInc X V)) n := biprod.inr_desc _ _
1637    rw [h3, ← smallV_comp_smallι]
1638    exact ((HF n).map_comp _ _).symm
1639
1640lemma mvSum_eq (n : ℕ) :
1641    mvSum U V n = (homologyBiprodIso U V n).inv ≫
1642      HomologicalComplex.homologyMap (mvβ U V) n ≫
1643        HomologicalComplex.homologyMap (smallι U V) n :=
1644  (homologyMap_mvβ_compat U V n).symm
1645
1646/-- `H_n(U ∩ V) → H_n(U) ⊞ H_n(V) → H_n(X)` composes to zero. -/
1647lemma mvPair_comp_mvSum (n : ℕ) : mvPair U V n ≫ mvSum U V n = 0 := by
1648  rw [mvPair_eq, mvSum_eq, assoc, Iso.hom_inv_id_assoc, ← assoc,
1649    ← HomologicalComplex.homologyMap_comp]
1650  have h : mvα U V ≫ mvβ U V = 0 := mvα_comp_mvβ U V
1651  rw [h, HomologicalComplex.homologyMap_zero, zero_comp]
1652
1653variable {U V}
1654
1655/-- `H_{n+1}(U) ⊞ H_{n+1}(V) → H_{n+1}(X) → H_n(U ∩ V)` composes to
1656zero. -/
1657lemma mvSum_comp_mvδ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1658    (n : ℕ) :
1659    mvSum U V (n + 1) ≫ mvδ hU hV hUV n = 0 := by
1660  have h : HomologicalComplex.homologyMap (mvβ U V) (n + 1) ≫
1661      (mvSES_shortExact U V).δ (n + 1) n (ComplexShape.down_mk _ _ rfl) = 0 :=
1662    (mvSES_shortExact U V).comp_δ (n + 1) n (ComplexShape.down_mk _ _ rfl)
1663  rw [mvSum_eq, mvδ, ← smallIso_hom hU hV hUV (n + 1)]
1664  simp only [assoc]
1665  rw [Iso.hom_inv_id_assoc, h, comp_zero]
1666
1667/-- `H_{n+1}(X) → H_n(U ∩ V) → H_n(U) ⊞ H_n(V)` composes to zero. -/
1668lemma mvδ_comp_mvPair (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1669    (n : ℕ) :
1670    mvδ hU hV hUV n ≫ mvPair U V n = 0 := by
1671  have h : (mvSES_shortExact U V).δ (n + 1) n (ComplexShape.down_mk _ _ rfl) ≫
1672      HomologicalComplex.homologyMap (mvα U V) n = 0 :=
1673    (mvSES_shortExact U V).δ_comp (n + 1) n (ComplexShape.down_mk _ _ rfl)
1674  rw [mvδ, mvPair_eq]
1675  simp only [assoc]
1676  rw [reassoc_of% h, zero_comp, comp_zero]
1677
1678/-- **Mayer-Vietoris, exactness at `H_n(U ∩ V)`**:
1679`H_{n+1}(X) ⟶ H_n(U ∩ V) ⟶ H_n(U) ⊞ H_n(V)` is exact. -/
1680theorem mv_exact₁ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1681    (n : ℕ) :
1682    (ShortComplex.mk (mvδ hU hV hUV n) (mvPair U V n)
1683      (mvδ_comp_mvPair hU hV hUV n)).Exact := by
1684  refine ShortComplex.exact_of_iso ?_
1685    ((mvSES_shortExact U V).homology_exact₁ (n + 1) n
1686      (ComplexShape.down_mk _ _ rfl))
1687  refine ShortComplex.isoMk (smallChainsHomologyIso hU hV hUV (n + 1))
1688    (Iso.refl _) (homologyBiprodIso U V n) ?_ ?_
1689  · show (smallChainsHomologyIso hU hV hUV (n + 1)).hom ≫ mvδ hU hV hUV n =
1690      (mvSES_shortExact U V).δ (n + 1) n (ComplexShape.down_mk _ _ rfl) ≫
1691        (Iso.refl _).hom
1692    rw [mvδ, Iso.hom_inv_id_assoc, Iso.refl_hom, comp_id]
1693  · show (Iso.refl _).hom ≫ mvPair U V n =
1694      HomologicalComplex.homologyMap (mvα U V) n ≫ (homologyBiprodIso U V n).hom
1695    rw [Iso.refl_hom, id_comp, mvPair_eq]
1696
1697/-- **Mayer-Vietoris, exactness at `H_n(U) ⊞ H_n(V)`**:
1698`H_n(U ∩ V) ⟶ H_n(U) ⊞ H_n(V) ⟶ H_n(X)` is exact (all degrees, including
1699`0`). -/
1700theorem mv_exact₂ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1701    (n : ℕ) :
1702    (ShortComplex.mk (mvPair U V n) (mvSum U V n)
1703      (mvPair_comp_mvSum U V n)).Exact := by
1704  refine ShortComplex.exact_of_iso ?_
1705    ((mvSES_shortExact U V).homology_exact₂ n)
1706  refine ShortComplex.isoMk (Iso.refl _) (homologyBiprodIso U V n)
1707    (smallChainsHomologyIso hU hV hUV n) ?_ ?_
1708  · show (Iso.refl _).hom ≫ mvPair U V n =
1709      HomologicalComplex.homologyMap (mvα U V) n ≫ (homologyBiprodIso U V n).hom
1710    rw [Iso.refl_hom, id_comp, mvPair_eq]
1711  · show (homologyBiprodIso U V n).hom ≫ mvSum U V n =
1712      HomologicalComplex.homologyMap (mvβ U V) n ≫
1713        (smallChainsHomologyIso hU hV hUV n).hom
1714    rw [mvSum_eq, Iso.hom_inv_id_assoc, smallIso_hom]
1715
1716/-- **Mayer-Vietoris, exactness at `H_{n+1}(X)`**:
1717`H_{n+1}(U) ⊞ H_{n+1}(V) ⟶ H_{n+1}(X) ⟶ H_n(U ∩ V)` is exact. -/
1718theorem mv_exact₃ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
1719    (n : ℕ) :
1720    (ShortComplex.mk (mvSum U V (n + 1)) (mvδ hU hV hUV n)
1721      (mvSum_comp_mvδ hU hV hUV n)).Exact := by
1722  refine ShortComplex.exact_of_iso ?_
1723    ((mvSES_shortExact U V).homology_exact₃ (n + 1) n
1724      (ComplexShape.down_mk _ _ rfl))
1725  refine ShortComplex.isoMk (homologyBiprodIso U V (n + 1))
1726    (smallChainsHomologyIso hU hV hUV (n + 1)) (Iso.refl _) ?_ ?_
1727  · show (homologyBiprodIso U V (n + 1)).hom ≫ mvSum U V (n + 1) =
1728      HomologicalComplex.homologyMap (mvβ U V) (n + 1) ≫
1729        (smallChainsHomologyIso hU hV hUV (n + 1)).hom
1730    rw [mvSum_eq, Iso.hom_inv_id_assoc, smallIso_hom]
1731  · show (smallChainsHomologyIso hU hV hUV (n + 1)).hom ≫ mvδ hU hV hUV n =
1732      (mvSES_shortExact U V).δ (n + 1) n (ComplexShape.down_mk _ _ rfl) ≫
1733        (Iso.refl _).hom
1734    rw [mvδ, Iso.hom_inv_id_assoc, Iso.refl_hom, comp_id]
1735
1736/-- **The degree-`0` tail**: `H_0(U) ⊞ H_0(V) ⟶ H_0(X)` is surjective; the
1737Mayer-Vietoris sequence ends `⋯ ⟶ H_0(U) ⊞ H_0(V) ⟶ H_0(X) ⟶ 0`. -/
1738theorem mvSum_epi_zero (hU : IsOpen U) (hV : IsOpen V)
1739    (hUV : U ∪ V = Set.univ) : Epi (mvSum U V 0) := by
1740  haveI h1 : Epi (HomologicalComplex.homologyMap (mvβ U V) 0) := by
1741    refine epi_homologyMap_chain_zero (mvβ U V) ?_
1742    intro y
1743    have hepi : Epi ((mvβ U V).f 0) := (mvSES_degreewise_shortExact U V 0).epi_g
1744    have hsurj : Function.Surjective ((mvβ U V).f 0) :=
1745      (ModuleCat.epi_iff_surjective _).mp hepi
1746    obtain ⟨x, hx⟩ := hsurj y
1747    refine ⟨x, 0, ?_⟩
1748    rw [map_zero, add_zero, hx]
1749  haveI h2 : IsIso (HomologicalComplex.homologyMap (smallι U V) 0) :=
1750    smallι_isIso_homologyMap hU hV hUV 0
1751  rw [mvSum_eq]
1752  infer_instance
1753
1754/-- **Sanity lock**: when `U = univ` (so `U` alone already covers `X`), the
1755Mayer-Vietoris sum map `H_n(U) ⊞ H_n(V) ⟶ H_n(X)` is an epimorphism in
1756every degree, because its first component is induced by the isomorphism
1757`univ ≃ X`. -/
1758theorem mvSum_epi_of_left_univ (V : Set X) (n : ℕ) :
1759    Epi (mvSum (Set.univ : Set X) V n) := by
1760  haveI hiso : IsIso (SingularPair.subInc X (Set.univ : Set X)) := by
1761    refine ⟨TopCat.ofHom ⟨fun x => ⟨x, trivial⟩,
1762      Continuous.subtype_mk continuous_id fun _ => trivial⟩, ?_, ?_⟩
1763    · ext x
1764      rfl
1765    · ext x
1766      rfl
1767  haveI h1 : IsIso (sChainMap (SingularPair.subInc X (Set.univ : Set X))) := by
1768    show IsIso (((AlgebraicTopology.singularChainComplexFunctor
1769      (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)).map
1770      (SingularPair.subInc X (Set.univ : Set X)))
1771    infer_instance
1772  haveI h2 : Epi (HomologicalComplex.homologyMap
1773      (sChainMap (SingularPair.subInc X (Set.univ : Set X))) n) := by
1774    haveI : IsIso (HomologicalComplex.homologyMap
1775        (sChainMap (SingularPair.subInc X (Set.univ : Set X))) n) := by
1776      show IsIso ((HF n).map (sChainMap (SingularPair.subInc X (Set.univ : Set X))))
1777      infer_instance
1778    infer_instance
1779  have hfac : (biprod.inl :
1780      (SC (TopCat.of (Set.univ : Set X))).homology n ⟶ _) ≫
1781      mvSum (Set.univ : Set X) V n =
1782      HomologicalComplex.homologyMap
1783        (sChainMap (SingularPair.subInc X (Set.univ : Set X))) n :=
1784    biprod.inl_desc _ _
1785  exact epi_of_epi_fac hfac
1786
1787end MVLES
1788
1789end SingularMayerVietoris
1790end Foundation
1791end IndisputableMonolith
1792