# Symmetrized algebra #

A commutative multiplication on a real or complex space can be constructed from any multiplication by "symmetrization" i.e $$a \circ b = \frac{1}{2}(ab + ba)$$

We provide the symmetrized version of a type α as SymAlg α, with notation αˢʸᵐ.

## Implementation notes #

The approach taken here is inspired by Mathlib/Algebra/Opposites.lean. We use Oxford Spellings (IETF en-GB-oxendict).

## References #

• [Hanche-Olsen and Størmer, Jordan Operator Algebras][hancheolsenstormer1984]
def SymAlg (α : Type u_1) :
Type u_1

The symmetrized algebra has the same underlying space as the original algebra.

Equations
Instances For
Equations
Instances For
@[match_pattern]
def SymAlg.sym {α : Type u_1} :

The element of SymAlg α that represents a : α.

Equations
• SymAlg.sym =
Instances For
def SymAlg.unsym {α : Type u_1} :

The element of α represented by x : αˢʸᵐ.

Equations
• SymAlg.unsym =
Instances For
@[simp]
theorem SymAlg.unsym_sym {α : Type u_1} (a : α) :
SymAlg.unsym (SymAlg.sym a) = a
@[simp]
theorem SymAlg.sym_unsym {α : Type u_1} (a : α) :
SymAlg.sym (SymAlg.unsym a) = a
@[simp]
theorem SymAlg.sym_comp_unsym {α : Type u_1} :
SymAlg.sym SymAlg.unsym = id
@[simp]
theorem SymAlg.unsym_comp_sym {α : Type u_1} :
SymAlg.unsym SymAlg.sym = id
@[simp]
theorem SymAlg.sym_symm {α : Type u_1} :
SymAlg.sym.symm = SymAlg.unsym
@[simp]
theorem SymAlg.unsym_symm {α : Type u_1} :
SymAlg.unsym.symm = SymAlg.sym
theorem SymAlg.sym_bijective {α : Type u_1} :
Function.Bijective SymAlg.sym
theorem SymAlg.unsym_bijective {α : Type u_1} :
Function.Bijective SymAlg.unsym
theorem SymAlg.sym_injective {α : Type u_1} :
Function.Injective SymAlg.sym
theorem SymAlg.sym_surjective {α : Type u_1} :
Function.Surjective SymAlg.sym
theorem SymAlg.unsym_injective {α : Type u_1} :
Function.Injective SymAlg.unsym
theorem SymAlg.unsym_surjective {α : Type u_1} :
Function.Surjective SymAlg.unsym
theorem SymAlg.sym_inj {α : Type u_1} {a : α} {b : α} :
SymAlg.sym a = SymAlg.sym b a = b
theorem SymAlg.unsym_inj {α : Type u_1} {a : αˢʸᵐ} {b : αˢʸᵐ} :
SymAlg.unsym a = SymAlg.unsym b a = b
instance SymAlg.instNontrivial {α : Type u_1} [] :
Equations
• =
instance SymAlg.instInhabited {α : Type u_1} [] :
Equations
• SymAlg.instInhabited = { default := SymAlg.sym default }
instance SymAlg.instSubsingleton {α : Type u_1} [] :
Equations
• =
instance SymAlg.instUnique {α : Type u_1} [] :
Equations
• SymAlg.instUnique =
instance SymAlg.instIsEmpty {α : Type u_1} [] :
Equations
• =
instance SymAlg.instZero {α : Type u_1} [Zero α] :
Equations
• SymAlg.instZero = { zero := SymAlg.sym 0 }
instance SymAlg.instOne {α : Type u_1} [One α] :
Equations
• SymAlg.instOne = { one := SymAlg.sym 1 }
Equations
• SymAlg.instAdd = { add := fun (a b : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a + SymAlg.unsym b) }
instance SymAlg.instSub {α : Type u_1} [Sub α] :
Equations
• SymAlg.instSub = { sub := fun (a b : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a - SymAlg.unsym b) }
instance SymAlg.instNeg {α : Type u_1} [Neg α] :
Equations
• SymAlg.instNeg = { neg := fun (a : αˢʸᵐ) => SymAlg.sym (-SymAlg.unsym a) }
instance SymAlg.instMulOfAddOfInvertibleOfNat {α : Type u_1} [Add α] [Mul α] [One α] [OfNat α 2] [] :
Equations
• SymAlg.instMulOfAddOfInvertibleOfNat = { mul := fun (a b : αˢʸᵐ) => SymAlg.sym (2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)) }
instance SymAlg.instInv {α : Type u_1} [Inv α] :
Equations
• SymAlg.instInv = { inv := fun (a : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a)⁻¹ }
instance SymAlg.instSMul {α : Type u_1} (R : Type u_2) [SMul R α] :
Equations
• = { smul := fun (r : R) (a : αˢʸᵐ) => SymAlg.sym (r SymAlg.unsym a) }
@[simp]
theorem SymAlg.sym_zero {α : Type u_1} [Zero α] :
SymAlg.sym 0 = 0
@[simp]
theorem SymAlg.sym_one {α : Type u_1} [One α] :
SymAlg.sym 1 = 1
@[simp]
theorem SymAlg.unsym_zero {α : Type u_1} [Zero α] :
SymAlg.unsym 0 = 0
@[simp]
theorem SymAlg.unsym_one {α : Type u_1} [One α] :
SymAlg.unsym 1 = 1
@[simp]
theorem SymAlg.sym_add {α : Type u_1} [Add α] (a : α) (b : α) :
SymAlg.sym (a + b) = SymAlg.sym a + SymAlg.sym b
@[simp]
theorem SymAlg.unsym_add {α : Type u_1} [Add α] (a : αˢʸᵐ) (b : αˢʸᵐ) :
SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b
@[simp]
theorem SymAlg.sym_sub {α : Type u_1} [Sub α] (a : α) (b : α) :
SymAlg.sym (a - b) = SymAlg.sym a - SymAlg.sym b
@[simp]
theorem SymAlg.unsym_sub {α : Type u_1} [Sub α] (a : αˢʸᵐ) (b : αˢʸᵐ) :
SymAlg.unsym (a - b) = SymAlg.unsym a - SymAlg.unsym b
@[simp]
theorem SymAlg.sym_neg {α : Type u_1} [Neg α] (a : α) :
SymAlg.sym (-a) = -SymAlg.sym a
@[simp]
theorem SymAlg.unsym_neg {α : Type u_1} [Neg α] (a : αˢʸᵐ) :
SymAlg.unsym (-a) = -SymAlg.unsym a
theorem SymAlg.mul_def {α : Type u_1} [Add α] [Mul α] [One α] [OfNat α 2] [] (a : αˢʸᵐ) (b : αˢʸᵐ) :
a * b = SymAlg.sym (2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a))
theorem SymAlg.unsym_mul {α : Type u_1} [Mul α] [Add α] [One α] [OfNat α 2] [] (a : αˢʸᵐ) (b : αˢʸᵐ) :
SymAlg.unsym (a * b) = 2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)
theorem SymAlg.sym_mul_sym {α : Type u_1} [Mul α] [Add α] [One α] [OfNat α 2] [] (a : α) (b : α) :
SymAlg.sym a * SymAlg.sym b = SymAlg.sym (2 * (a * b + b * a))
@[simp]
theorem SymAlg.sym_inv {α : Type u_1} [Inv α] (a : α) :
SymAlg.sym a⁻¹ = (SymAlg.sym a)⁻¹
@[simp]
theorem SymAlg.unsym_inv {α : Type u_1} [Inv α] (a : αˢʸᵐ) :
SymAlg.unsym a⁻¹ = (SymAlg.unsym a)⁻¹
@[simp]
theorem SymAlg.sym_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : α) :
SymAlg.sym (c a) = c SymAlg.sym a
@[simp]
theorem SymAlg.unsym_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : αˢʸᵐ) :
SymAlg.unsym (c a) = c SymAlg.unsym a
@[simp]
theorem SymAlg.unsym_eq_zero_iff {α : Type u_1} [Zero α] (a : αˢʸᵐ) :
SymAlg.unsym a = 0 a = 0
@[simp]
theorem SymAlg.unsym_eq_one_iff {α : Type u_1} [One α] (a : αˢʸᵐ) :
SymAlg.unsym a = 1 a = 1
@[simp]
theorem SymAlg.sym_eq_zero_iff {α : Type u_1} [Zero α] (a : α) :
SymAlg.sym a = 0 a = 0
@[simp]
theorem SymAlg.sym_eq_one_iff {α : Type u_1} [One α] (a : α) :
SymAlg.sym a = 1 a = 1
theorem SymAlg.unsym_ne_zero_iff {α : Type u_1} [Zero α] (a : αˢʸᵐ) :
SymAlg.unsym a 0 a 0
theorem SymAlg.unsym_ne_one_iff {α : Type u_1} [One α] (a : αˢʸᵐ) :
SymAlg.unsym a 1 a 1
theorem SymAlg.sym_ne_zero_iff {α : Type u_1} [Zero α] (a : α) :
SymAlg.sym a 0 a 0
theorem SymAlg.sym_ne_one_iff {α : Type u_1} [One α] (a : α) :
SymAlg.sym a 1 a 1
instance SymAlg.addCommSemigroup {α : Type u_1} [] :
Equations
instance SymAlg.addMonoid {α : Type u_1} [] :
Equations
instance SymAlg.addGroup {α : Type u_1} [] :
Equations
instance SymAlg.addCommMonoid {α : Type u_1} [] :
Equations
instance SymAlg.addCommGroup {α : Type u_1} [] :
Equations
instance SymAlg.instModule {α : Type u_1} {R : Type u_2} [] [] [Module R α] :
Equations
instance SymAlg.instInvertibleCoeEquivSym {α : Type u_1} [Mul α] [] [] (a : α) [] :
Invertible (SymAlg.sym a)
Equations
• = { invOf := SymAlg.sym a, invOf_mul_self := , mul_invOf_self := }
@[simp]
theorem SymAlg.invOf_sym {α : Type u_1} [Mul α] [] [] (a : α) [] :
(SymAlg.sym a) = SymAlg.sym a
instance SymAlg.nonAssocSemiring {α : Type u_1} [] [] :
Equations
• SymAlg.nonAssocSemiring = let __src := SymAlg.addCommMonoid;
instance SymAlg.instNonAssocRingOfInvertibleOfNat {α : Type u_1} [Ring α] [] :

The symmetrization of a real (unital, associative) algebra is a non-associative ring.

Equations
• SymAlg.instNonAssocRingOfInvertibleOfNat = let __src := SymAlg.nonAssocSemiring; let __src_1 := SymAlg.addCommGroup; NonAssocRing.mk

The squaring operation coincides for both multiplications

theorem SymAlg.unsym_mul_self {α : Type u_1} [] [] (a : αˢʸᵐ) :
SymAlg.unsym (a * a) = SymAlg.unsym a * SymAlg.unsym a
theorem SymAlg.sym_mul_self {α : Type u_1} [] [] (a : α) :
SymAlg.sym (a * a) = SymAlg.sym a * SymAlg.sym a
theorem SymAlg.mul_comm {α : Type u_1} [Mul α] [] [One α] [OfNat α 2] [] (a : αˢʸᵐ) (b : αˢʸᵐ) :
a * b = b * a
instance SymAlg.instCommMagmaOfInvertibleOfNat {α : Type u_1} [Ring α] [] :
Equations
• SymAlg.instCommMagmaOfInvertibleOfNat =
instance SymAlg.instIsCommJordan {α : Type u_1} [Ring α] [] :
Equations
• =