feat(algebra/star/self_adjoint): define the self-adjoint elements of …

…a star additive group (#11135)

Given a type `R` with `[add_group R] [star_add_monoid R]`, we define `self_adjoint R` as the additive subgroup of self-adjoint elements, i.e. those such that `star x = x`. To avoid confusion, we move `is_self_adjoint` (which defines this to mean `⟪T x, y⟫ = ⟪x, T y⟫` in an inner product space) to the `inner_product_space` namespace.

docs/overview.yaml

@@ -179,7 +179,7 @@ Linear algebra:
     polar form of a quadratic: 'quadratic_form.polar'
   Finite-dimensional inner product spaces (see also Hilbert spaces, below):
     existence of orthonormal basis: 'orthonormal_basis'
-    diagonalization of self-adjoint endomorphisms: 'is_self_adjoint.diagonalization_basis_apply_self_apply'
+    diagonalization of self-adjoint endomorphisms: 'inner_product_space.is_self_adjoint.diagonalization_basis_apply_self_apply'
 
 Topology:
   General topology:
@@ -258,12 +258,12 @@ Analysis:
   Hilbert spaces:
     Inner product space, over $R$ or $C$: 'inner_product_space'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
-    self-adjoint endomorphism: 'is_self_adjoint'
+    self-adjoint endomorphism: 'inner_product_space.is_self_adjoint'
     orthogonal projection: 'orthogonal_projection'
     reflection: 'reflection'
     orthogonal complement: 'submodule.orthogonal'
     existence of Hilbert basis: 'exists_is_orthonormal_dense_span'
-    eigenvalues from Rayleigh quotient: 'is_self_adjoint.has_eigenvector_of_is_local_extr_on'
+    eigenvalues from Rayleigh quotient: 'inner_product_space.is_self_adjoint.has_eigenvector_of_is_local_extr_on'
     Fréchet-Riesz representation of the dual of a Hilbert space: 'inner_product_space.to_dual'
 
   Differentiability:

docs/undergrad.yaml

@@ -223,9 +223,9 @@ Bilinear and Quadratic Forms Over a Vector Space:
     unitary group: ''
     special orthogonal group: ''
     special unitary group: ''
-    self-adjoint endomorphism: 'is_self_adjoint'
+    self-adjoint endomorphism: 'inner_product_space.is_self_adjoint'
     normal endomorphism: 'https://en.wikipedia.org/wiki/Normal_operator'
-    diagonalization of a self-adjoint endomorphism: 'is_self_adjoint.diagonalization_basis_apply_self_apply'
+    diagonalization of a self-adjoint endomorphism: 'inner_product_space.is_self_adjoint.diagonalization_basis_apply_self_apply'
     diagonalization of normal endomorphisms: 'https://en.wikipedia.org/wiki/Spectral_theorem#Normal_matrices'
     simultaneous diagonalization of two real quadratic forms, with one positive-definite: 'https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_spectral#Formalisation_alg%C3%A9brique'
     decomposition of an orthogonal transformation as a product of reflections: 'linear_isometry_equiv.reflections_generate'

src/algebra/star/self_adjoint.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2021 Frédéric Dupuis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Frédéric Dupuis
+-/
+
+import algebra.star.basic
+import group_theory.subgroup.basic
+
+/-!
+# Self-adjoint elements of a star additive group
+
+This file defines `self_adjoint R`, where `R` is a star additive monoid, as the additive subgroup
+containing the elements that satisfy `star x = x`. This includes, for instance, Hermitian
+operators on Hilbert spaces.
+
+## TODO
+
+* If `R` is a `star_module R₂ R`, put a module structure on `self_adjoint R`. This would naturally
+  be a `module (self_adjoint R₂) (self_adjoint R)`, but doing this literally would be undesirable
+  since in the main case of interest (`R₂ = ℂ`) we want `module ℝ (self_adjoint R)` and not
+  `module (self_adjoint ℂ) (self_adjoint R)`. One way of doing this would be to add the typeclass
+  `[has_trivial_star R]`, of which `ℝ` would be an instance, and then add a
+  `[module R (self_adjoint E)]` instance whenever we have `[module R E] [has_trivial_star E]`.
+  Another one would be to define a `[star_invariant_scalars R E]` to express the fact that
+  `star (x • v) = x • star v`.
+
+* Define `λ z x, z * x * star z` (i.e. conjugation by `z`) as a monoid action of `R` on `R`
+  (similar to the existing `conj_act` for groups), and then state the fact that `self_adjoint R` is
+  invariant under it.
+
+-/
+
+variables (R : Type*)
+
+/-- The self-adjoint elements of a star additive group, as an additive subgroup. -/
+def self_adjoint [add_group R] [star_add_monoid R] : add_subgroup R :=
+{ carrier := {x | star x = x},
+  zero_mem' := star_zero R,
+  add_mem' := λ x y (hx : star x = x) (hy : star y = y),
+                show star (x + y) = x + y, by simp only [star_add x y, hx, hy],
+  neg_mem' := λ x (hx : star x = x), show star (-x) = -x, by simp only [hx, star_neg] }
+variables {R}
+
+namespace self_adjoint
+
+section add_group
+variables [add_group R] [star_add_monoid R]
+
+lemma mem_iff {x : R} : x ∈ self_adjoint R ↔ star x = x :=
+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
+
+end add_group
+
+instance [add_comm_group R] [star_add_monoid R] : add_comm_group (self_adjoint R) :=
+{ add_comm := add_comm,
+  ..add_subgroup.to_add_group (self_adjoint R) }
+
+section ring
+variables [ring R] [star_ring R]
+
+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
+
+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 :=
+by simp only [mem_iff, star_bit0, mem_iff.mp hx]
+
+lemma bit1_mem {x : R} (hx : x ∈ self_adjoint R) : bit1 x ∈ self_adjoint R :=
+by simp only [mem_iff, star_bit1, mem_iff.mp hx]
+
+lemma conjugate {x : R} (hx : x ∈ self_adjoint R) (z : R) : z * x * star z ∈ self_adjoint R :=
+by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, mul_assoc]
+
+lemma conjugate' {x : R} (hx : x ∈ self_adjoint R) (z : R) : star z * x * z ∈ self_adjoint R :=
+by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, mul_assoc]
+
+end ring
+
+section comm_ring
+variables [comm_ring R] [star_ring R]
+
+instance : has_mul (self_adjoint R) :=
+⟨λ x y, ⟨(x : R) * y, by simp only [mem_iff, star_mul', star_coe_eq]⟩⟩
+
+@[simp, norm_cast] lemma coe_mul (x y : self_adjoint R) :
+  (coe : self_adjoint R → R) (x * y) = (x : R) * y := rfl
+
+instance : comm_ring (self_adjoint R) :=
+{ mul_assoc := λ x y z, by { ext, exact mul_assoc _ _ _ },
+  one_mul := λ x, by { ext, simp only [coe_mul, one_mul, coe_one] },
+  mul_one := λ x, by { ext, simp only [mul_one, coe_mul, coe_one] },
+  mul_comm := λ x y, by { ext, exact mul_comm _ _ },
+  left_distrib := λ x y z, by { ext, exact left_distrib _ _ _ },
+  right_distrib := λ x y z, by { ext, exact right_distrib _ _ _ },
+  ..self_adjoint.add_comm_group,
+  ..self_adjoint.has_one,
+  ..self_adjoint.has_mul }
+
+end comm_ring
+
+section field
+
+variables [field R] [star_ring R]
+
+instance : field (self_adjoint R) :=
+{ inv :=  λ x, ⟨(x.val)⁻¹, by simp only [mem_iff, star_inv', star_coe_eq, subtype.val_eq_coe]⟩,
+  exists_pair_ne := ⟨0, 1, subtype.ne_of_val_ne zero_ne_one⟩,
+  mul_inv_cancel := λ x hx, by { ext, exact mul_inv_cancel (λ H, hx $ subtype.eq H) },
+  inv_zero := by { ext, exact inv_zero },
+  ..self_adjoint.comm_ring }
+
+@[simp, norm_cast] lemma coe_inv (x : self_adjoint R) :
+  (coe : self_adjoint R → R) (x⁻¹) = (x : R)⁻¹ := rfl
+
+end field
+
+end self_adjoint

src/analysis/inner_product_space/basic.lean

@@ -1918,7 +1918,7 @@ end orthogonal
 
 /-! ### Self-adjoint operators -/
 
-section is_self_adjoint
+namespace inner_product_space
 
 /-- A (not necessarily bounded) operator on an inner product space is self-adjoint, if for all
 `x`, `y`, we have `⟪T x, y⟫ = ⟪x, T y⟫`. -/
@@ -1958,4 +1958,4 @@ lemma is_self_adjoint.restrict_invariant {T : E →ₗ[𝕜] E} (hT : is_self_ad
   is_self_adjoint (T.restrict hV) :=
 λ v w, hT v w
 
-end is_self_adjoint
+end inner_product_space

src/analysis/inner_product_space/rayleigh.lean

@@ -85,6 +85,7 @@ by simp only [@cinfi_set _ _ _ _ rayleigh_quotient, T.image_rayleigh_eq_image_ra
 
 end continuous_linear_map
 
+namespace inner_product_space
 namespace is_self_adjoint
 
 section real
@@ -279,3 +280,4 @@ lemma subsingleton_of_no_eigenvalue_finite_dimensional
 end finite_dimensional
 
 end is_self_adjoint
+end inner_product_space

src/analysis/inner_product_space/spectrum.lean

@@ -52,6 +52,7 @@ local attribute [instance] fact_one_le_two_real
 open_locale big_operators complex_conjugate
 open module.End
 
+namespace inner_product_space
 namespace is_self_adjoint
 
 variables {T : E →ₗ[𝕜] E} (hT : is_self_adjoint T)
@@ -240,3 +241,4 @@ end
 end version2
 
 end is_self_adjoint
+end inner_product_space