feat(data/quaternion): define quaternions and prove some basic proper…

…ties (#2339)

src/algebra/algebra/basic.lean

@@ -8,6 +8,7 @@ import data.matrix.basic
 import linear_algebra.tensor_product
 import ring_theory.subring
 import deprecated.subring
+import algebra.opposites
 
 /-!
 # Algebra over Commutative Semiring
@@ -321,6 +322,22 @@ end ring
 
 end algebra
 
+namespace opposite
+
+variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
+
+instance : algebra R Aᵒᵖ :=
+{ smul := λ c x, op (c • unop x),
+  to_ring_hom := (algebra_map R A).to_opposite $ λ x y, algebra.commutes _ _,
+  smul_def' := λ c x, by dsimp; simp only [op_mul, algebra.smul_def, algebra.commutes, op_unop],
+  commutes' := λ r, op_induction $ λ x, by dsimp; simp only [← op_mul, algebra.commutes] }
+
+@[simp] lemma op_smul (c : R) (a : A) : op (c • a) = c • op a := rfl
+
+@[simp] lemma algebra_map_apply (c : R) : algebra_map R Aᵒᵖ c = op (algebra_map R A c) := rfl
+
+end opposite
+
 namespace module
 variables (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [semimodule R M]
 

src/algebra/big_operators/basic.lean

@@ -969,6 +969,21 @@ lemma sum_flip [add_comm_monoid β] {n : ℕ} (f : ℕ → β) :
 @prod_flip (multiplicative β) _ _ _
 attribute [to_additive] prod_flip
 
+section opposite
+
+open opposite
+
+/-- Moving to the opposite additive commutative monoid commutes with summing. -/
+@[simp] lemma op_sum [add_comm_monoid β] {s : finset α} (f : α → β) :
+  op (∑ x in s, f x) = ∑ x in s, op (f x) :=
+(op_add_equiv : β ≃+ βᵒᵖ).map_sum _ _
+
+@[simp] lemma unop_sum [add_comm_monoid β] {s : finset α} (f : α → βᵒᵖ) :
+  unop (∑ x in s, f x) = ∑ x in s, unop (f x) :=
+(op_add_equiv : β ≃+ βᵒᵖ).symm.map_sum _ _
+
+end opposite
+
 section comm_group
 variables [comm_group β]
 

src/algebra/big_operators/order.lean

@@ -339,15 +339,4 @@ begin
   exact sum_lt_top_iff
 end
 
-open opposite
-
-/-- Moving to the opposite additive commutative monoid commutes with summing. -/
-@[simp] lemma op_sum [add_comm_monoid β] {s : finset α} (f : α → β) :
-  op (∑ x in s, f x) = ∑ x in s, op (f x) :=
-(@op_add_hom β _).map_sum _ _
-
-@[simp] lemma unop_sum [add_comm_monoid β] {s : finset α} (f : α → βᵒᵖ) :
-  unop (∑ x in s, f x) = ∑ x in s, unop (f x) :=
-(@unop_add_hom β _).map_sum _ _
-
 end with_top

src/algebra/module/linear_map.lean

@@ -443,6 +443,14 @@ e.to_equiv.image_eq_preimage s
 
 end
 
+/-- An involutive linear map is a linear equivalence. -/
+def of_involutive [semimodule R M] (f : M →ₗ[R] M) (hf : involutive f) : M ≃ₗ[R] M :=
+{ .. f, .. hf.to_equiv f  }
+
+@[simp] lemma coe_of_involutive [semimodule R M] (f : M →ₗ[R] M) (hf : involutive f) :
+  ⇑(of_involutive f hf) = f :=
+rfl
+
 end add_comm_monoid
 
 end linear_equiv

src/algebra/opposites.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import data.opposite
 import algebra.field
+import data.equiv.mul_add
 
 /-!
 # Algebraic operations on `αᵒᵖ`
@@ -166,13 +167,29 @@ variable {α}
 @[simp] lemma op_sub [add_group α] (x y : α) : op (x - y) = op x - op y := rfl
 @[simp] lemma unop_sub [add_group α] (x y : αᵒᵖ) : unop (x - y) = unop x - unop y := rfl
 
-/-- The function `op` is a homomorphism of additive commutative monoids. -/
-def op_add_hom [add_comm_monoid α] : α →+ αᵒᵖ := ⟨op, op_zero α, op_add⟩
+/-- The function `op` is an additive equivalence. -/
+def op_add_equiv [has_add α] : α ≃+ αᵒᵖ :=
+{ map_add' := λ a b, rfl, .. equiv_to_opposite }
 
-/-- The function `unop` is a homomorphism of additive commutative monoids. -/
-def unop_add_hom [add_comm_monoid α] : αᵒᵖ →+ α := ⟨unop, unop_zero α, unop_add⟩
+@[simp] lemma coe_op_add_equiv [has_add α] : (op_add_equiv : α → αᵒᵖ) = op := rfl
+@[simp] lemma coe_op_add_equiv_symm [has_add α] :
+  (op_add_equiv.symm : αᵒᵖ → α) = unop := rfl
 
-@[simp] lemma coe_op_add_hom [add_comm_monoid α] : (op_add_hom : α → αᵒᵖ) = op := rfl
-@[simp] lemma coe_unop_add_hom [add_comm_monoid α] : (unop_add_hom : αᵒᵖ → α) = unop := rfl
+@[simp] lemma op_add_equiv_to_equiv [has_add α] :
+  (op_add_equiv : α ≃+ αᵒᵖ).to_equiv = equiv_to_opposite :=
+rfl
 
 end opposite
+
+open opposite
+
+/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
+a ring homomorphism to `Sᵒᵖ`. -/
+def ring_hom.to_opposite {R S : Type*} [semiring R] [semiring S] (f : R →+* S)
+  (hf : ∀ x y, commute (f x) (f y)) : R →+* Sᵒᵖ :=
+{ map_one' := congr_arg op f.map_one,
+  map_mul' := λ x y, by simp [(hf x y).eq],
+  .. (opposite.op_add_equiv : S ≃+ Sᵒᵖ).to_add_monoid_hom.comp ↑f }
+
+@[simp] lemma ring_hom.coe_to_opposite {R S : Type*} [semiring R] [semiring S] (f : R →+* S)
+  (hf : ∀ x y, commute (f x) (f y)) : ⇑(f.to_opposite hf) = op ∘ f := rfl

src/analysis/normed_space/inner_product.lean

@@ -132,7 +132,7 @@ structure inner_product_space.core
 (inner     : F → F → 𝕜)
 (conj_sym  : ∀ x y, conj (inner y x) = inner x y)
 (nonneg_im : ∀ x, im (inner x x) = 0)
-(nonneg_re : ∀ x, re (inner x x) ≥ 0)
+(nonneg_re : ∀ x, 0 ≤ re (inner x x))
 (definite  : ∀ x, inner x x = 0 → x = 0)
 (add_left  : ∀ x y z, inner (x + y) z = inner x z + inner y z)
 (smul_left : ∀ x y r, inner (r • x) y = (conj r) * inner x y)

src/analysis/quaternion.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import data.quaternion
+import analysis.normed_space.inner_product
+
+/-!
+# Quaternions as a normed algebra
+
+In this file we define the following structures on the space `ℍ := ℍ[ℝ]` of quaternions:
+
+* inner product space;
+* normed ring;
+* normed space over `ℝ`.
+
+## Notation
+
+The following notation is available with `open_locale quaternion`:
+
+* `ℍ` : quaternions
+
+## Tags
+
+quaternion, normed ring, normed space, normed algebra
+-/
+
+localized "notation `ℍ` := quaternion ℝ" in quaternion
+open_locale real_inner_product_space
+
+noncomputable theory
+
+namespace quaternion
+
+instance : has_inner ℝ ℍ := ⟨λ a b, (a * b.conj).re⟩
+
+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 ℝ ℍ :=
+inner_product_space.of_core
+{ inner := has_inner.inner,
+  conj_sym := λ x y, by simp [inner_def, mul_comm],
+  nonneg_im := λ _, rfl,
+  nonneg_re := λ x, norm_sq_nonneg,
+  definite := λ x, norm_sq_eq_zero.1,
+  add_left := λ x y z, by simp only [inner_def, add_mul, add_re],
+  smul_left := λ x y r, by simp [inner_def] }
+
+lemma norm_sq_eq_norm_square (a : ℍ) : norm_sq a = ∥a∥ * ∥a∥ :=
+by rw [← inner_self, real_inner_self_eq_norm_square]
+
+instance : norm_one_class ℍ :=
+⟨by rw [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_one, real.sqrt_one]⟩
+
+@[simp] lemma norm_mul (a b : ℍ) : ∥a * b∥ = ∥a∥ * ∥b∥ :=
+begin
+  simp only [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_mul],
+  exact real.sqrt_mul norm_sq_nonneg _
+end
+
+@[simp, norm_cast] lemma norm_coe (a : ℝ) : ∥(a : ℍ)∥ = ∥a∥ :=
+by rw [norm_eq_sqrt_real_inner, inner_self, norm_sq_coe, real.sqrt_sqr_eq_abs, real.norm_eq_abs]
+
+noncomputable instance : normed_ring ℍ :=
+{ dist_eq := λ _ _, rfl,
+  norm_mul := λ a b, (norm_mul a b).le }
+
+noncomputable instance : normed_algebra ℝ ℍ :=
+{ norm_algebra_map_eq := norm_coe,
+  to_algebra := quaternion.algebra }
+
+instance : has_coe ℂ ℍ := ⟨λ z, ⟨z.re, z.im, 0, 0⟩⟩
+
+@[simp, norm_cast] lemma coe_complex_re (z : ℂ) : (z : ℍ).re = z.re := rfl
+@[simp, norm_cast] lemma coe_complex_im_i (z : ℂ) : (z : ℍ).im_i = z.im := rfl
+@[simp, norm_cast] lemma coe_complex_im_j (z : ℂ) : (z : ℍ).im_j = 0 := rfl
+@[simp, norm_cast] lemma coe_complex_im_k (z : ℂ) : (z : ℍ).im_k = 0 := rfl
+
+@[simp, norm_cast] lemma coe_complex_add (z w : ℂ) : ↑(z + w) = (z + w : ℍ) := by ext; simp
+@[simp, norm_cast] lemma coe_complex_mul (z w : ℂ) : ↑(z * w) = (z * w : ℍ) := by ext; simp
+@[simp, norm_cast] lemma coe_complex_zero : ((0 : ℂ) : ℍ) = 0 := rfl
+@[simp, norm_cast] lemma coe_complex_one : ((1 : ℂ) : ℍ) = 1 := rfl
+@[simp, norm_cast] lemma coe_complex_smul (r : ℝ) (z : ℂ) : ↑(r • z) = (r • z : ℍ) := by ext; simp
+@[simp, norm_cast] lemma coe_complex_coe (r : ℝ) : ((r : ℂ) : ℍ) = r := rfl
+
+/-- Coercion `ℂ →ₐ[ℝ] ℍ` as an algebra homomorphism. -/
+def of_complex : ℂ →ₐ[ℝ] ℍ :=
+{ to_fun := coe,
+  map_one' := rfl,
+  map_zero' := rfl,
+  map_add' := coe_complex_add,
+  map_mul' := coe_complex_mul,
+  commutes' := λ x, rfl }
+
+@[simp] lemma coe_of_complex : ⇑of_complex = coe := rfl
+
+end quaternion