feat(analysis/quaternion): add complete_space, module.free, and module.finite instances (#18347)

The main trick here is showing that the quaternions are in isometric equivalence with 4D euclidean space.

Author: eric-wieser

src/algebra/quaternion.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import algebra.algebra.equiv
+import linear_algebra.finrank
+import linear_algebra.free_module.basic
+import linear_algebra.free_module.finite.basic
 import set_theory.cardinal.ordinal
 import tactic.ring_exp
 
@@ -65,6 +68,17 @@ def equiv_prod {R : Type*} (c₁ c₂ : R) : ℍ[R, c₁, c₂] ≃ R × R × R
   left_inv := λ ⟨a₁, a₂, a₃, a₄⟩, rfl,
   right_inv := λ ⟨a₁, a₂, a₃, a₄⟩, rfl }
 
+/-- The equivalence between a quaternion algebra over `R` and `fin 4 → R`. -/
+@[simps symm_apply]
+def equiv_tuple {R : Type*} (c₁ c₂ : R) : ℍ[R, c₁, c₂] ≃ (fin 4 → R) :=
+{ to_fun := λ a, ![a.1, a.2, a.3, a.4],
+  inv_fun := λ a, ⟨a 0, a 1, a 2, a 3⟩,
+  left_inv := λ ⟨a₁, a₂, a₃, a₄⟩, rfl,
+  right_inv := λ f, by ext ⟨_, _|_|_|_|_|⟨⟩⟩; refl }
+
+@[simp] lemma equiv_tuple_apply {R : Type*} (c₁ c₂ : R) (x : ℍ[R, c₁, c₂]) :
+  equiv_tuple c₁ c₂ x = ![x.re, x.im_i, x.im_j, x.im_k] := rfl
+
 @[simp] lemma mk.eta {R : Type*} {c₁ c₂} : ∀ a : ℍ[R, c₁, c₂], mk a.1 a.2 a.3 a.4 = a
 | ⟨a₁, a₂, a₃, a₄⟩ := rfl
 
@@ -191,7 +205,7 @@ instance : algebra R ℍ[R, c₁, c₂] :=
 lemma algebra_map_eq (r : R) : algebra_map R ℍ[R,c₁,c₂] r = ⟨r, 0, 0, 0⟩ := rfl
 
 section
-variables (R c₁ c₂)
+variables (c₁ c₂)
 
 /-- `quaternion_algebra.re` as a `linear_map`-/
 @[simps] def re_lm : ℍ[R, c₁, c₂] →ₗ[R] R :=
@@ -209,6 +223,37 @@ variables (R c₁ c₂)
 @[simps] def im_k_lm : ℍ[R, c₁, c₂] →ₗ[R] R :=
 { to_fun := im_k, map_add' := λ x y, rfl, map_smul' := λ r x, rfl }
 
+/-- `quaternion_algebra.equiv_tuple` as a linear equivalence. -/
+def linear_equiv_tuple : ℍ[R,c₁,c₂] ≃ₗ[R] (fin 4 → R) :=
+linear_equiv.symm  -- proofs are not `rfl` in the forward direction
+  { to_fun := (equiv_tuple c₁ c₂).symm,
+    inv_fun := equiv_tuple c₁ c₂,
+    map_add' := λ v₁ v₂, rfl,
+    map_smul' := λ v₁ v₂, rfl,
+    .. (equiv_tuple c₁ c₂).symm }
+
+@[simp] lemma coe_linear_equiv_tuple : ⇑(linear_equiv_tuple c₁ c₂) = equiv_tuple c₁ c₂ := rfl
+@[simp] lemma coe_linear_equiv_tuple_symm :
+  ⇑(linear_equiv_tuple c₁ c₂).symm = (equiv_tuple c₁ c₂).symm := rfl
+
+/-- `ℍ[R, c₁, c₂]` has a basis over `R` given by `1`, `i`, `j`, and `k`. -/
+noncomputable def basis_one_i_j_k : basis (fin 4) R ℍ[R, c₁, c₂] :=
+basis.of_equiv_fun $ linear_equiv_tuple c₁ c₂
+
+@[simp] lemma coe_basis_one_i_j_k_repr (q : ℍ[R, c₁, c₂]) :
+  ⇑((basis_one_i_j_k c₁ c₂).repr q) = ![q.re, q.im_i, q.im_j, q.im_k] := rfl
+
+instance : module.finite R ℍ[R, c₁, c₂] := module.finite.of_basis (basis_one_i_j_k c₁ c₂)
+instance : module.free R ℍ[R, c₁, c₂] := module.free.of_basis (basis_one_i_j_k c₁ c₂)
+
+lemma dim_eq_four [strong_rank_condition R] : module.rank R ℍ[R, c₁, c₂] = 4 :=
+by { rw [dim_eq_card_basis (basis_one_i_j_k c₁ c₂), fintype.card_fin], norm_num }
+
+lemma finrank_eq_four [strong_rank_condition R] : finite_dimensional.finrank R ℍ[R, c₁, c₂] = 4 :=
+have cardinal.to_nat 4 = 4,
+  by rw [←cardinal.to_nat_cast 4, nat.cast_bit0, nat.cast_bit0, nat.cast_one],
+by rw [finite_dimensional.finrank, dim_eq_four, this]
+
 end
 
 @[norm_cast, simp] lemma coe_sub : ((x - y : R) : ℍ[R, c₁, c₂]) = x - y :=
@@ -344,10 +389,19 @@ def quaternion (R : Type*) [has_one R] [has_neg R] := quaternion_algebra R (-1)
 
 localized "notation (name := quaternion) `ℍ[` R `]` := quaternion R" in quaternion
 
-/-- The equivalence between the quaternions over R and R × R × R × R. -/
+/-- The equivalence between the quaternions over `R` and `R × R × R × R`. -/
+@[simps]
 def quaternion.equiv_prod (R : Type*) [has_one R] [has_neg R] : ℍ[R] ≃ R × R × R × R :=
 quaternion_algebra.equiv_prod _ _
 
+/-- The equivalence between the quaternions over `R` and `fin 4 → R`. -/
+@[simps symm_apply]
+def quaternion.equiv_tuple (R : Type*) [has_one R] [has_neg R] : ℍ[R] ≃ (fin 4 → R) :=
+quaternion_algebra.equiv_tuple _ _
+
+@[simp] lemma quaternion.equiv_tuple_apply (R : Type*) [has_one R] [has_neg R] (x : ℍ[R]) :
+  quaternion.equiv_tuple R x = ![x.re, x.im_i, x.im_j, x.im_k] := rfl
+
 namespace quaternion
 
 variables {R : Type*} [comm_ring R] (r x y z : R) (a b c : ℍ[R])
@@ -445,6 +499,15 @@ lemma mul_coe_eq_smul : a * r = r • a := quaternion_algebra.mul_coe_eq_smul r
 
 lemma smul_coe : x • (y : ℍ[R]) = ↑(x * y) := quaternion_algebra.smul_coe x y
 
+instance : module.finite R ℍ[R] := quaternion_algebra.module.finite _ _
+instance : module.free R ℍ[R] := quaternion_algebra.module.free _ _
+
+lemma dim_eq_four [strong_rank_condition R] : module.rank R ℍ[R] = 4 :=
+quaternion_algebra.dim_eq_four _ _
+
+lemma finrank_eq_four [strong_rank_condition R] : finite_dimensional.finrank R ℍ[R] = 4 :=
+quaternion_algebra.finrank_eq_four _ _
+
 /-- Quaternion conjugate. -/
 def conj : ℍ[R] ≃ₗ[R]  ℍ[R] := quaternion_algebra.conj
 

src/analysis/quaternion.lean

@@ -1,10 +1,11 @@
 /-
 Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Eric Wieser
 -/
 import algebra.quaternion
 import analysis.inner_product_space.basic
+import analysis.inner_product_space.pi_L2
 
 /-!
 # Quaternions as a normed algebra
@@ -15,6 +16,8 @@ In this file we define the following structures on the space `ℍ := ℍ[ℝ]` o
 * normed ring;
 * normed space over `ℝ`.
 
+We show that the norm on `ℍ[ℝ]` agrees with the euclidean norm of its components.
+
 ## Notation
 
 The following notation is available with `open_locale quaternion`:
@@ -29,8 +32,6 @@ quaternion, normed ring, normed space, normed algebra
 localized "notation (name := quaternion.real) `ℍ` := quaternion ℝ" in quaternion
 open_locale real_inner_product_space
 
-noncomputable theory
-
 namespace quaternion
 
 instance : has_inner ℝ ℍ := ⟨λ a b, (a * b.conj).re⟩
@@ -39,7 +40,7 @@ lemma inner_self (a : ℍ) : ⟪a, a⟫ = norm_sq a := rfl
 
 lemma inner_def (a b : ℍ) : ⟪a, b⟫ = (a * b.conj).re := rfl
 
-instance : inner_product_space ℝ ℍ :=
+noncomputable instance : inner_product_space ℝ ℍ :=
 inner_product_space.of_core
 { inner := has_inner.inner,
   conj_sym := λ x y, by simp [inner_def, mul_comm],
@@ -65,7 +66,7 @@ noncomputable instance : normed_division_ring ℍ :=
   norm_mul' := λ a b, by { simp only [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_mul],
                            exact real.sqrt_mul norm_sq_nonneg _ } }
 
-noncomputable instance : normed_algebra ℝ ℍ :=
+instance : normed_algebra ℝ ℍ :=
 { norm_smul_le := λ a x, (norm_smul a x).le,
   to_algebra := quaternion.algebra }
 
@@ -95,4 +96,42 @@ def of_complex : ℂ →ₐ[ℝ] ℍ :=
 
 @[simp] lemma coe_of_complex : ⇑of_complex = coe := rfl
 
+/-- The norm of the components as a euclidean vector equals the norm of the quaternion. -/
+lemma norm_pi_Lp_equiv_symm_equiv_tuple (x : ℍ) :
+  ‖(pi_Lp.equiv 2 (λ _ : fin 4, _)).symm (equiv_tuple ℝ x)‖ = ‖x‖ :=
+begin
+  rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, norm_sq_def', pi_Lp.inner_apply,
+    fin.sum_univ_four],
+  simp_rw [is_R_or_C.inner_apply, star_ring_end_apply, star_trivial, ←sq],
+  refl,
+end
+
+/-- `quaternion_algebra.linear_equiv_tuple` as a `linear_isometry_equiv`. -/
+@[simps apply symm_apply]
+noncomputable def linear_isometry_equiv_tuple : ℍ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin 4) :=
+{ to_fun := λ a, (pi_Lp.equiv _ (λ _ : fin 4, _)).symm ![a.1, a.2, a.3, a.4],
+  inv_fun := λ a, ⟨a 0, a 1, a 2, a 3⟩,
+  norm_map' := norm_pi_Lp_equiv_symm_equiv_tuple,
+  ..(quaternion_algebra.linear_equiv_tuple (-1 : ℝ) (-1 : ℝ)).trans
+      (pi_Lp.linear_equiv 2 ℝ (λ _ : fin 4, ℝ)).symm }
+
+@[continuity] lemma continuous_re : continuous (λ q : ℍ, q.re) :=
+(continuous_apply 0).comp linear_isometry_equiv_tuple.continuous
+
+@[continuity] lemma continuous_im_i : continuous (λ q : ℍ, q.im_i) :=
+(continuous_apply 1).comp linear_isometry_equiv_tuple.continuous
+
+@[continuity] lemma continuous_im_j : continuous (λ q : ℍ, q.im_j) :=
+(continuous_apply 2).comp linear_isometry_equiv_tuple.continuous
+
+@[continuity] lemma continuous_im_k : continuous (λ q : ℍ, q.im_k) :=
+(continuous_apply 3).comp linear_isometry_equiv_tuple.continuous
+
+instance : complete_space ℍ :=
+begin
+  have : uniform_embedding linear_isometry_equiv_tuple.to_linear_equiv.to_equiv.symm :=
+    linear_isometry_equiv_tuple.to_continuous_linear_equiv.symm.uniform_embedding,
+  exact (complete_space_congr this).1 (by apply_instance)
+end
+
 end quaternion