IndisputableMonolith.Foundation.SingularPair

   1/-
   2The long exact sequence of a pair in singular homology.
   3
   4Layer 2 of the excision spine (layer 1: `SingularPrism.lean`, homotopy
   5invariance).  For an injective continuous map `f : A ⟶ X` (in particular a
   6subspace inclusion) this file proves, with `ℤ` coefficients:
   7
   81. the induced chain map `C_*(A) ⟶ C_*(X)` is a degreewise (split)
   9   monomorphism, hence a monomorphism of chain complexes
  10   (`chainMap_mono`, `sChainMap_mono`);
  112. the relative singular chain complex `C_*(X, A)` is the cokernel
  12   (`relSC`), giving a short exact sequence of chain complexes
  13   `0 ⟶ C_*(A) ⟶ C_*(X) ⟶ C_*(X, A) ⟶ 0` (`pairSES`,
  14   `pairSES_shortExact`, degreewise form `pairSES_degreewise_shortExact`);
  153. the long exact sequence of the pair via Mathlib's homology sequence:
  16   the connecting homomorphism `pairδ : H_{n+1}(X, A) ⟶ H_n(A)` and the
  17   three exactness statements `pair_les_exact₁/₂/₃`;
  184. the sanity theorem `relative_homology_id_isZero`: for the identity
  19   inclusion `A = X` the relative homology vanishes in every degree
  20   (guards against a degenerate cokernel definition).
  21
  22Conventions (`Idx`, `Cgrp`, `gen`, `SC`, `chainMap`, `sChainMap`,
  23`gen_map`, `toSSetObjEquiv_map`) are inherited from `SingularPrism`.
  24-/
  25import IndisputableMonolith.Foundation.SingularPrism
  26import Mathlib.Algebra.Homology.HomologicalComplexAbelian
  27import Mathlib.Algebra.Homology.HomologySequence
  28
  29namespace IndisputableMonolith
  30namespace Foundation
  31namespace SingularPair
  32
  33open CategoryTheory Category Limits AlgebraicTopology Simplicial Opposite
  34open SingularPrism
  35
  36/-! ## Part 1: injectivity on singular simplices and the degreewise mono -/
  37
  38variable {A X : TopCat.{0}}
  39
  40/-- An injective continuous map induces an injective map on singular
  41`n`-simplices (postcomposition with an injective map is injective). -/
  42lemma toSSet_map_app_injective (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
  43    Function.Injective ((TopCat.toSSet.map f).app (op ⦋n⦌)) := by
  44  intro a b hab
  45  have h1 : f.hom.comp (A.toSSetObjEquiv (op ⦋n⦌) a) =
  46      f.hom.comp (A.toSSetObjEquiv (op ⦋n⦌) b) := by
  47    rw [← toSSetObjEquiv_map f a, ← toSSetObjEquiv_map f b, hab]
  48  have h2 : A.toSSetObjEquiv (op ⦋n⦌) a = A.toSSetObjEquiv (op ⦋n⦌) b := by
  49    ext t
  50    apply hf
  51    simpa only [ContinuousMap.comp_apply] using ContinuousMap.congr_fun h1 t
  52  exact (A.toSSetObjEquiv (op ⦋n⦌)).injective h2
  53
  54open Classical in
  55/-- The retraction of the degree-`n` chain map of `f`, defined on generators:
  56a singular simplex of `X` in the image of `f` goes to (a choice of) its
  57preimage, everything else goes to `0`.  For injective `f` this splits
  58`chainMap f n`. -/
  59noncomputable def genRetract (f : A ⟶ X) (n : ℕ) : Cgrp X n ⟶ Cgrp A n :=
  60  Sigma.desc fun x =>
  61    if hx : ∃ a : Idx A n, (TopCat.toSSet.map f).app (op ⦋n⦌) a = x then
  62      gen A n hx.choose
  63    else 0
  64
  65/-- For injective `f`, `genRetract` retracts the chain map on generators. -/
  66lemma gen_comp_genRetract (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ)
  67    (a : Idx A n) :
  68    gen X n ((TopCat.toSSet.map f).app (op ⦋n⦌) a) ≫ genRetract f n = gen A n a := by
  69  unfold genRetract
  70  rw [Sigma.ι_desc]
  71  have hx : ∃ a' : Idx A n, (TopCat.toSSet.map f).app (op ⦋n⦌) a' =
  72      (TopCat.toSSet.map f).app (op ⦋n⦌) a := ⟨a, rfl⟩
  73  rw [dif_pos hx]
  74  exact congrArg (gen A n) (toSSet_map_app_injective f hf n hx.choose_spec)
  75
  76/-- The chain map splits: `chainMap f n ≫ genRetract f n = 𝟙`. -/
  77lemma chainMap_comp_genRetract (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
  78    chainMap f n ≫ genRetract f n = 𝟙 (Cgrp A n) := by
  79  apply Sigma.hom_ext
  80  intro a
  81  rw [comp_id, ← assoc, gen_map f n a]
  82  exact gen_comp_genRetract f hf n a
  83
  84/-- An injective continuous map induces a degreewise monomorphism of
  85singular chain complexes. -/
  86lemma chainMap_mono (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
  87    Mono (chainMap f n) :=
  88  mono_of_mono_fac (chainMap_comp_genRetract f hf n)
  89
  90/-- An injective continuous map induces a monomorphism of singular chain
  91complexes. -/
  92lemma sChainMap_mono (f : A ⟶ X) (hf : Function.Injective f.hom) :
  93    Mono (sChainMap f) :=
  94  HomologicalComplex.mono_of_mono_f _ fun n => chainMap_mono f hf n
  95
  96/-! ## Part 2: the relative chain complex and the short exact sequence -/
  97
  98/-- The relative singular chain complex `C_*(X, A)`: the cokernel of the
  99chain map induced by `f : A ⟶ X` (degreewise the quotient
 100`C_n(X) / C_n(A)`, with the induced differential). -/
 101noncomputable def relSC (f : A ⟶ X) : ChainComplex (ModuleCat.{0} ℤ) ℕ :=
 102  cokernel (sChainMap f)
 103
 104/-- The projection `C_*(X) ⟶ C_*(X, A)`. -/
 105noncomputable def relπ (f : A ⟶ X) : SC X ⟶ relSC f :=
 106  cokernel.π (sChainMap f)
 107
 108/-- The short complex `0 ⟶ C_*(A) ⟶ C_*(X) ⟶ C_*(X, A) ⟶ 0` of singular
 109chain complexes attached to `f : A ⟶ X`. -/
 110noncomputable def pairSES (f : A ⟶ X) :
 111    ShortComplex (ChainComplex (ModuleCat.{0} ℤ) ℕ) :=
 112  ShortComplex.mk (sChainMap f) (relπ f) (cokernel.condition _)
 113
 114/-- For an injective continuous map, the sequence
 115`0 ⟶ C_*(A) ⟶ C_*(X) ⟶ C_*(X, A) ⟶ 0` is short exact. -/
 116lemma pairSES_shortExact (f : A ⟶ X) (hf : Function.Injective f.hom) :
 117    (pairSES f).ShortExact where
 118  exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel (sChainMap f))
 119  mono_f := sChainMap_mono f hf
 120  epi_g := by
 121    show Epi (cokernel.π (sChainMap f))
 122    infer_instance
 123
 124/-- Degreewise form of the short exact sequence: in every degree `n`,
 125`0 ⟶ C_n(A) ⟶ C_n(X) ⟶ C_n(X, A) ⟶ 0` is a short exact sequence of
 126`ℤ`-modules. -/
 127lemma pairSES_degreewise_shortExact (f : A ⟶ X) (hf : Function.Injective f.hom)
 128    (n : ℕ) :
 129    ((pairSES f).map
 130      (HomologicalComplex.eval (ModuleCat.{0} ℤ) (ComplexShape.down ℕ) n)).ShortExact :=
 131  (pairSES_shortExact f hf).map_of_exact _
 132
 133/-! ## Part 3: the long exact sequence of the pair -/
 134
 135/-- The connecting homomorphism `∂ : H_{n+1}(X, A) ⟶ H_n(A)` of the pair. -/
 136noncomputable def pairδ (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
 137    (relSC f).homology (n + 1) ⟶ (SC A).homology n :=
 138  (pairSES_shortExact f hf).δ (n + 1) n (ComplexShape.down_mk _ _ rfl)
 139
 140/-- `∂ ≫ H_n(A → X) = 0`. -/
 141lemma pairδ_comp (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
 142    pairδ f hf n ≫ HomologicalComplex.homologyMap (sChainMap f) n = 0 :=
 143  (pairSES_shortExact f hf).δ_comp (n + 1) n (ComplexShape.down_mk _ _ rfl)
 144
 145/-- `H_{n+1}(X → (X, A)) ≫ ∂ = 0`. -/
 146lemma comp_pairδ (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
 147    HomologicalComplex.homologyMap (relπ f) (n + 1) ≫ pairδ f hf n = 0 :=
 148  (pairSES_shortExact f hf).comp_δ (n + 1) n (ComplexShape.down_mk _ _ rfl)
 149
 150/-- The composite `H_n(A) ⟶ H_n(X) ⟶ H_n(X, A)` vanishes. -/
 151lemma pair_homologyMap_comp_zero (f : A ⟶ X) (n : ℕ) :
 152    HomologicalComplex.homologyMap (sChainMap f) n ≫
 153      HomologicalComplex.homologyMap (relπ f) n = 0 := by
 154  rw [← HomologicalComplex.homologyMap_comp, relπ, cokernel.condition,
 155    HomologicalComplex.homologyMap_zero]
 156
 157/-- **LES of the pair, exactness at `H_n(A)`**:
 158`H_{n+1}(X, A) ⟶ H_n(A) ⟶ H_n(X)` is exact. -/
 159lemma pair_les_exact₁ (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
 160    (ShortComplex.mk (pairδ f hf n)
 161      (HomologicalComplex.homologyMap (sChainMap f) n)
 162      (pairδ_comp f hf n)).Exact :=
 163  (pairSES_shortExact f hf).homology_exact₁ (n + 1) n (ComplexShape.down_mk _ _ rfl)
 164
 165/-- **LES of the pair, exactness at `H_n(X)`**:
 166`H_n(A) ⟶ H_n(X) ⟶ H_n(X, A)` is exact (all degrees `n`, including `0`). -/
 167lemma pair_les_exact₂ (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
 168    (ShortComplex.mk (HomologicalComplex.homologyMap (sChainMap f) n)
 169      (HomologicalComplex.homologyMap (relπ f) n)
 170      (pair_homologyMap_comp_zero f n)).Exact :=
 171  (pairSES_shortExact f hf).homology_exact₂ n
 172
 173/-- **LES of the pair, exactness at `H_{n+1}(X, A)`**:
 174`H_{n+1}(X) ⟶ H_{n+1}(X, A) ⟶ H_n(A)` is exact. -/
 175lemma pair_les_exact₃ (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
 176    (ShortComplex.mk (HomologicalComplex.homologyMap (relπ f) (n + 1))
 177      (pairδ f hf n)
 178      (comp_pairδ f hf n)).Exact :=
 179  (pairSES_shortExact f hf).homology_exact₃ (n + 1) n (ComplexShape.down_mk _ _ rfl)
 180
 181/-! ## Part 4: subspace inclusions -/
 182
 183/-- The inclusion of a subspace `S : Set X` as a morphism of `TopCat`. -/
 184noncomputable def subInc (X : TopCat.{0}) (S : Set X) : TopCat.of S ⟶ X :=
 185  TopCat.ofHom ⟨Subtype.val, continuous_subtype_val⟩
 186
 187lemma subInc_injective (X : TopCat.{0}) (S : Set X) :
 188    Function.Injective (subInc X S).hom :=
 189  fun _ _ h => Subtype.ext h
 190
 191/-- The short exact sequence `0 ⟶ C_*(S) ⟶ C_*(X) ⟶ C_*(X, S) ⟶ 0` for a
 192subspace `S : Set X`; all the LES lemmas above apply with
 193`f := subInc X S`, `hf := subInc_injective X S`. -/
 194lemma subpair_shortExact (X : TopCat.{0}) (S : Set X) :
 195    (pairSES (subInc X S)).ShortExact :=
 196  pairSES_shortExact _ (subInc_injective X S)
 197
 198/-! ## Part 5: sanity theorem, `H_n(X, X) = 0` -/
 199
 200/-- For the identity inclusion the relative chain complex is zero. -/
 201lemma relSC_id_isZero (X : TopCat.{0}) : IsZero (relSC (𝟙 X)) := by
 202  have h : sChainMap (𝟙 X) = 𝟙 (SC X) := CategoryTheory.Functor.map_id _ _
 203  have : Epi (sChainMap (𝟙 X)) := by rw [h]; infer_instance
 204  exact isZero_cokernel_of_epi _
 205
 206/-- **Sanity**: the relative homology of the identity pair vanishes in every
 207degree: `H_n(X, X) = 0`.  This locks the semantics of the cokernel
 208definition of the relative complex. -/
 209theorem relative_homology_id_isZero (X : TopCat.{0}) (n : ℕ) :
 210    IsZero ((relSC (𝟙 X)).homology n) :=
 211  (HomologicalComplex.homologyFunctor (ModuleCat.{0} ℤ)
 212    (ComplexShape.down ℕ) n).map_isZero (relSC_id_isZero X)
 213
 214/-! ### Frontier note
 215
 216Complete for this layer: degreewise split mono (`chainMap_mono`,
 217`sChainMap_mono`), the relative complex as cokernel (`relSC`), the short
 218exact sequence of chain complexes with its degreewise form
 219(`pairSES_shortExact`, `pairSES_degreewise_shortExact`), the connecting
 220homomorphism (`pairδ`) and the three exactness statements of the long
 221exact sequence of the pair (`pair_les_exact₁/₂/₃`), the subspace
 222specialization (`subInc`, `subpair_shortExact`), and the sanity theorem
 223`relative_homology_id_isZero` (`H_n(X, X) = 0`).
 224
 225Deferred (new scope, not required for the excision spine):
 226
 227* Reduced homology (augmentation `C_0(X) → ℤ` and the reduced LES): not
 228  needed by the layer-3 excision argument, which works with the relative
 229  complexes directly; cheap to add later via the augmented complex.
 230* A concrete degreewise description `C_n(X, A) ≅ C_n(X)/C_n(A)` as an
 231  explicit quotient module: downstream work should instead use
 232  `pairSES_degreewise_shortExact` (degree-`n` projection is the cokernel
 233  of the degree-`n` inclusion), which is the categorical form of the same
 234  fact.
 235-/
 236
 237end SingularPair
 238end Foundation
 239end IndisputableMonolith
 240