From 7ab3ca854defd58cf5852161f55d13aedad5bf99 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 4 Nov 2020 05:43:18 +0000 Subject: [PATCH] feat(data/quaternion): define quaternions and prove some basic properties (#2339) --- src/algebra/algebra/basic.lean | 17 + src/algebra/big_operators/basic.lean | 15 + src/algebra/big_operators/order.lean | 11 - src/algebra/module/linear_map.lean | 8 + src/algebra/opposites.lean | 29 +- src/analysis/normed_space/inner_product.lean | 2 +- src/analysis/quaternion.lean | 100 ++++ src/data/quaternion.lean | 526 +++++++++++++++++++ src/number_theory/arithmetic_function.lean | 9 +- 9 files changed, 694 insertions(+), 23 deletions(-) create mode 100644 src/analysis/quaternion.lean create mode 100644 src/data/quaternion.lean diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index 5641aad31a475..db2cb82fc2201 100644 --- a/src/algebra/algebra/basic.lean +++ b/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] diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index 959e2cd6be305..20fc953b1bc57 100644 --- a/src/algebra/big_operators/basic.lean +++ b/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 β] diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean index b613f5a1ba6f7..e45822bfc3fe5 100644 --- a/src/algebra/big_operators/order.lean +++ b/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 diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean index e5a411d04286e..5da76b73c4aea 100644 --- a/src/algebra/module/linear_map.lean +++ b/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 diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean index 5d65f5512b9d5..997fbf3b13438 100644 --- a/src/algebra/opposites.lean +++ b/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 diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean index c842fd6f59ee9..ca5ab3cf34df7 100644 --- a/src/analysis/normed_space/inner_product.lean +++ b/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) diff --git a/src/analysis/quaternion.lean b/src/analysis/quaternion.lean new file mode 100644 index 0000000000000..3e5148d59030f --- /dev/null +++ b/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 diff --git a/src/data/quaternion.lean b/src/data/quaternion.lean new file mode 100644 index 0000000000000..16da03066b3ec --- /dev/null +++ b/src/data/quaternion.lean @@ -0,0 +1,526 @@ +/- +Copyright (c) 2020 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ +import tactic.ring_exp +import algebra.algebra.basic +import algebra.opposites +import data.equiv.ring + +/-! +# Quaternions + +In this file we define quaternions `ℍ[R]` over a commutative ring `R`, and define some +algebraic structures on `ℍ[R]`. + +## Main definitions + +* `quaternion_algebra R a b`, `ℍ[R, a, b]` : + [quaternion algebra](https://en.wikipedia.org/wiki/Quaternion_algebra) with coefficients `a`, `b` +* `quaternion R`, `ℍ[R]` : the space of quaternions, a.k.a. `quaternion_algebra R (-1) (-1)`; +* `quaternion.norm_sq` : square of the norm of a quaternion; +* `quaternion.conj` : conjugate of a quaternion; + +We also define the following algebraic structures on `ℍ[R]`: + +* `ring ℍ[R, a, b]` and `algebra R ℍ[R, a, b]` : for any commutative ring `R`; +* `ring ℍ[R]` and `algebra R ℍ[R]` : for any commutative ring `R`; +* `domain ℍ[R]` : for a linear ordered commutative ring `R`; +* `division_algebra ℍ[R]` : for a linear ordered field `R`. + +## Notation + +The following notation is available with `open_locale quaternion`. + +* `ℍ[R, c₁, c₂]` : `quaternion_algebra R c₁ c₂` +* `ℍ[R]` : quaternions over `R`. + +## Implementation notes + +We define quaternions over any ring `R`, not just `ℝ` to be able to deal with, e.g., integer +or rational quaternions without using real numbers. In particular, all definitions in this file +are computable. + +## Tags + +quaternion +-/ + +/-- Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$. +Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`. -/ +@[nolint unused_arguments, ext] +structure quaternion_algebra (R : Type*) (a b : R) := +mk {} :: (re : R) (im_i : R) (im_j : R) (im_k : R) + +localized "notation `ℍ[` R`,` a`,` b `]` := quaternion_algebra R a b" in quaternion + +namespace quaternion_algebra + +@[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 + +variables {R : Type*} [comm_ring R] {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R, c₁, c₂]) + +instance : has_coe_t R (ℍ[R, c₁, c₂]) := ⟨λ x, ⟨x, 0, 0, 0⟩⟩ + +@[simp] lemma coe_re : (x : ℍ[R, c₁, c₂]).re = x := rfl +@[simp] lemma coe_im_i : (x : ℍ[R, c₁, c₂]).im_i = 0 := rfl +@[simp] lemma coe_im_j : (x : ℍ[R, c₁, c₂]).im_j = 0 := rfl +@[simp] lemma coe_im_k : (x : ℍ[R, c₁, c₂]).im_k = 0 := rfl + +lemma coe_injective : function.injective (coe : R → ℍ[R, c₁, c₂]) := +λ x y h, congr_arg re h + +@[simp] lemma coe_inj {x y : R} : (x : ℍ[R, c₁, c₂]) = y ↔ x = y := coe_injective.eq_iff + +@[simps] instance : has_zero ℍ[R, c₁, c₂] := ⟨⟨0, 0, 0, 0⟩⟩ + +@[simp, norm_cast] lemma coe_zero : ((0 : R) : ℍ[R, c₁, c₂]) = 0 := rfl + +instance : inhabited ℍ[R, c₁, c₂] := ⟨0⟩ + +@[simps] instance : has_one ℍ[R, c₁, c₂] := ⟨⟨1, 0, 0, 0⟩⟩ + +@[simp, norm_cast] lemma coe_one : ((1 : R) : ℍ[R, c₁, c₂]) = 1 := rfl + +@[simps] instance : has_add ℍ[R, c₁, c₂] := +⟨λ a b, ⟨a.1 + b.1, a.2 + b.2, a.3 + b.3, a.4 + b.4⟩⟩ + +@[simp] lemma mk_add_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) : + (mk a₁ a₂ a₃ a₄ : ℍ[R, c₁, c₂]) + mk b₁ b₂ b₃ b₄ = mk (a₁ + b₁) (a₂ + b₂) (a₃ + b₃) (a₄ + b₄) := +rfl + +@[simps] instance : has_neg ℍ[R, c₁, c₂] := ⟨λ a, ⟨-a.1, -a.2, -a.3, -a.4⟩⟩ + +@[simp] lemma neg_mk (a₁ a₂ a₃ a₄ : R) : -(mk a₁ a₂ a₃ a₄ : ℍ[R, c₁, c₂]) = ⟨-a₁, -a₂, -a₃, -a₄⟩ := +rfl + +/-- Multiplication is given by + +* `1 * x = x * 1 = x`; +* `i * i = c₁`; +* `j * j = c₂`; +* `i * j = k`, `j * i = -k`; +* `k * k = -c₁ * c₂`; +* `i * k = c₁ * j`, `k * i = `-c₁ * j`; +* `j * k = -c₂ * i`, `k * j = c₂ * i`. -/ +@[simps] instance : has_mul ℍ[R, c₁, c₂] := ⟨λ a b, + ⟨a.1 * b.1 + c₁ * a.2 * b.2 + c₂ * a.3 * b.3 - c₁ * c₂ * a.4 * b.4, + a.1 * b.2 + a.2 * b.1 - c₂ * a.3 * b.4 + c₂ * a.4 * b.3, + a.1 * b.3 + c₁ * a.2 * b.4 + a.3 * b.1 - c₁ * a.4 * b.2, + a.1 * b.4 + a.2 * b.3 - a.3 * b.2 + a.4 * b.1⟩⟩ + +@[simp] lemma mk_mul_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) : + (mk a₁ a₂ a₃ a₄ : ℍ[R, c₁, c₂]) * mk b₁ b₂ b₃ b₄ = + ⟨a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄, + a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃, + a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, + a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁⟩ := rfl + +instance : ring ℍ[R, c₁, c₂] := +by refine_struct + { add := (+), zero := (0 : ℍ[R, c₁, c₂]), neg := has_neg.neg, mul := (*), one := 1 }; + intros; ext; simp; ring_exp + +@[simp] lemma mk_sub_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) : + (mk a₁ a₂ a₃ a₄ : ℍ[R, c₁, c₂]) - mk b₁ b₂ b₃ b₄ = mk (a₁ - b₁) (a₂ - b₂) (a₃ - b₃) (a₄ - b₄) := +rfl + +instance : algebra R ℍ[R, c₁, c₂] := +{ smul := λ r a, ⟨r * a.1, r * a.2, r * a.3, r * a.4⟩, + to_fun := coe, + map_one' := rfl, + map_zero' := rfl, + map_mul' := λ x y, by ext; simp, + map_add' := λ x y, by ext; simp, + smul_def' := λ r x, by ext; simp, + commutes' := λ r x, by ext; simp [mul_comm] } + +@[simp] lemma smul_re : (r • a).re = r • a.re := rfl +@[simp] lemma smul_im_i : (r • a).im_i = r • a.im_i := rfl +@[simp] lemma smul_im_j : (r • a).im_j = r • a.im_j := rfl +@[simp] lemma smul_im_k : (r • a).im_k = r • a.im_k := rfl + +@[norm_cast, simp] lemma coe_add : ((x + y : R) : ℍ[R, c₁, c₂]) = x + y := +(algebra_map R ℍ[R, c₁, c₂]).map_add x y + +@[norm_cast, simp] lemma coe_sub : ((x - y : R) : ℍ[R, c₁, c₂]) = x - y := +(algebra_map R ℍ[R, c₁, c₂]).map_sub x y + +@[norm_cast, simp] lemma coe_neg : ((-x : R) : ℍ[R, c₁, c₂]) = -x := +(algebra_map R ℍ[R, c₁, c₂]).map_neg x + +@[norm_cast, simp] lemma coe_mul : ((x * y : R) : ℍ[R, c₁, c₂]) = x * y := +(algebra_map R ℍ[R, c₁, c₂]).map_mul x y + +lemma coe_commutes : ↑r * a = a * r := algebra.commutes r a + +lemma coe_commute : commute ↑r a := coe_commutes r a + +lemma coe_mul_eq_smul : ↑r * a = r • a := (algebra.smul_def r a).symm + +lemma mul_coe_eq_smul : a * r = r • a := +by rw [← coe_commutes, coe_mul_eq_smul] + +@[norm_cast, simp] lemma coe_algebra_map : ⇑(algebra_map R ℍ[R, c₁, c₂]) = coe := rfl + +lemma smul_coe : x • (y : ℍ[R, c₁, c₂]) = ↑(x * y) := by rw [coe_mul, coe_mul_eq_smul] + +/-- Quaternion conjugate. -/ +def conj : ℍ[R, c₁, c₂] ≃ₗ[R] ℍ[R, c₁, c₂] := +linear_equiv.of_involutive +{ to_fun := λ a, ⟨a.1, -a.2, -a.3, -a.4⟩, + map_add' := λ a b, by ext; simp [neg_add], + map_smul' := λ r a, by ext; simp } $ +λ a, by simp + +@[simp] lemma re_conj : (conj a).re = a.re := rfl +@[simp] lemma im_i_conj : (conj a).im_i = - a.im_i := rfl +@[simp] lemma im_j_conj : (conj a).im_j = - a.im_j := rfl +@[simp] lemma im_k_conj : (conj a).im_k = - a.im_k := rfl + +@[simp] lemma conj_conj : a.conj.conj = a := ext _ _ rfl (neg_neg _) (neg_neg _) (neg_neg _) + +lemma conj_add : (a + b).conj = a.conj + b.conj := conj.map_add a b + +@[simp] lemma conj_mul : (a * b).conj = b.conj * a.conj := by ext; simp; ring_exp + +lemma conj_conj_mul : (a.conj * b).conj = b.conj * a := +by rw [conj_mul, conj_conj] + +lemma conj_mul_conj : (a * b.conj).conj = b * a.conj := +by rw [conj_mul, conj_conj] + +lemma self_add_conj' : a + a.conj = ↑(2 * a.re) := by ext; simp [two_mul] + +lemma self_add_conj : a + a.conj = 2 * a.re := +by simp only [self_add_conj', two_mul, coe_add] + +lemma conj_add_self' : a.conj + a = ↑(2 * a.re) := by rw [add_comm, self_add_conj'] + +lemma conj_add_self : a.conj + a = 2 * a.re := by rw [add_comm, self_add_conj] + +lemma conj_eq_two_re_sub : a.conj = ↑(2 * a.re) - a := eq_sub_iff_add_eq.2 a.conj_add_self' + +lemma commute_conj_self : commute a.conj a := +begin + rw [a.conj_eq_two_re_sub], + exact (coe_commute (2 * a.re) a).sub_left (commute.refl a) +end + +lemma commute_self_conj : commute a a.conj := +a.commute_conj_self.symm + +lemma commute_conj_conj {a b : ℍ[R, c₁, c₂]} (h : commute a b) : commute a.conj b.conj := +calc a.conj * b.conj = (b * a).conj : (conj_mul b a).symm + ... = (a * b).conj : by rw h.eq + ... = b.conj * a.conj : conj_mul a b + +@[simp] lemma conj_coe : conj (x : ℍ[R, c₁, c₂]) = x := by ext; simp + +lemma conj_smul : conj (r • a) = r • conj a := conj.map_smul r a + +@[simp] lemma conj_one : conj (1 : ℍ[R, c₁, c₂]) = 1 := conj_coe 1 + +lemma eq_re_of_eq_coe {a : ℍ[R, c₁, c₂]} {x : R} (h : a = x) : a = a.re := +by rw [h, coe_re] + +lemma eq_re_iff_mem_range_coe {a : ℍ[R, c₁, c₂]} : + a = a.re ↔ a ∈ set.range (coe : R → ℍ[R, c₁, c₂]) := +⟨λ h, ⟨a.re, h.symm⟩, λ ⟨x, h⟩, eq_re_of_eq_coe h.symm⟩ + +@[simp] +lemma conj_fixed {R : Type*} [integral_domain R] [char_zero R] {c₁ c₂ : R} {a : ℍ[R, c₁, c₂]} : + conj a = a ↔ a = a.re := +by simp [ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero] + +-- Can't use `rw ← conj_fixed` in the proof without additional assumptions + +lemma conj_mul_eq_coe : conj a * a = (conj a * a).re := by ext; simp; ring_exp + +lemma mul_conj_eq_coe : a * conj a = (a * conj a).re := +by { rw a.commute_self_conj.eq, exact a.conj_mul_eq_coe } + +lemma conj_zero : conj (0 : ℍ[R, c₁, c₂]) = 0 := conj.map_zero + +lemma conj_neg : (-a).conj = -a.conj := (conj : ℍ[R, c₁, c₂] ≃ₗ[R] _).map_neg a + +lemma conj_sub : (a - b).conj = a.conj - b.conj := (conj : ℍ[R, c₁, c₂] ≃ₗ[R] _).map_sub a b + +open opposite + +/-- Quaternion conjugate as an `alg_equiv` to the opposite ring. -/ +def conj_alg_equiv : ℍ[R, c₁, c₂] ≃ₐ[R] (ℍ[R, c₁, c₂]ᵒᵖ) := +{ to_fun := op ∘ conj, + inv_fun := conj ∘ unop, + map_mul' := λ x y, by simp, + commutes' := λ r, by simp, + .. conj.to_add_equiv.trans op_add_equiv } + +@[simp] lemma coe_conj_alg_equiv : ⇑(conj_alg_equiv : ℍ[R, c₁, c₂] ≃ₐ[R] _) = op ∘ conj := rfl + +end quaternion_algebra + +/-- Space of quaternions over a type. Implemented as a structure with four fields: +`re`, `im_i`, `im_j`, and `im_k`. -/ +def quaternion (R : Type*) [has_one R] [has_neg R] := quaternion_algebra R (-1) (-1) + +localized "notation `ℍ[` R `]` := quaternion R" in quaternion + +namespace quaternion + +variables {R : Type*} [comm_ring R] (r x y z : R) (a b c : ℍ[R]) + +export quaternion_algebra (re im_i im_j im_k) + +instance : has_coe_t R ℍ[R] := quaternion_algebra.has_coe_t +instance : ring ℍ[R] := quaternion_algebra.ring +instance : inhabited ℍ[R] := quaternion_algebra.inhabited +instance : algebra R ℍ[R] := quaternion_algebra.algebra + +@[ext] lemma ext : a.re = b.re → a.im_i = b.im_i → a.im_j = b.im_j → a.im_k = b.im_k → a = b := +quaternion_algebra.ext a b + +lemma ext_iff {a b : ℍ[R]} : + a = b ↔ a.re = b.re ∧ a.im_i = b.im_i ∧ a.im_j = b.im_j ∧ a.im_k = b.im_k := +quaternion_algebra.ext_iff a b + +@[simp, norm_cast] lemma coe_re : (x : ℍ[R]).re = x := rfl +@[simp, norm_cast] lemma coe_im_i : (x : ℍ[R]).im_i = 0 := rfl +@[simp, norm_cast] lemma coe_im_j : (x : ℍ[R]).im_j = 0 := rfl +@[simp, norm_cast] lemma coe_im_k : (x : ℍ[R]).im_k = 0 := rfl + +@[simp] lemma zero_re : (0 : ℍ[R]).re = 0 := rfl +@[simp] lemma zero_im_i : (0 : ℍ[R]).im_i = 0 := rfl +@[simp] lemma zero_im_j : (0 : ℍ[R]).im_j = 0 := rfl +@[simp] lemma zero_im_k : (0 : ℍ[R]).im_k = 0 := rfl +@[simp, norm_cast] lemma coe_zero : ((0 : R) : ℍ[R]) = 0 := rfl + +@[simp] lemma one_re : (1 : ℍ[R]).re = 1 := rfl +@[simp] lemma one_im_i : (1 : ℍ[R]).im_i = 0 := rfl +@[simp] lemma one_im_j : (1 : ℍ[R]).im_j = 0 := rfl +@[simp] lemma one_im_k : (1 : ℍ[R]).im_k = 0 := rfl +@[simp, norm_cast] lemma coe_one : ((1 : R) : ℍ[R]) = 1 := rfl + +@[simp] lemma add_re : (a + b).re = a.re + b.re := rfl +@[simp] lemma add_im_i : (a + b).im_i = a.im_i + b.im_i := rfl +@[simp] lemma add_im_j : (a + b).im_j = a.im_j + b.im_j := rfl +@[simp] lemma add_im_k : (a + b).im_k = a.im_k + b.im_k := rfl +@[simp, norm_cast] lemma coe_add : ((x + y : R) : ℍ[R]) = x + y := quaternion_algebra.coe_add x y + +@[simp] lemma neg_re : (-a).re = -a.re := rfl +@[simp] lemma neg_im_i : (-a).im_i = -a.im_i := rfl +@[simp] lemma neg_im_j : (-a).im_j = -a.im_j := rfl +@[simp] lemma neg_im_k : (-a).im_k = -a.im_k := rfl +@[simp, norm_cast] lemma coe_neg : ((-x : R) : ℍ[R]) = -x := quaternion_algebra.coe_neg x + +@[simp] lemma sub_re : (a - b).re = a.re - b.re := rfl +@[simp] lemma sub_im_i : (a - b).im_i = a.im_i - b.im_i := rfl +@[simp] lemma sub_im_j : (a - b).im_j = a.im_j - b.im_j := rfl +@[simp] lemma sub_im_k : (a - b).im_k = a.im_k - b.im_k := rfl +@[simp, norm_cast] lemma coe_sub : ((x - y : R) : ℍ[R]) = x - y := quaternion_algebra.coe_sub x y + +@[simp] lemma mul_re : + (a * b).re = a.re * b.re - a.im_i * b.im_i - a.im_j * b.im_j - a.im_k * b.im_k := +(quaternion_algebra.has_mul_mul_re a b).trans $ + by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg] + +@[simp] lemma mul_im_i : + (a * b).im_i = a.re * b.im_i + a.im_i * b.re + a.im_j * b.im_k - a.im_k * b.im_j := +(quaternion_algebra.has_mul_mul_im_i a b).trans $ + by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg] + +@[simp] lemma mul_im_j : + (a * b).im_j = a.re * b.im_j - a.im_i * b.im_k + a.im_j * b.re + a.im_k * b.im_i := +(quaternion_algebra.has_mul_mul_im_j a b).trans $ + by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg] + +@[simp] lemma mul_im_k : + (a * b).im_k = a.re * b.im_k + a.im_i * b.im_j - a.im_j * b.im_i + a.im_k * b.re := +(quaternion_algebra.has_mul_mul_im_k a b).trans $ + by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg] + +@[simp, norm_cast] lemma coe_mul : ((x * y : R) : ℍ[R]) = x * y := quaternion_algebra.coe_mul x y + +lemma coe_injective : function.injective (coe : R → ℍ[R]) := quaternion_algebra.coe_injective + +@[simp] lemma coe_inj {x y : R} : (x : ℍ[R]) = y ↔ x = y := coe_injective.eq_iff + +@[simp] lemma smul_re : (r • a).re = r • a.re := rfl +@[simp] lemma smul_im_i : (r • a).im_i = r • a.im_i := rfl +@[simp] lemma smul_im_j : (r • a).im_j = r • a.im_j := rfl +@[simp] lemma smul_im_k : (r • a).im_k = r • a.im_k := rfl + +lemma coe_commutes : ↑r * a = a * r := quaternion_algebra.coe_commutes r a + +lemma coe_commute : commute ↑r a := quaternion_algebra.coe_commute r a + +lemma coe_mul_eq_smul : ↑r * a = r • a := quaternion_algebra.coe_mul_eq_smul r a + +lemma mul_coe_eq_smul : a * r = r • a := quaternion_algebra.mul_coe_eq_smul r a + +@[simp] lemma algebra_map_def : ⇑(algebra_map R ℍ[R]) = coe := rfl + +lemma smul_coe : x • (y : ℍ[R]) = ↑(x * y) := quaternion_algebra.smul_coe x y + +/-- Quaternion conjugate. -/ +def conj : ℍ[R] ≃ₗ[R] ℍ[R] := quaternion_algebra.conj + +@[simp] lemma conj_re : a.conj.re = a.re := rfl +@[simp] lemma conj_im_i : a.conj.im_i = - a.im_i := rfl +@[simp] lemma conj_im_j : a.conj.im_j = - a.im_j := rfl +@[simp] lemma conj_im_k : a.conj.im_k = - a.im_k := rfl + +@[simp] lemma conj_conj : a.conj.conj = a := a.conj_conj + +@[simp] lemma conj_add : (a + b).conj = a.conj + b.conj := a.conj_add b + +@[simp] lemma conj_mul : (a * b).conj = b.conj * a.conj := a.conj_mul b + +lemma conj_conj_mul : (a.conj * b).conj = b.conj * a := a.conj_conj_mul b + +lemma conj_mul_conj : (a * b.conj).conj = b * a.conj := a.conj_mul_conj b + +lemma self_add_conj' : a + a.conj = ↑(2 * a.re) := a.self_add_conj' + +lemma self_add_conj : a + a.conj = 2 * a.re := a.self_add_conj + +lemma conj_add_self' : a.conj + a = ↑(2 * a.re) := a.conj_add_self' + +lemma conj_add_self : a.conj + a = 2 * a.re := a.conj_add_self + +lemma conj_eq_two_re_sub : a.conj = ↑(2 * a.re) - a := a.conj_eq_two_re_sub + +lemma commute_conj_self : commute a.conj a := a.commute_conj_self + +lemma commute_self_conj : commute a a.conj := a.commute_self_conj + +lemma commute_conj_conj {a b : ℍ[R]} (h : commute a b) : commute a.conj b.conj := +quaternion_algebra.commute_conj_conj h + +alias commute_conj_conj ← commute.quaternion_conj + +@[simp] lemma conj_coe : conj (x : ℍ[R]) = x := quaternion_algebra.conj_coe x + +@[simp] lemma conj_smul : conj (r • a) = r • conj a := a.conj_smul r + +@[simp] lemma conj_one : conj (1 : ℍ[R]) = 1 := conj_coe 1 + +lemma eq_re_of_eq_coe {a : ℍ[R]} {x : R} (h : a = x) : a = a.re := +quaternion_algebra.eq_re_of_eq_coe h + +lemma eq_re_iff_mem_range_coe {a : ℍ[R]} : a = a.re ↔ a ∈ set.range (coe : R → ℍ[R]) := +quaternion_algebra.eq_re_iff_mem_range_coe + +@[simp] lemma conj_fixed {R : Type*} [integral_domain R] [char_zero R] {a : ℍ[R]} : + conj a = a ↔ a = a.re := +quaternion_algebra.conj_fixed + +lemma conj_mul_eq_coe : conj a * a = (conj a * a).re := a.conj_mul_eq_coe + +lemma mul_conj_eq_coe : a * conj a = (a * conj a).re := a.mul_conj_eq_coe + +@[simp] lemma conj_zero : conj (0:ℍ[R]) = 0 := quaternion_algebra.conj_zero + +@[simp] lemma conj_neg : (-a).conj = -a.conj := a.conj_neg + +@[simp] lemma conj_sub : (a - b).conj = a.conj - b.conj := a.conj_sub b + +open opposite + +/-- Quaternion conjugate as an `alg_equiv` to the opposite ring. -/ +def conj_alg_equiv : ℍ[R] ≃ₐ[R] (ℍ[R]ᵒᵖ) := quaternion_algebra.conj_alg_equiv + +@[simp] lemma coe_conj_alg_equiv : ⇑(conj_alg_equiv : ℍ[R] ≃ₐ[R] ℍ[R]ᵒᵖ) = op ∘ conj := rfl + +/-- Square of the norm. -/ +def norm_sq : ℍ[R] →* R := +{ to_fun := λ a, (a * a.conj).re, + map_one' := by rw [conj_one, one_mul, one_re], + map_mul' := λ x y, coe_injective $ by conv_lhs { rw [← mul_conj_eq_coe, conj_mul, mul_assoc, + ← mul_assoc y, y.mul_conj_eq_coe, coe_commutes, ← mul_assoc, x.mul_conj_eq_coe, ← coe_mul] } } + +lemma norm_sq_def : norm_sq a = (a * a.conj).re := rfl + +lemma norm_sq_def' : norm_sq a = a.1^2 + a.2^2 + a.3^2 + a.4^2 := +by simp only [norm_sq_def, pow_two, ← neg_mul_eq_mul_neg, sub_neg_eq_add, + mul_re, conj_re, conj_im_i, conj_im_j, conj_im_k] + +lemma norm_sq_coe : norm_sq (x : ℍ[R]) = x^2 := +by rw [norm_sq_def, conj_coe, ← coe_mul, coe_re, pow_two] + +lemma norm_sq_zero : norm_sq (0 : ℍ[R]) = 0 := +by simp [norm_sq_def', pow_two, mul_zero, add_zero] + +@[simp] lemma norm_sq_neg : norm_sq (-a) = norm_sq a := +by simp only [norm_sq_def, conj_neg, neg_mul_neg] + +lemma self_mul_conj : a * a.conj = norm_sq a := by rw [mul_conj_eq_coe, norm_sq_def] + +lemma conj_mul_self : a.conj * a = norm_sq a := by rw [← a.commute_self_conj.eq, self_mul_conj] + +lemma coe_norm_sq_add : + (norm_sq (a + b) : ℍ[R]) = norm_sq a + a * b.conj + b * a.conj + norm_sq b := +by simp [← self_mul_conj, mul_add, add_mul, add_assoc] + +end quaternion + +namespace quaternion + +variables {R : Type*} + +section linear_ordered_comm_ring + +variables [linear_ordered_comm_ring R] {a : ℍ[R]} + +@[simp] lemma norm_sq_eq_zero : norm_sq a = 0 ↔ a = 0 := +begin + refine ⟨λ h, _, λ h, h.symm ▸ norm_sq_zero⟩, + rw [norm_sq_def', add_eq_zero_iff_eq_zero_of_nonneg, add_eq_zero_iff_eq_zero_of_nonneg, + add_eq_zero_iff_eq_zero_of_nonneg] at h, + exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2), + all_goals { apply_rules [pow_two_nonneg, add_nonneg] } +end + +lemma norm_sq_ne_zero : norm_sq a ≠ 0 ↔ a ≠ 0 := not_congr norm_sq_eq_zero + +@[simp] lemma norm_sq_nonneg : 0 ≤ norm_sq a := +by { rw norm_sq_def', apply_rules [pow_two_nonneg, add_nonneg] } + +@[simp] lemma norm_sq_le_zero : norm_sq a ≤ 0 ↔ a = 0 := +by simpa only [le_antisymm_iff, norm_sq_nonneg, and_true] using @norm_sq_eq_zero _ _ a + +instance : domain ℍ[R] := +{ exists_pair_ne := ⟨0, 1, mt (congr_arg re) zero_ne_one⟩, + eq_zero_or_eq_zero_of_mul_eq_zero := λ a b hab, + have norm_sq a * norm_sq b = 0, by rwa [← norm_sq.map_mul, norm_sq_eq_zero], + (eq_zero_or_eq_zero_of_mul_eq_zero this).imp norm_sq_eq_zero.1 norm_sq_eq_zero.1, + .. quaternion.ring } + +end linear_ordered_comm_ring + +section field + +variables [linear_ordered_field R] (a b : ℍ[R]) + +@[simps { attrs := [] }]instance : has_inv ℍ[R] := ⟨λ a, (norm_sq a)⁻¹ • a.conj⟩ + +instance : division_ring ℍ[R] := +{ inv := has_inv.inv, + inv_zero := by rw [has_inv_inv, conj_zero, smul_zero], + inv_mul_cancel := λ a ha, by rw [has_inv_inv, algebra.smul_mul_assoc, conj_mul_self, smul_coe, + inv_mul_cancel (norm_sq_ne_zero.2 ha), coe_one], + mul_inv_cancel := λ a ha, by rw [has_inv_inv, algebra.mul_smul_comm, self_mul_conj, smul_coe, + inv_mul_cancel (norm_sq_ne_zero.2 ha), coe_one], + .. quaternion.domain } + +@[simp] lemma norm_sq_inv : norm_sq a⁻¹ = (norm_sq a)⁻¹ := +(norm_sq : ℍ[R] →* R).map_inv' norm_sq_zero _ + +@[simp] lemma norm_sq_div : norm_sq (a / b) = norm_sq a / norm_sq b := +(norm_sq : ℍ[R] →* R).map_div norm_sq_zero a b + +end field + +end quaternion diff --git a/src/number_theory/arithmetic_function.lean b/src/number_theory/arithmetic_function.lean index f0fded6d2a39c..5688f9ac8ed27 100644 --- a/src/number_theory/arithmetic_function.lean +++ b/src/number_theory/arithmetic_function.lean @@ -274,9 +274,9 @@ theorem mul_zeta_apply [semiring R] {f : arithmetic_function R} {x : ℕ} : (f * ζ) x = ∑ i in divisors x, f i := begin apply opposite.op_injective, - rw [← opposite.coe_op_add_hom, add_monoid_hom.map_sum], - convert @zeta_mul_apply Rᵒᵖ _ { to_fun := opposite.op_add_hom ∘ f, map_zero' := by simp} x, - rw [mul_apply, mul_apply, add_monoid_hom.map_sum], + rw [op_sum], + convert @zeta_mul_apply Rᵒᵖ _ { to_fun := opposite.op ∘ f, map_zero' := by simp} x, + rw [mul_apply, mul_apply, op_sum], conv_lhs { rw ← map_swap_divisors_antidiagonal, }, rw sum_map, apply sum_congr rfl, @@ -284,8 +284,7 @@ begin by_cases h1 : y.fst = 0, { simp [function.comp_apply, h1] }, { simp only [h1, mul_one, one_mul, prod.fst_swap, function.embedding.coe_fn_mk, prod.snd_swap, - if_false, zeta_apply, opposite.coe_op_add_hom], - refl } + if_false, zeta_apply, zero_hom.coe_mk] } end end zeta