Lumenary.LowDimensionalTopology

Formal library

• three_sphere_isManifoldtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- The unit sphere `S³ = {x ∈ ℝ⁴ : ‖x‖ = 1}` is an analytic (in particular smooth) manifold of
  dimension 3, with charts given by stereographic projection. This is Mathlib's instance
  `EuclideanSpace.instIsManifoldSphere`. By Perelman's theorem it is the only closed, simply
  connected 3-manifold up to homeomorphism (and, in dimension 3, up to diffeomorphism). -/
  theorem three_sphere_isManifold :
      IsManifold (𝓡 3) ω (sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :=
    inferInstance

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• LensHomeoReldefDefinitionpropext, Quot.sound

  /-- The **Reidemeister–Brody relation** on residues coprime to `p`: `q' ≡ ±q` or `qq' ≡ ±1`
  (mod `p`), i.e. `q' ∈ {q, −q, q⁻¹, −q⁻¹}`. By the classification of lens spaces (Reidemeister
  1935 for the combinatorial version, Brody 1960 for homeomorphism), `L(p, q)` and `L(p, q')` are
  homeomorphic exactly when this relation holds. -/
  def LensHomeoRel (q q' : (ZMod p)ˣ) : Prop :=
    q' = q ∨ q' = -q ∨ q' = q⁻¹ ∨ q' = -q⁻¹

  Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• LensHomotopyReldefDefinitionpropext, Quot.sound

  /-- The **Whitehead relation**: `qq' ≡ ±n²` (mod `p`) for some unit `n`. By J. H. C. Whitehead
  (1941), `L(p, q)` and `L(p, q')` are homotopy equivalent exactly when this relation holds. -/
  def LensHomotopyRel (q q' : (ZMod p)ˣ) : Prop :=
    ∃ n : (ZMod p)ˣ, q * q' = n ^ 2 ∨ q * q' = -(n ^ 2)

  Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• lensHomeoRel_equivalencetheoremProved here from basic factspropext, Quot.sound

  /-- The Reidemeister–Brody relation is an equivalence relation. The set `{q, −q, q⁻¹, −q⁻¹}` is the
  orbit of `q` under the Klein four-group generated by negation and inversion (which commute), so
  each case of transitivity is an identity such as `(−q)⁻¹ = −q⁻¹` or `(q⁻¹)⁻¹ = q`. -/
  theorem lensHomeoRel_equivalence : Equivalence (LensHomeoRel (p := p)) where
    refl q := Or.inl rfl
    symm := by
      intro q q' h
      rcases h with rfl | rfl | rfl | rfl
      · exact Or.inl rfl
      · exact Or.inr (Or.inl (neg_neg q).symm)
      · exact Or.inr (Or.inr (Or.inl (inv_inv q).symm))
      · refine Or.inr (Or.inr (Or.inr ?_))
        rw [inv_neg, neg_neg, inv_inv]
    trans := by
      intro q q' q'' h₁ h₂
      unfold LensHomeoRel at *
      rcases h₁ with rfl | rfl | rfl | rfl <;> rcases h₂ with rfl | rfl | rfl | rfl <;>
        simp [inv_neg]

  Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• lensHomotopyRel_of_lensHomeoReltheoremProved here from basic factspropext, Quot.sound

  /-- Homeomorphic lens spaces are homotopy equivalent, at the level of the criteria: if
  `q' ∈ {±q, ±q⁻¹}` then `qq'` is `±q²` or `±1 = ±1²`, a square up to sign. -/
  theorem lensHomotopyRel_of_lensHomeoRel {q q' : (ZMod p)ˣ} (h : LensHomeoRel q q') :
      LensHomotopyRel q q' := by
    rcases h with h | h | h | h <;> rw [h]
    · exact ⟨q, Or.inl (sq q).symm⟩
    · exact ⟨q, Or.inr (by rw [mul_neg, sq])⟩
    · exact ⟨1, Or.inl (by simp)⟩
    · exact ⟨1, Or.inr (by simp)⟩

  Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• lens_seventheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **`L(7, 1)` and `L(7, 2)`**: the Whitehead relation holds (`1 · 2 ≡ 3²` mod 7) but the
  Reidemeister–Brody relation fails (`2 ∉ {±1}` mod 7). With the classification theorems, these two
  lens spaces are homotopy equivalent but not homeomorphic. Checked by `decide` over the six
  units of `ZMod 7`. -/
  theorem lens_seven :
      LensHomotopyRel (p := 7) 1 (ZMod.unitOfCoprime 2 (by norm_num)) ∧
        ¬ LensHomeoRel (p := 7) 1 (ZMod.unitOfCoprime 2 (by norm_num)) := by
    unfold LensHomotopyRel LensHomeoRel
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• lens_fivetheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **`L(5, 1)` and `L(5, 2)`**: the Whitehead relation fails, since `1 · 2 = 2` is not `±n²`
  modulo 5 (the squares of units are `1` and `4 = −1`). With Whitehead's theorem: two closed
  3-manifolds with the same fundamental group `ℤ/5` and the same homology groups that are not even
  homotopy equivalent. -/
  theorem lens_five :
      ¬ LensHomotopyRel (p := 5) 1 (ZMod.unitOfCoprime 2 (by norm_num)) := by
    unfold LensHomotopyRel
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• lens_five_fourtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **`L(5, 1)` and `L(5, 4)`** satisfy the Reidemeister–Brody relation, because `4 ≡ −1`
  (mod 5); indeed `L(p, q)` and `L(p, −q)` are always homeomorphic, by a homeomorphism that
  reverses orientation. -/
  theorem lens_five_four : LensHomeoRel (p := 5) 1 (ZMod.unitOfCoprime 4 (by norm_num)) := by
    unfold LensHomeoRel
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• even_form_of_even_diagtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Even forms.** If `A` is a symmetric integer matrix whose diagonal entries are even, then
  `xᵀAx` is even for every integer vector `x`. Proof: write `A = D + U + Uᵀ` with `D` diagonal and
  `U` strictly upper triangular; then `xᵀAx = xᵀDx + 2·xᵀUx`, and `xᵀDx = Σ Aᵢᵢ xᵢ²` is even. For
  the intersection form of a closed simply connected 4-manifold, "even" is equivalent to the
  second Stiefel–Whitney class vanishing (the manifold is spin). -/
  theorem even_form_of_even_diag {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (hA : A.IsSymm)
      (hdiag : ∀ i, Even (A i i)) (x : Fin n → ℤ) : Even (x ⬝ᵥ (A *ᵥ x)) := by
    classical
    let U : Matrix (Fin n) (Fin n) ℤ := Matrix.of fun i j => if i < j then A i j else 0
    let D : Matrix (Fin n) (Fin n) ℤ := Matrix.diagonal fun i => A i i
    have hsplit : A = D + U + Uᵀ := by
      ext i j
      simp only [D, U, Matrix.add_apply, Matrix.diagonal_apply, Matrix.transpose_apply,
        Matrix.of_apply]
      rcases lt_trichotomy i j with h | rfl | h
      · simp [h, h.ne, not_lt.mpr h.le]
      · simp
      · simp [h, h.ne', not_lt.mpr h.le]
        exact hA.apply j i
    have hU : x ⬝ᵥ (Uᵀ *ᵥ x) = x ⬝ᵥ (U *ᵥ x) := by
      rw [dotProduct_mulVec, vecMul_transpose, dotProduct_comm]
    have hD : Even (x ⬝ᵥ (D *ᵥ x)) := by
      simp only [D, mulVec_diagonal, dotProduct]
      refine Finset.even_sum _ fun i _ => ?_
      obtain ⟨k, hk⟩ := hdiag i
      exact ⟨x i * k * x i, by rw [hk]; ring⟩
    rw [hsplit, add_mulVec, add_mulVec, dotProduct_add, dotProduct_add, hU, add_assoc]
    exact hD.add ⟨x ⬝ᵥ (U *ᵥ x), rfl⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• e8_eventheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- The **E₈ form** — the Cartan matrix of the exceptional Lie algebra `e₈`, Mathlib's
  `CartanMatrix.E 8` — is even: `xᵀE₈x ∈ 2ℤ` for all `x ∈ ℤ⁸`. It is symmetric with `2`s on the
  diagonal (`CartanMatrix.E_isSymm`, `CartanMatrix.E_diag`), so `even_form_of_even_diag` applies.
  Freedman showed that there is a closed simply connected *topological* 4-manifold with
  intersection form E₈; Rokhlin's theorem shows it has no smooth structure. -/
  theorem e8_even (x : Fin 8 → ℤ) : Even (x ⬝ᵥ (CartanMatrix.E 8 *ᵥ x)) :=
    even_form_of_even_diag _ (CartanMatrix.E_isSymm 8)
      (fun i => ⟨1, by rw [CartanMatrix.E_diag]; rfl⟩) x

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• e8_unimodulartheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- The E₈ form is **unimodular**: its determinant is `1`, so it is the intersection form of a
  closed 4-manifold that could exist by Poincaré duality. This is Mathlib's
  `CartanMatrix.E₈_det`, proved by a determinant-evaluation tactic. -/
  theorem e8_unimodular : (CartanMatrix.E 8).det = 1 :=
    CartanMatrix.E₈_det

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

• e8_posDeftheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- The E₈ form is **positive definite**: `xᵀE₈x > 0` for every non-zero `x ∈ ℤ⁸`. Proof by
  completing squares (the `LDLᵀ` decomposition, cleared of denominators):
  `60·xᵀE₈x = 30(2x₀ − x₂)² + 30(2x₁ − x₃)² + 10(3x₂ − 2x₃)² + 2(5x₃ − 6x₄)² + 3(4x₄ − 5x₅)²
  + 5(3x₅ − 4x₆)² + 10(2x₆ − 3x₇)² + 30x₇²`. If the form vanished, every square would vanish,
  and back-substitution from `x₇ = 0` gives `x = 0`. Together with `e8_even` and
  `e8_unimodular`: E₈ is an even, unimodular, positive definite form of rank 8 — so its
  signature is 8, which is not divisible by 16. -/
  theorem e8_posDef (x : Fin 8 → ℤ) (hx : x ≠ 0) : 0 < x ⬝ᵥ (CartanMatrix.E 8 *ᵥ x) := by
    have hQ : x ⬝ᵥ (CartanMatrix.E 8 *ᵥ x) =
        2 * x 0 ^ 2 - 2 * x 0 * x 2 + 2 * x 1 ^ 2 - 2 * x 1 * x 3 + 2 * x 2 ^ 2 - 2 * x 2 * x 3
          + 2 * x 3 ^ 2 - 2 * x 3 * x 4 + 2 * x 4 ^ 2 - 2 * x 4 * x 5 + 2 * x 5 ^ 2
          - 2 * x 5 * x 6 + 2 * x 6 ^ 2 - 2 * x 6 * x 7 + 2 * x 7 ^ 2 := by
      rw [CartanMatrix.E_eight_eq]
      simp [Matrix.mulVec, dotProduct, Fin.sum_univ_eight]
      ring
    rw [hQ]
    by_contra hle
    push Not at hle
    have s0 := sq_nonneg (2 * x 0 - x 2)
    have s1 := sq_nonneg (2 * x 1 - x 3)
    have s2 := sq_nonneg (3 * x 2 - 2 * x 3)
    have s3 := sq_nonneg (5 * x 3 - 6 * x 4)
    have s4 := sq_nonneg (4 * x 4 - 5 * x 5)
    have s5 := sq_nonneg (3 * x 5 - 4 * x 6)
    have s6 := sq_nonneg (2 * x 6 - 3 * x 7)
    have s7 := sq_nonneg (x 7)
    have z7 : x 7 = 0 := pow_eq_zero_iff two_ne_zero |>.mp (by linarith)
    have z6 : x 6 = 0 := by
      have : (2 * x 6 - 3 * x 7) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    have z5 : x 5 = 0 := by
      have : (3 * x 5 - 4 * x 6) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    have z4 : x 4 = 0 := by
      have : (4 * x 4 - 5 * x 5) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    have z3 : x 3 = 0 := by
      have : (5 * x 3 - 6 * x 4) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    have z2 : x 2 = 0 := by
      have : (3 * x 2 - 2 * x 3) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    have z1 : x 1 = 0 := by
      have : (2 * x 1 - x 3) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    have z0 : x 0 = 0 := by
      have : (2 * x 0 - x 2) ^ 2 = 0 := by linarith
      have := pow_eq_zero_iff two_ne_zero |>.mp this
      omega
    apply hx
    ext i
    fin_cases i <;> assumption

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Show that the residues `1` and `4` modulo 5 satisfy the Reidemeister–Brody relation, so
`L(5, 1)` and `L(5, 4)` are homeomorphic.
Hint: unfold `LensHomeoRel`; the statement is about the four units of `ZMod 5`, so `decide`
can check it. Which of the four cases holds? -/
theorem lens_five_four : LensHomeoRel (p := 5) 1 (ZMod.unitOfCoprime 4 (by norm_num)) := by
  sorry

/-- **`L(5, 1)` and `L(5, 4)`** satisfy the Reidemeister–Brody relation, because `4 ≡ −1`
(mod 5); indeed `L(p, q)` and `L(p, −q)` are always homeomorphic, by a homeomorphism that
reverses orientation. -/
theorem lens_five_four : LensHomeoRel (p := 5) 1 (ZMod.unitOfCoprime 4 (by norm_num)) := by
  unfold LensHomeoRel
  decide

/-- Show that the homeomorphism criterion implies the homotopy criterion.
Hint: split into the four cases `q' = q`, `q' = -q`, `q' = q⁻¹`, `q' = -q⁻¹` and rewrite. The
witness `n` is `q` in the first two cases and `1` in the last two. -/
theorem lensHomotopyRel_of_lensHomeoRel {p : ℕ} {q q' : (ZMod p)ˣ} (h : LensHomeoRel q q') :
    LensHomotopyRel q q' := by
  sorry

/-- Homeomorphic lens spaces are homotopy equivalent, at the level of the criteria: if
`q' ∈ {±q, ±q⁻¹}` then `qq'` is `±q²` or `±1 = ±1²`, a square up to sign. -/
theorem lensHomotopyRel_of_lensHomeoRel {q q' : (ZMod p)ˣ} (h : LensHomeoRel q q') :
    LensHomotopyRel q q' := by
  rcases h with h | h | h | h <;> rw [h]
  · exact ⟨q, Or.inl (sq q).symm⟩
  · exact ⟨q, Or.inr (by rw [mul_neg, sq])⟩
  · exact ⟨1, Or.inl (by simp)⟩
  · exact ⟨1, Or.inr (by simp)⟩