Maximal self-adjoint subrings

This file introduces the IsMaximalSelfAdjoint R α typeclass, which records that the TrivialStar ring R carries the self-adjoint part of a star ring α. It bundles an additive, R-linear map selfadjMap : α →+ R that inverts algebraMap R α on self-adjoint elements. The guiding example is R = ℝ, α = ℂ: it lets a quantity such as the trace of a Hermitian matrix be valued in ℝ instead of ℂ, reflecting that physical observables are self-adjoint and take real expectation values.

class IsMaximalSelfAdjoint (R : outParam (Type u_1)) (α : Type u_2) [Star α] [Star R] [CommSemiring R] [Semiring α] [TrivialStar R] [Algebra R α] : Type (max u_1 u_2)

IsMaximalSelfAdjoint R α witnesses that R is the maximal TrivialStar subring of the star ring α, via an additive map selfadjMap : α →+ R collecting the self-adjoint part of each element. This lets HermitianMat.trace return 𝕜 when 𝕜 already has a trivial star, and the "clean" underlying type otherwise, e.g. ℝ when the input field is ℂ.

• selfadjMap : α →+ R

  The additive map sending an element of α to its self-adjoint part in R.

• selfadj_smul (r : R) (a : α) : selfadjMap (r • a) = r * selfadjMap a

  selfadjMap pulls scalar multiplication by R out of its argument.

• selfadj_algebra {a : α} : IsSelfAdjoint a → (algebraMap R α) (selfadjMap a) = a

  On self-adjoint elements, selfadjMap is a section of algebraMap R α.

@[implicit_reducible]

instance instTrivialStar_IsMaximalSelfAdjoint {R : Type u_1} [Star R] [TrivialStar R] [CommSemiring R] : IsMaximalSelfAdjoint R R

Every TrivialStar CommSemiring is its own maximal self adjoints.

Equations

• instTrivialStar_IsMaximalSelfAdjoint = { selfadjMap := AddMonoidHom.id R, selfadj_smul := ⋯, selfadj_algebra := ⋯ }

@[implicit_reducible]

instance instRCLike_IsMaximalSelfAdjoint {α : Type u_1} [RCLike α] : IsMaximalSelfAdjoint ℝ α

ℝ is the maximal self adjoint elements over RCLike

Equations

• instRCLike_IsMaximalSelfAdjoint = { selfadjMap := RCLike.re, selfadj_smul := ⋯, selfadj_algebra := ⋯ }

@[simp]

theorem IsMaximalSelfAdjoint.trivial_selfadjMap {R : Type u_1} [Star R] [TrivialStar R] [CommSemiring R] : selfadjMap = AddMonoidHom.id R

@[simp]

theorem IsMaximalSelfAdjoint.RCLike_selfadjMap {α : Type u_1} [RCLike α] : selfadjMap = RCLike.re