feat(algebra/star/unitary): (re)define unitary elements of a star mon…

…oid (#11457)

This PR defines `unitary R` for a star monoid `R` as the submonoid containing the elements that satisfy both `star U * U = 1` and `U * star U = 1`. We show basic properties (i.e. that this forms a group) and show that they
preserve the norm when `R` is a C* ring.

Note that this replaces `unitary_submonoid`, which only included the condition `star U * U = 1` -- see [the discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/unitary.20submonoid) on Zulip.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

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 :=

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

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ₗᵢ

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]