diff --git a/src/algebra/star/self_adjoint.lean b/src/algebra/star/self_adjoint.lean index 81381369e5838..27d5d68348dd7 100644 --- a/src/algebra/star/self_adjoint.lean +++ b/src/algebra/star/self_adjoint.lean @@ -55,6 +55,8 @@ by { rw [←add_subgroup.mem_carrier], exact iff.rfl } @[simp, norm_cast] lemma star_coe_eq {x : self_adjoint R} : star (x : R) = x := x.prop +instance : inhabited (self_adjoint R) := ⟨0⟩ + end add_group instance [add_comm_group R] [star_add_monoid R] : add_comm_group (self_adjoint R) := @@ -68,6 +70,8 @@ instance : has_one (self_adjoint R) := ⟨⟨1, by rw [mem_iff, star_one]⟩⟩ @[simp, norm_cast] lemma coe_one : (coe : self_adjoint R → R) (1 : self_adjoint R) = (1 : R) := rfl +instance [nontrivial R] : nontrivial (self_adjoint R) := ⟨⟨0, 1, subtype.ne_of_val_ne zero_ne_one⟩⟩ + lemma one_mem : (1 : R) ∈ self_adjoint R := by simp only [mem_iff, star_one] lemma bit0_mem {x : R} (hx : x ∈ self_adjoint R) : bit0 x ∈ self_adjoint R := diff --git a/src/algebra/star/unitary.lean b/src/algebra/star/unitary.lean new file mode 100644 index 0000000000000..e539eb74f5dbf --- /dev/null +++ b/src/algebra/star/unitary.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2022 Frédéric Dupuis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shing Tak Lam, Frédéric Dupuis +-/ +import algebra.star.basic +import group_theory.submonoid.operations + +/-! +# Unitary elements of a star monoid + +This file defines `unitary R`, where `R` is a star monoid, as the submonoid made of the elements +that satisfy `star U * U = 1` and `U * star U = 1`, and these form a group. +This includes, for instance, unitary operators on Hilbert spaces. + +See also `matrix.unitary_group` for specializations to `unitary (matrix n n R)`. + +## Tags + +unitary +-/ + +/-- +In a `star_monoid R`, `unitary R` is the submonoid consisting of all the elements `U` of +`R` such that `star U * U = 1` and `U * star U = 1`. +-/ +def unitary (R : Type*) [monoid R] [star_monoid R] : submonoid R := +{ carrier := {U | star U * U = 1 ∧ U * star U = 1}, + one_mem' := by simp only [mul_one, and_self, set.mem_set_of_eq, star_one], + mul_mem' := λ U B ⟨hA₁, hA₂⟩ ⟨hB₁, hB₂⟩, + begin + refine ⟨_, _⟩, + { calc star (U * B) * (U * B) = star B * star U * U * B : by simp only [mul_assoc, star_mul] + ... = star B * (star U * U) * B : by rw [←mul_assoc] + ... = 1 : by rw [hA₁, mul_one, hB₁] }, + { calc U * B * star (U * B) = U * B * (star B * star U) : by rw [star_mul] + ... = U * (B * star B) * star U : by simp_rw [←mul_assoc] + ... = 1 : by rw [hB₂, mul_one, hA₂] } + end } + +variables {R : Type*} + +namespace unitary +variables [monoid R] [star_monoid R] + +@[simp] lemma star_mul_self_of_mem {U : R} (hU : U ∈ unitary R) : star U * U = 1 := hU.1 +@[simp] lemma mul_star_self_of_mem {U : R} (hU : U ∈ unitary R) : U * star U = 1 := hU.2 + +lemma star_mem {U : R} (hU : U ∈ unitary R) : star U ∈ unitary R := +⟨by rw [star_star, mul_star_self_of_mem hU], by rw [star_star, star_mul_self_of_mem hU]⟩ + +@[simp] lemma star_mem_iff {U : R} : star U ∈ unitary R ↔ U ∈ unitary R := +⟨λ h, star_star U ▸ star_mem h, star_mem⟩ + +instance : has_star (unitary R) := ⟨λ U, ⟨star U, star_mem U.prop⟩⟩ + +@[simp, norm_cast] lemma coe_star {U : unitary R} : ↑(star U) = (star U : R) := rfl + +lemma coe_star_mul_self (U : unitary R) : (star U : R) * U = 1 := star_mul_self_of_mem U.prop +lemma coe_mul_star_self (U : unitary R) : (U : R) * star U = 1 := mul_star_self_of_mem U.prop + +@[simp] lemma star_mul_self (U : unitary R) : star U * U = 1 := subtype.ext $ coe_star_mul_self U +@[simp] lemma mul_star_self (U : unitary R) : U * star U = 1 := subtype.ext $ coe_mul_star_self U + +instance : group (unitary R) := +{ inv := star, + mul_left_inv := star_mul_self, + ..submonoid.to_monoid _ } + +instance : has_involutive_star (unitary R) := +⟨λ _, by { ext, simp only [coe_star, star_star] }⟩ + +instance : star_monoid (unitary R) := +⟨λ _ _, by { ext, simp only [coe_star, submonoid.coe_mul, star_mul] }⟩ + +instance : inhabited (unitary R) := ⟨1⟩ + +lemma star_eq_inv (U : unitary R) : star U = U⁻¹ := rfl + +lemma star_eq_inv' : (star : unitary R → unitary R) = has_inv.inv := rfl + +end unitary diff --git a/src/analysis/normed_space/star.lean b/src/analysis/normed_space/star.lean index 5de8d4b86595b..763f836aab9be 100644 --- a/src/analysis/normed_space/star.lean +++ b/src/analysis/normed_space/star.lean @@ -7,6 +7,7 @@ Authors: Frédéric Dupuis import analysis.normed.group.hom import analysis.normed_space.basic import analysis.normed_space.linear_isometry +import algebra.star.unitary /-! # Normed star rings and algebras @@ -138,6 +139,53 @@ begin exact one_ne_zero (norm_eq_zero.mp h) } end +@[priority 100] -- see Note [lower instance priority] +instance [nontrivial E] : norm_one_class E := ⟨norm_one⟩ + +lemma norm_coe_unitary [nontrivial E] (U : unitary E) : ∥(U : E)∥ = 1 := +begin + have := calc + ∥(U : E)∥^2 = ∥(U : E)∥ * ∥(U : E)∥ : pow_two _ + ... = ∥(U⋆ * U : E)∥ : cstar_ring.norm_star_mul_self.symm + ... = ∥(1 : E)∥ : by rw unitary.coe_star_mul_self + ... = 1 : cstar_ring.norm_one, + refine (sq_eq_sq (norm_nonneg _) zero_le_one).mp _, + rw [one_pow 2, this], +end + +@[simp] lemma norm_of_mem_unitary [nontrivial E] {U : E} (hU : U ∈ unitary E) : ∥U∥ = 1 := +norm_coe_unitary ⟨U, hU⟩ + +@[simp] lemma norm_coe_unitary_mul (U : unitary E) (A : E) : ∥(U : E) * A∥ = ∥A∥ := +begin + by_cases h_nontriv : ∃ (x y : E), x ≠ y, + { haveI : nontrivial E := ⟨h_nontriv⟩, + refine le_antisymm _ _, + { calc _ ≤ ∥(U : E)∥ * ∥A∥ : norm_mul_le _ _ + ... = ∥A∥ : by rw [norm_coe_unitary, one_mul] }, + { calc ∥A∥ = ∥(U : E)⋆ * U * A∥ : by { nth_rewrite_lhs 0 [←one_mul A], + rw [←unitary.coe_star_mul_self U, mul_assoc] } + ... ≤ ∥(U : E)⋆∥ * ∥(U : E) * A∥ : by { rw [mul_assoc], exact norm_mul_le _ _ } + ... = ∥(U : E) * A∥ : by simp only [one_mul, norm_coe_unitary, norm_star] } }, + { push_neg at h_nontriv, + rw [h_nontriv (U * A)] } +end + +@[simp] lemma norm_unitary_smul (U : unitary E) (A : E) : ∥U • A∥ = ∥A∥ := +norm_coe_unitary_mul U A + +lemma norm_mem_unitary_mul {U : E} (A : E) (hU : U ∈ unitary E) : ∥U * A∥ = ∥A∥ := +norm_coe_unitary_mul ⟨U, hU⟩ A + +@[simp] lemma norm_mul_coe_unitary (A : E) (U : unitary E) : ∥A * U∥ = ∥A∥ := +calc _ = ∥star (star (U : E) * star A)∥ : by simp only [star_star, star_mul] + ... = ∥star (U : E) * star A∥ : by rw [norm_star] + ... = ∥star A∥ : norm_mem_unitary_mul (star A) (unitary.star_mem U.prop) + ... = ∥A∥ : norm_star + +lemma norm_mul_mem_unitary (A : E) {U : E} (hU : U ∈ unitary E) : ∥A * U∥ = ∥A∥ := +norm_mul_coe_unitary A ⟨U, hU⟩ + end cstar_ring section starₗᵢ diff --git a/src/linear_algebra/unitary_group.lean b/src/linear_algebra/unitary_group.lean index 53f0670402215..50b9743daa1ed 100644 --- a/src/linear_algebra/unitary_group.lean +++ b/src/linear_algebra/unitary_group.lean @@ -5,6 +5,7 @@ Authors: Shing Tak Lam -/ import linear_algebra.matrix.to_lin import linear_algebra.matrix.nonsingular_inverse +import algebra.star.unitary /-! # The Unitary Group @@ -35,22 +36,6 @@ matrix group, group, unitary group, orthogonal group universes u v -section - -variables (M : Type v) [monoid M] [star_monoid M] - -/-- -In a `star_monoid M`, `unitary_submonoid M` is the submonoid consisting of all the elements of -`M` such that `star A * A = 1`. --/ -def unitary_submonoid : submonoid M := -{ carrier := {A | star A * A = 1}, - one_mem' := by simp, - mul_mem' := λ A B (hA : star A * A = 1) (hB : star B * B = 1), show star (A * B) * (A * B) = 1, - by rwa [star_mul, ←mul_assoc, mul_assoc _ _ A, hA, mul_one] } - -end - namespace matrix open linear_map open_locale matrix @@ -63,27 +48,13 @@ variables (α : Type v) [comm_ring α] [star_ring α] /-- `unitary_group n` is the group of `n` by `n` matrices where the star-transpose is the inverse. -/ -@[derive monoid] -def unitary_group : Type* := unitary_submonoid (matrix n n α) +abbreviation unitary_group := unitary (matrix n n α) end variables {n : Type u} [decidable_eq n] [fintype n] variables {α : Type v} [comm_ring α] [star_ring α] -namespace unitary_submonoid - -lemma star_mem {A : matrix n n α} (h : A ∈ unitary_submonoid (matrix n n α)) : - star A ∈ unitary_submonoid (matrix n n α) := -mul_eq_one_comm.mp $ (star_star A).symm ▸ h - -@[simp] -lemma star_mem_iff {A : matrix n n α} : - star A ∈ unitary_submonoid (matrix n n α) ↔ A ∈ unitary_submonoid (matrix n n α) := -⟨λ ha, star_star A ▸ star_mem ha, star_mem⟩ - -end unitary_submonoid - namespace unitary_group instance coe_matrix : has_coe (unitary_group n α) (matrix n n α) := ⟨subtype.val⟩ @@ -105,18 +76,8 @@ subtype.ext_iff_val.trans ⟨(λ h i j, congr_fun (congr_fun h i) j), matrix.ext @[ext] lemma ext (A B : unitary_group n α) : (∀ i j, A i j = B i j) → A = B := (unitary_group.ext_iff A B).mpr -instance : has_inv (unitary_group n α) := -⟨λ A, ⟨star A.1, unitary_submonoid.star_mem_iff.mpr A.2⟩⟩ - -instance : star_monoid (unitary_group n α) := -{ star := λ A, ⟨star A.1, unitary_submonoid.star_mem A.2⟩, - star_involutive := λ A, subtype.ext $ star_star A.1, - star_mul := λ A B, subtype.ext $ star_mul A.1 B.1 } - @[simp] -lemma star_mul_self (A : unitary_group n α) : star A ⬝ A = 1 := A.2 - -instance : inhabited (unitary_group n α) := ⟨1⟩ +lemma star_mul_self (A : unitary_group n α) : star A ⬝ A = 1 := A.2.1 section coe_lemmas @@ -144,21 +105,16 @@ matrix.to_lin'_one end coe_lemmas -instance : group (unitary_group n α) := -{ mul_left_inv := λ A, subtype.eq A.2, - ..unitary_group.has_inv, - ..unitary_group.monoid n α } - /-- `to_linear_equiv A` is matrix multiplication of vectors by `A`, as a linear equivalence. -/ def to_linear_equiv (A : unitary_group n α) : (n → α) ≃ₗ[α] (n → α) := -{ inv_fun := A⁻¹.to_lin', +{ inv_fun := to_lin' A⁻¹, left_inv := λ x, calc - A⁻¹.to_lin'.comp A.to_lin' x - = (A⁻¹ * A).to_lin' x : by rw [←to_lin'_mul] + (to_lin' A⁻¹).comp (to_lin' A) x + = (to_lin' (A⁻¹ * A)) x : by rw [←to_lin'_mul] ... = x : by rw [mul_left_inv, to_lin'_one, id_apply], right_inv := λ x, calc - A.to_lin'.comp A⁻¹.to_lin' x - = (A * A⁻¹).to_lin' x : by rw [←to_lin'_mul] + (to_lin' A).comp (to_lin' A⁻¹) x + = to_lin' (A * A⁻¹) x : by rw [←to_lin'_mul] ... = x : by rw [mul_right_inv, to_lin'_one, id_apply], ..matrix.to_lin' A } @@ -167,7 +123,7 @@ def to_GL (A : unitary_group n α) : general_linear_group α (n → α) := general_linear_group.of_linear_equiv (to_linear_equiv A) lemma coe_to_GL (A : unitary_group n α) : - ↑(to_GL A) = A.to_lin' := + ↑(to_GL A) = to_lin' A := rfl @[simp]