Lumenary.VectorBundlesCharacteristicClasses

Formal library

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

  /-- **Every section of the Möbius bundle vanishes somewhere.** The Möbius line bundle over
  `S¹ = ℝ/ℤ` is the quotient of `ℝ × ℝ` by `(t, v) ~ (t + 1, -v)`, so its continuous sections are
  the continuous functions with `s(t + 1) = -s(t)`. Then `s(0)` and `s(1) = -s(0)` have opposite
  signs (or vanish), and the intermediate value theorem gives a zero in `[0, 1]`. -/
  theorem mobius_section_vanishes (s : ℝ → ℝ) (hs : Continuous s) (anti : ∀ t, s (t + 1) = -s t) :
      ∃ t ∈ Set.Icc (0 : ℝ) 1, s t = 0 := by
    have h1 : s 1 = -s 0 := by simpa using anti 0
    rcases le_total (s 0) 0 with h0 | h0
    · -- `s 0 ≤ 0 ≤ s 1`
      exact intermediate_value_Icc zero_le_one hs.continuousOn ⟨h0, by linarith⟩
    · -- `s 1 ≤ 0 ≤ s 0`
      exact intermediate_value_Icc' zero_le_one hs.continuousOn ⟨by linarith, h0⟩

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

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

  /-- **The Möbius bundle is not trivial.** A trivial line bundle `S¹ × ℝ` has the nowhere-zero
  section `t ↦ 1`; the Möbius bundle has no nowhere-zero section at all. (Contrast: the constant
  function `1` is periodic, `s(t + 1) = s(t)`, i.e. a section of the trivial bundle.) -/
  theorem mobius_not_trivial :
      ¬ ∃ s : ℝ → ℝ, Continuous s ∧ (∀ t, s (t + 1) = -s t) ∧ ∀ t, s t ≠ 0 := by
    rintro ⟨s, hs, anti, hne⟩
    obtain ⟨t, -, ht⟩ := mobius_section_vanishes s hs anti
    exact hne t ht

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

• reInnerdefDefinitionpropext, Classical.choice, Quot.sound

  /-- The real (Euclidean) inner product on `ℂⁿ = ℝ²ⁿ`: `⟨z, w⟩ = Σₖ Re(z̄ₖ wₖ)`. -/
  def reInner {n : ℕ} (z w : Fin n → ℂ) : ℝ :=
    ∑ k, (conj (z k) * w k).re

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

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

  /-- **Odd-dimensional spheres can be combed.** On `S²ⁿ⁻¹ ⊂ ℂⁿ` the field `v(z) = i z` is tangent
  (`⟨z, i z⟩ = 0`) and has the same length as `z`, so it never vanishes on the sphere. In real
  coordinates it is `(x₁, y₁, …) ↦ (-y₁, x₁, …)`. -/
  theorem odd_sphere_vector_field {n : ℕ} (z : Fin n → ℂ) :
      reInner z (fun k => Complex.I * z k) = 0 ∧
        reInner (fun k => Complex.I * z k) (fun k => Complex.I * z k) = reInner z z := by
    constructor
    · -- each term `Re(z̄ · i z) = Re(i |z|²)` is zero
      apply Finset.sum_eq_zero
      intro k _
      simp only [Complex.mul_re, Complex.conj_re, Complex.conj_im, Complex.mul_im, Complex.I_re,
        Complex.I_im]
      ring
    · -- `|i z| = |z|` term by term
      apply Finset.sum_congr rfl
      intro k _
      simp only [map_mul, Complex.conj_I, Complex.mul_re, Complex.conj_re, Complex.conj_im,
        Complex.mul_im, Complex.I_re, Complex.I_im, Complex.neg_re, Complex.neg_im]
      ring

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

• dot4defDefinitionpropext, Classical.choice, Quot.sound

  /-- The dot product on `ℝ⁴`. -/
  def dot4 (x y : Fin 4 → ℝ) : ℝ := ∑ i, x i * y i

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

• frameIdefDefinitionpropext, Classical.choice, Quot.sound

  /-- Three vector fields on `ℝ⁴`: left multiplication of `x = x₀ + x₁ i + x₂ j + x₃ k` by the
  quaternion units `i`, `j`, `k`. -/
  def frameI (x : Fin 4 → ℝ) : Fin 4 → ℝ := ![-x 1, x 0, -x 3, x 2]

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

• frameJdefDefinitionpropext, Classical.choice, Quot.sound

  /-- Left multiplication by `j`. -/
  def frameJ (x : Fin 4 → ℝ) : Fin 4 → ℝ := ![-x 2, x 3, x 0, -x 1]

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

• frameKdefDefinitionpropext, Classical.choice, Quot.sound

  /-- Left multiplication by `k`. -/
  def frameK (x : Fin 4 → ℝ) : Fin 4 → ℝ := ![-x 3, -x 2, x 1, x 0]

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

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

  /-- **`S³` is parallelisable.** At every point `x` the vectors `i x`, `j x`, `k x` are tangent to
  the sphere through `x` (orthogonal to `x`), pairwise orthogonal, and as long as `x`; on the unit
  sphere they form an orthonormal basis of the tangent space, so `TS³ ≅ S³ × ℝ³`. -/
  theorem s3_parallelizable (x : Fin 4 → ℝ) :
      dot4 x (frameI x) = 0 ∧ dot4 x (frameJ x) = 0 ∧ dot4 x (frameK x) = 0 ∧
      dot4 (frameI x) (frameJ x) = 0 ∧ dot4 (frameI x) (frameK x) = 0 ∧
      dot4 (frameJ x) (frameK x) = 0 ∧
      dot4 (frameI x) (frameI x) = dot4 x x ∧ dot4 (frameJ x) (frameJ x) = dot4 x x ∧
      dot4 (frameK x) (frameK x) = dot4 x x := by
    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>
      simp [dot4, frameI, frameJ, frameK, Fin.sum_univ_four] <;> ring

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

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

  /-- In characteristic two, `(1 + a)^(2^k) = 1 + a^(2^k)`. Since `w(TℝPⁿ) = (1 + a)ⁿ⁺¹` with
  `aⁿ⁺¹ = 0`, this shows `w(TℝPⁿ) = 1` when `n + 1 = 2^k` (e.g. `ℝP³`, `ℝP⁷`). This applies
  Mathlib's `add_pow_char_pow`. -/
  theorem frobenius_two (k : ℕ) : ((1 + X) ^ (2 ^ k) : (ZMod 2)[X]) = 1 + X ^ (2 ^ k) := by
    simpa using add_pow_char_pow (1 : (ZMod 2)[X]) X (p := 2) (n := k)

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

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

  /-- The total Stiefel–Whitney class of `ℝP²` is `(1 + a)³ = 1 + a + a² + a³ = 1 + a + a²` in
  `H*(ℝP²; ℤ/2) = ℤ/2[a]/(a³)`. As a polynomial identity mod 2: squaring is additive, so
  `(1 + a)³ = (1 + a²)(1 + a)`. Since `w₁ = a ≠ 0`, `ℝP²` is non-orientable, and since `w₂ = a² ≠ 0`
  its tangent bundle is not trivial. -/
  theorem sw_rp2 : ((1 + X) ^ 3 : (ZMod 2)[X]) = 1 + X + X ^ 2 + X ^ 3 := by
    have hsq : ((1 + X) ^ 2 : (ZMod 2)[X]) = 1 + X ^ 2 := by
      simpa using add_pow_char (1 : (ZMod 2)[X]) X (p := 2)
    rw [pow_succ, hsq]
    ring

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

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

  /-- The product `B × ℝᵏ`, as Mathlib's `Bundle.Trivial B F`, is a vector bundle. This applies
  the instance `Bundle.Trivial.vectorBundle`. -/
  theorem trivial_bundle (B F : Type*) [TopologicalSpace B] [NormedAddCommGroup F]
      [NormedSpace ℝ F] : VectorBundle ℝ F (Bundle.Trivial B F) :=
    inferInstance

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

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

  /-- **Pullbacks.** If `E → B` is a vector bundle and `f : B' → B` is continuous, then `f*E → B'`
  (fibre `E_{f(b')}` over `b'`) is a vector bundle. This applies Mathlib's instance
  `VectorBundle.pullback`. Characteristic classes are, by definition, natural under pullback. -/
  theorem pullback_bundle {B B' F : Type*} [TopologicalSpace B] [TopologicalSpace B']
      [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type*} [∀ x, AddCommMonoid (E x)]
      [∀ x, Module ℝ (E x)] [TopologicalSpace (TotalSpace F E)] [∀ x, TopologicalSpace (E x)]
      [FiberBundle F E] [VectorBundle ℝ F E] (f : C(B', B)) :
      VectorBundle ℝ F ((f : B' → B) *ᵖ E) :=
    inferInstance

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

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

  /-- **Whitney sum.** The fibrewise direct sum `E₁ ⊕ E₂` of two vector bundles over the same base
  (Mathlib's `E₁ ×ᵇ E₂`) is a vector bundle. This applies Mathlib's instance `VectorBundle.prod`. -/
  theorem whitney_sum {B F₁ F₂ : Type*} [TopologicalSpace B]
      [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂]
      {E₁ E₂ : B → Type*} [∀ x, AddCommMonoid (E₁ x)] [∀ x, Module ℝ (E₁ x)]
      [∀ x, AddCommMonoid (E₂ x)] [∀ x, Module ℝ (E₂ x)]
      [TopologicalSpace (TotalSpace F₁ E₁)] [TopologicalSpace (TotalSpace F₂ E₂)]
      [∀ x, TopologicalSpace (E₁ x)] [∀ x, TopologicalSpace (E₂ x)]
      [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle ℝ F₁ E₁] [VectorBundle ℝ F₂ E₂] :
      VectorBundle ℝ (F₁ × F₂) (E₁ ×ᵇ E₂) :=
    inferInstance

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

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

  /-- **The tangent bundle** of a (once differentiable) manifold `M` modelled on a normed space `E`
  is a vector bundle with fibre `E`. This applies Mathlib's instance `TangentSpace.vectorBundle`,
  built from the derivatives of the chart transition maps — a cocycle of transition functions. -/
  theorem tangent_bundle {E H M : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
      [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [TopologicalSpace M] [ChartedSpace H M]
      [IsManifold I 1 M] : VectorBundle ℝ E (TangentSpace I : M → Type _) :=
    inferInstance

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/VectorBundlesCharacteristicClasses.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.

/-- Deduce that the Möbius bundle has no nowhere-zero section.
Hint: use `Lumenary.VectorBundlesCharacteristicClasses.mobius_section_vanishes` to find a zero
of `s`, contradicting `∀ t, s t ≠ 0`. -/
theorem mobius_not_trivial :
    ¬ ∃ s : ℝ → ℝ, Continuous s ∧ (∀ t, s (t + 1) = -s t) ∧ ∀ t, s t ≠ 0 := by
  sorry

/-- **The Möbius bundle is not trivial.** A trivial line bundle `S¹ × ℝ` has the nowhere-zero
section `t ↦ 1`; the Möbius bundle has no nowhere-zero section at all. (Contrast: the constant
function `1` is periodic, `s(t + 1) = s(t)`, i.e. a section of the trivial bundle.) -/
theorem mobius_not_trivial :
    ¬ ∃ s : ℝ → ℝ, Continuous s ∧ (∀ t, s (t + 1) = -s t) ∧ ∀ t, s t ≠ 0 := by
  rintro ⟨s, hs, anti, hne⟩
  obtain ⟨t, -, ht⟩ := mobius_section_vanishes s hs anti
  exact hne t ht

/-- Prove that every continuous antiperiodic function `s(t + 1) = -s(t)` has a zero in `[0, 1]`.
Hint: compare the signs of `s 0` and `s 1 = -s 0` with `le_total (s 0) 0`, then apply
`intermediate_value_Icc` or `intermediate_value_Icc'` on `[0, 1]`. -/
theorem mobius_section_vanishes (s : ℝ → ℝ) (hs : Continuous s) (anti : ∀ t, s (t + 1) = -s t) :
    ∃ t ∈ Set.Icc (0 : ℝ) 1, s t = 0 := by
  sorry

/-- **Every section of the Möbius bundle vanishes somewhere.** The Möbius line bundle over
`S¹ = ℝ/ℤ` is the quotient of `ℝ × ℝ` by `(t, v) ~ (t + 1, -v)`, so its continuous sections are
the continuous functions with `s(t + 1) = -s(t)`. Then `s(0)` and `s(1) = -s(0)` have opposite
signs (or vanish), and the intermediate value theorem gives a zero in `[0, 1]`. -/
theorem mobius_section_vanishes (s : ℝ → ℝ) (hs : Continuous s) (anti : ∀ t, s (t + 1) = -s t) :
    ∃ t ∈ Set.Icc (0 : ℝ) 1, s t = 0 := by
  have h1 : s 1 = -s 0 := by simpa using anti 0
  rcases le_total (s 0) 0 with h0 | h0
  · -- `s 0 ≤ 0 ≤ s 1`
    exact intermediate_value_Icc zero_le_one hs.continuousOn ⟨h0, by linarith⟩
  · -- `s 1 ≤ 0 ≤ s 0`
    exact intermediate_value_Icc' zero_le_one hs.continuousOn ⟨by linarith, h0⟩