2607.19276v1 / Norine/ChainObstruction.lean

all files

import Mathlib

/-!
# The algebraic chain-level Borsuk--Ulam obstruction

This is the algebraic argument of Lemma 3.1 in the paper.  It is deliberately
stated for one ambient `F₂`-vector space on each side; a graded chain complex
embeds in the direct sum of its degrees, with the boundary extended by zero.
The hypotheses mention only the finite Smith tower actually used by the proof.
-/

namespace Norine

noncomputable section

abbrev F₂ := ZMod 2

section Descent

variable {D : Type*} [AddCommGroup D] [Module F₂ D]

private theorem add_self_eq_zero (x : D) : x + x = 0 := by
  exact ZModModule.add_self x

/-- The descending half of the chain obstruction.  If `ν²=0`, `ker ν = im ν`,
`∂ν=ν∂`, and the displayed finite tower dies in degree `d+1`, its degree-zero
term has augmentation zero. -/
theorem norm_tower_aug_zero
    (boundary norm : D →ₗ[F₂] D) (aug : D →ₗ[F₂] F₂)
    (boundary_sq : boundary.comp boundary = 0)
    (boundary_norm : boundary.comp norm = norm.comp boundary)
    (aug_boundary : aug.comp boundary = 0)
    (aug_norm : aug.comp norm = 0)
    (norm_exact : ∀ y : D, norm y = 0 → ∃ z : D, norm z = y)
    (d : ℕ) (y : ℕ → D)
    (tower : ∀ i ≤ d, boundary (y (i + 1)) = norm (y i))
    (top : y (d + 1) = 0) :
    aug (y 0) = 0 := by
  induction d generalizing y with
  | zero =>
      have hnorm : norm (y 0) = 0 := by
        rw [← tower 0 (by omega), top]
        simp
      obtain ⟨z, hz⟩ := norm_exact (y 0) hnorm
      rw [← hz]
      exact LinearMap.congr_fun aug_norm z
  | succ d ih =>
      have hnorm_top : norm (y (d + 1)) = 0 := by
        rw [← tower (d + 1) (by omega), top]
        simp
      obtain ⟨z, hz⟩ := norm_exact (y (d + 1)) hnorm_top
      let y' : ℕ → D := fun i ↦
        if i = d then y i + boundary z
        else if i = d + 1 then 0
        else y i
      have hy'_top : y' (d + 1) = 0 := by
        simp [y']
      have hy'_tower : ∀ i ≤ d, boundary (y' (i + 1)) = norm (y' i) := by
        intro i hi
        by_cases hid : i = d
        · subst i
          have hcomm := LinearMap.congr_fun boundary_norm z
          simp only [LinearMap.comp_apply] at hcomm
          change boundary (y' (d + 1)) = norm (y' d)
          rw [show y' (d + 1) = 0 by simp [y'],
            show y' d = y d + boundary z by simp [y']]
          rw [map_zero, map_add, ← hcomm, hz, tower d (by omega),
            add_self_eq_zero]
        · have hilt : i < d := lt_of_le_of_ne hi hid
          have hi_ne_succ : i ≠ d + 1 := by omega
          have his_ne_succ : i + 1 ≠ d + 1 := by omega
          by_cases hisd : i + 1 = d
          · have hsq := LinearMap.congr_fun boundary_sq z
            simp only [LinearMap.comp_apply, LinearMap.zero_apply] at hsq
            change boundary (y' (i + 1)) = norm (y' i)
            have hy_s : y' (i + 1) = y (i + 1) + boundary z := by
              dsimp only [y']
              rw [if_pos hisd]
            have hy_i : y' i = y i := by
              dsimp only [y']
              rw [if_neg hid, if_neg hi_ne_succ]
            rw [hy_s, hy_i, map_add, hsq, add_zero, tower i (by omega)]
          · change boundary (y' (i + 1)) = norm (y' i)
            have hy_s : y' (i + 1) = y (i + 1) := by
              dsimp only [y']
              rw [if_neg hisd, if_neg his_ne_succ]
            have hy_i : y' i = y i := by
              dsimp only [y']
              rw [if_neg hid, if_neg hi_ne_succ]
            rw [hy_s, hy_i, tower i (by omega)]
      have hzero := ih y' hy'_tower hy'_top
      by_cases hd0 : d = 0
      · subst d
        simpa only [y', if_pos rfl, map_add, ← LinearMap.comp_apply,
          aug_boundary, LinearMap.zero_apply, add_zero] using hzero
      · have hzero_ne : (0 : ℕ) ≠ d := Ne.symm hd0
        have hzero_ne_succ : (0 : ℕ) ≠ d + 1 := by omega
        simpa only [y', if_neg hzero_ne, if_neg hzero_ne_succ] using hzero

end Descent

section Obstruction

variable {C D : Type*}
variable [AddCommGroup C] [Module F₂ C]
variable [AddCommGroup D] [Module F₂ D]

/-- Lemma 3.1 in the finite-tower form used by the paper.

`x` is the Smith tower in the source:
`∂xᵢ₊₁ = (1+T)xᵢ`, with augmentation one at its base.
Equivariance sends it to such a tower in the target.  Boundedness kills its
top, and `norm_tower_aug_zero` contradicts augmentation preservation.
-/
theorem chain_level_borsuk_ulam
    (boundaryC normC : C →ₗ[F₂] C) (augC : C →ₗ[F₂] F₂)
    (boundaryD normD : D →ₗ[F₂] D) (augD : D →ₗ[F₂] F₂)
    (φ : C →ₗ[F₂] D)
    (map_boundary : boundaryD.comp φ = φ.comp boundaryC)
    (map_norm : normD.comp φ = φ.comp normC)
    (map_aug : augD.comp φ = augC)
    (boundaryD_sq : boundaryD.comp boundaryD = 0)
    (boundaryD_norm : boundaryD.comp normD = normD.comp boundaryD)
    (augD_boundary : augD.comp boundaryD = 0)
    (augD_norm : augD.comp normD = 0)
    (normD_exact : ∀ y : D, normD y = 0 → ∃ z : D, normD z = y)
    (d : ℕ) (x : ℕ → C)
    (source_tower : ∀ i ≤ d, boundaryC (x (i + 1)) = normC (x i))
    (source_aug : augC (x 0) = 1)
    (target_bounded : φ (x (d + 1)) = 0) :
    False := by
  let y : ℕ → D := fun i ↦ φ (x i)
  have target_tower : ∀ i ≤ d, boundaryD (y (i + 1)) = normD (y i) := by
    intro i hi
    have hb := LinearMap.congr_fun map_boundary (x (i + 1))
    have hn := LinearMap.congr_fun map_norm (x i)
    simp only [LinearMap.comp_apply] at hb hn
    change boundaryD (φ (x (i + 1))) = normD (φ (x i))
    rw [hb, source_tower i hi]
    exact hn.symm
  have target_aug_zero : augD (y 0) = 0 :=
    norm_tower_aug_zero boundaryD normD augD boundaryD_sq boundaryD_norm
      augD_boundary augD_norm normD_exact d y target_tower target_bounded
  have target_aug_one : augD (y 0) = 1 := by
    have ha := LinearMap.congr_fun map_aug (x 0)
    simp only [LinearMap.comp_apply] at ha
    change augD (φ (x 0)) = 1
    rw [ha, source_aug]
  exact one_ne_zero (target_aug_one.symm.trans target_aug_zero)

end Obstruction

/-! ## Packaged interface used by the rook construction -/

/-- All data of the forbidden finite Smith tower produced in Sections 4--5 of
the paper.  The types are ambient direct sums of the graded chain groups.

This structure is an interface, not an assumption: the next theorem proves it
is empty.  A completed polyhedral development would show that a rook labeling
constructs an inhabitant of this structure. -/
structure ForbiddenChainMap (d : ℕ) where
  C : Type
  D : Type
  addC : AddCommGroup C
  moduleC : Module F₂ C
  addD : AddCommGroup D
  moduleD : Module F₂ D
  boundaryC : C →ₗ[F₂] C
  normC : C →ₗ[F₂] C
  augC : C →ₗ[F₂] F₂
  boundaryD : D →ₗ[F₂] D
  normD : D →ₗ[F₂] D
  augD : D →ₗ[F₂] F₂
  map : C →ₗ[F₂] D
  map_boundary : boundaryD.comp map = map.comp boundaryC
  map_norm : normD.comp map = map.comp normC
  map_aug : augD.comp map = augC
  boundaryD_sq : boundaryD.comp boundaryD = 0
  boundaryD_norm : boundaryD.comp normD = normD.comp boundaryD
  augD_boundary : augD.comp boundaryD = 0
  augD_norm : augD.comp normD = 0
  normD_exact : ∀ y : D, normD y = 0 → ∃ z : D, normD z = y
  sourceTower : ℕ → C
  source_tower : ∀ i ≤ d, boundaryC (sourceTower (i + 1)) = normC (sourceTower i)
  source_aug : augC (sourceTower 0) = 1
  target_bounded : map (sourceTower (d + 1)) = 0

/-- The packaged forbidden chain map is genuinely impossible, with no
topological or geometric assumptions. -/
theorem forbiddenChainMap_isEmpty (d : ℕ) : IsEmpty (ForbiddenChainMap d) := by
  constructor
  intro F
  letI : AddCommGroup F.C := F.addC
  letI : Module F₂ F.C := F.moduleC
  letI : AddCommGroup F.D := F.addD
  letI : Module F₂ F.D := F.moduleD
  exact chain_level_borsuk_ulam F.boundaryC F.normC F.augC
    F.boundaryD F.normD F.augD F.map F.map_boundary F.map_norm F.map_aug
    F.boundaryD_sq F.boundaryD_norm F.augD_boundary F.augD_norm F.normD_exact
    d F.sourceTower F.source_tower F.source_aug F.target_bounded

end

end Norine