noncomputable def ofLp_linear : R3 →ₗ[ℝ] R3_raw

The goal of this module is just to prove lemma fixed_lemma (g : SO3) : g≠1 → ({x ∈ S2 | g • x = x} = ∅ ∨ Nat.card ({x ∈ S2 | g • x = x}) = 2)

Equations

• ofLp_linear = ↑(WithLp.linearEquiv 2 ℝ R3_raw)

noncomputable def to_R3_linear : R3_raw →ₗ[ℝ] R3

Equations

• to_R3_linear = ↑(WithLp.linearEquiv 2 ℝ R3_raw).symm

noncomputable def g_end_raw (g : ↥SO3) : Module.End ℝ R3_raw

Equations

• g_end_raw g = Matrix.toLin' ↑g

noncomputable def g_end (g : ↥SO3) : Module.End ℝ R3

Equations

• g_end g = to_R3_linear ∘ₗ g_end_raw g ∘ₗ ofLp_linear

def kermap_raw (g : ↥SO3) : R3_raw →ₗ[ℝ] R3_raw

Equations

• kermap_raw g = Matrix.toLin' (↑g - 1)

noncomputable def kermap (g : ↥SO3) : R3 →ₗ[ℝ] R3

Equations

• kermap g = to_R3_linear ∘ₗ kermap_raw g ∘ₗ ofLp_linear

noncomputable def K (g : ↥SO3) : Submodule ℝ R3

Equations

• K g = (kermap g).ker

theorem same_char_0 (g : ↥SO3) : LinearMap.charpoly (g_end g) = (↑g).charpoly

theorem mapMatrix_is_map (g : ↥SO3) : ((algebraMap ℝ ℂ).mapMatrix ↑g).charpoly = ((↑g).map ⇑(algebraMap ℝ ℂ)).charpoly

noncomputable def as_complex (M : MAT) : Matrix (Fin 3) (Fin 3) ℂ

Equations

• as_complex M = (algebraMap ℝ ℂ).mapMatrix M

noncomputable def cpoly (g : ↥SO3) : Polynomial ℂ

Equations

• cpoly g = (as_complex ↑g).charpoly

theorem same_char (g : ↥SO3) : Polynomial.map (algebraMap ℝ ℂ) (LinearMap.charpoly (g_end g)) = cpoly g

theorem cpoly_coef_real (g : ↥SO3) (i : ℕ) : ∃ (x : ℝ), ↑x = (cpoly g).coeff i

theorem det_as_prod (g : ↥SO3) : (cpoly g).roots.prod = 1

theorem charpoly_deg_3 (g : ↥SO3) : (cpoly g).degree = 3

theorem charpoly_natdeg_3 (g : ↥SO3) : (cpoly g).natDegree = 3

theorem num_roots_eq_deg (g : ↥SO3) : (cpoly g).roots.card = (cpoly g).natDegree

theorem num_roots_eq_3 (g : ↥SO3) : (cpoly g).roots.card = 3

@[reducible, inline]

abbrev C3 : Type

Equations

• C3 = Matrix (Fin 3) (Fin 3) ℂ

theorem eig_norms (g : ↥SO3) (z : ℂ) : z ∈ (cpoly g).roots → ‖z‖ = 1

def CONJ : ℂ →+* ℂ

Equations

• CONJ = starRingEnd ℂ

theorem flem {z : ℂ} (g : ↥SO3) : z ∈ (cpoly g).roots → z = CONJ z → z = 1 ∨ z = -1

theorem flem2 {z : ℂ} (g : ↥SO3) : z ∈ (cpoly g).roots → z ≠ 1 ∧ z ≠ -1 → z ≠ CONJ z

theorem conj_roots (g : ↥SO3) : (cpoly g).roots = Multiset.map (⇑CONJ) (cpoly g).roots

theorem conj_roots_2 (g : ↥SO3) (z : ℂ) : z ∈ (cpoly g).roots → CONJ z ∈ (cpoly g).roots

theorem conj_roots_3 (g : ↥SO3) (z : ℂ) : Multiset.count z (cpoly g).roots = Multiset.count (CONJ z) (cpoly g).roots

theorem conj_roots_4 {z : ℂ} (g : ↥SO3) : z ∈ (cpoly g).roots → z ≠ 1 ∧ z ≠ -1 → Multiset.count z (cpoly g).roots = 1

theorem conj_mul_roots {z : ℂ} (g : ↥SO3) : z ∈ (cpoly g).roots → z * CONJ z = 1

theorem cast_root_mult1 (g : ↥SO3) : Polynomial.rootMultiplicity 1 (↑g).charpoly = Polynomial.rootMultiplicity 1 (Polynomial.map (algebraMap ℝ ℂ) (↑g).charpoly)

theorem same_mult (g : ↥SO3) : Polynomial.rootMultiplicity 1 (LinearMap.charpoly (g_end g)) = Polynomial.rootMultiplicity 1 (Polynomial.map (algebraMap ℝ ℂ) (LinearMap.charpoly (g_end g)))

theorem idlem (g : ↥SO3) : Multiset.count 1 (cpoly g).roots = 3 → g = 1

theorem tight_space_lemma (g : ↥SO3) : Multiset.count 1 (cpoly g).roots + Multiset.count (-1) (cpoly g).roots ≥ 2 → ∀ w ∈ (cpoly g).roots, w = 1 ∨ w = -1

theorem tight_space_lemma_2 (g : ↥SO3) : Multiset.count 1 (cpoly g).roots + Multiset.count (-1) (cpoly g).roots ≥ 2 → Multiset.count 1 (cpoly g).roots + Multiset.count (-1) (cpoly g).roots = 3

theorem spec_lem (g : ↥SO3) : g ≠ 1 → Multiset.count 1 (cpoly g).roots = 1

theorem K_id (g : ↥SO3) : K g = (g_end g).eigenspace 1

theorem dim_ker (g : ↥SO3) : g ≠ 1 → Module.finrank ℝ ↥(K g) ≤ 1

theorem fixed_lemma (g : ↥SO3) : g ≠ 1 → {x : R3 | x ∈ S2 ∧ g • x = x} = ∅ ∨ Nat.card ↑{x : R3 | x ∈ S2 ∧ g • x = x} = 2