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

def SymAlg (α : Type u_1) : Type u_1

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

Equations

• αˢʸᵐ = α

def «term_ˢʸᵐ» : Lean.TrailingParserDescr

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

Equations

• «term_ˢʸᵐ» = Lean.ParserDescr.trailingNode `«term_ˢʸᵐ» 1024 1024 (Lean.ParserDescr.symbol "ˢʸᵐ")

@[match_pattern]

def SymAlg.sym {α : Type u_1} : α ≃ αˢʸᵐ

The element of SymAlg α that represents a : α.

Equations

• SymAlg.sym = Equiv.refl α

def SymAlg.unsym {α : Type u_1} : αˢʸᵐ ≃ α

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

Equations

• SymAlg.unsym = Equiv.refl αˢʸᵐ

@[simp]

theorem SymAlg.unsym_sym {α : Type u_1} (a : α) : unsym (sym a) = a

@[simp]

theorem SymAlg.sym_unsym {α : Type u_1} (a : α) : sym (unsym a) = a

@[simp]

theorem SymAlg.sym_comp_unsym {α : Type u_1} : ⇑sym ∘ ⇑unsym = id

@[simp]

theorem SymAlg.unsym_comp_sym {α : Type u_1} : ⇑unsym ∘ ⇑sym = id

@[simp]

theorem SymAlg.sym_symm {α : Type u_1} : sym.symm = unsym

@[simp]

theorem SymAlg.unsym_symm {α : Type u_1} : unsym.symm = sym

theorem SymAlg.sym_bijective {α : Type u_1} : Function.Bijective ⇑sym

theorem SymAlg.unsym_bijective {α : Type u_1} : Function.Bijective ⇑unsym

theorem SymAlg.sym_injective {α : Type u_1} : Function.Injective ⇑sym

theorem SymAlg.sym_surjective {α : Type u_1} : Function.Surjective ⇑sym

theorem SymAlg.unsym_injective {α : Type u_1} : Function.Injective ⇑unsym

theorem SymAlg.unsym_surjective {α : Type u_1} : Function.Surjective ⇑unsym

theorem SymAlg.sym_inj {α : Type u_1} {a b : α} : sym a = sym b ↔ a = b

theorem SymAlg.unsym_inj {α : Type u_1} {a b : αˢʸᵐ} : unsym a = unsym b ↔ a = b

instance SymAlg.instNontrivial {α : Type u_1} [Nontrivial α] : Nontrivial αˢʸᵐ

instance SymAlg.instInhabited {α : Type u_1} [Inhabited α] : Inhabited αˢʸᵐ

Equations

• SymAlg.instInhabited = { default := SymAlg.sym default }

instance SymAlg.instSubsingleton {α : Type u_1} [Subsingleton α] : Subsingleton αˢʸᵐ

instance SymAlg.instUnique {α : Type u_1} [Unique α] : Unique αˢʸᵐ

Equations

• SymAlg.instUnique = Unique.mk' αˢʸᵐ

instance SymAlg.instIsEmpty {α : Type u_1} [IsEmpty α] : IsEmpty αˢʸᵐ

instance SymAlg.instOne {α : Type u_1} [One α] : One αˢʸᵐ

Equations

• SymAlg.instOne = { one := SymAlg.sym 1 }

instance SymAlg.instZero {α : Type u_1} [Zero α] : Zero αˢʸᵐ

Equations

• SymAlg.instZero = { zero := SymAlg.sym 0 }

instance SymAlg.instAdd {α : Type u_1} [Add α] : Add αˢʸᵐ

Equations

• SymAlg.instAdd = { add := fun (a b : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a + SymAlg.unsym b) }

instance SymAlg.instSub {α : Type u_1} [Sub α] : Sub αˢʸᵐ

Equations

• SymAlg.instSub = { sub := fun (a b : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a - SymAlg.unsym b) }

instance SymAlg.instNeg {α : Type u_1} [Neg α] : Neg αˢʸᵐ

Equations

• SymAlg.instNeg = { neg := fun (a : αˢʸᵐ) => SymAlg.sym (-SymAlg.unsym a) }

instance SymAlg.instMulOfAddOfInvertibleOfNat {α : Type u_1} [Add α] [Mul α] [One α] [OfNat α 2] [Invertible 2] : Mul αˢʸᵐ

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 α] : Inv αˢʸᵐ

Equations

• SymAlg.instInv = { inv := fun (a : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a)⁻¹ }

instance SymAlg.instSMul {α : Type u_1} (R : Type u_2) [SMul R α] : SMul R αˢʸᵐ

Equations

• SymAlg.instSMul R = { smul := fun (r : R) (a : αˢʸᵐ) => SymAlg.sym (r • SymAlg.unsym a) }

@[simp]

theorem SymAlg.sym_one {α : Type u_1} [One α] : sym 1 = 1

@[simp]

theorem SymAlg.sym_zero {α : Type u_1} [Zero α] : sym 0 = 0

@[simp]

theorem SymAlg.unsym_one {α : Type u_1} [One α] : unsym 1 = 1

@[simp]

theorem SymAlg.unsym_zero {α : Type u_1} [Zero α] : unsym 0 = 0

@[simp]

theorem SymAlg.sym_add {α : Type u_1} [Add α] (a b : α) : sym (a + b) = sym a + sym b

@[simp]

theorem SymAlg.unsym_add {α : Type u_1} [Add α] (a b : αˢʸᵐ) : unsym (a + b) = unsym a + unsym b

@[simp]

theorem SymAlg.sym_sub {α : Type u_1} [Sub α] (a b : α) : sym (a - b) = sym a - sym b

@[simp]

theorem SymAlg.unsym_sub {α : Type u_1} [Sub α] (a b : αˢʸᵐ) : unsym (a - b) = unsym a - unsym b

@[simp]

theorem SymAlg.sym_neg {α : Type u_1} [Neg α] (a : α) : sym (-a) = -sym a

@[simp]

theorem SymAlg.unsym_neg {α : Type u_1} [Neg α] (a : αˢʸᵐ) : unsym (-a) = -unsym a

theorem SymAlg.mul_def {α : Type u_1} [Add α] [Mul α] [One α] [OfNat α 2] [Invertible 2] (a b : αˢʸᵐ) : a * b = sym (⅟2 * (unsym a * unsym b + unsym b * unsym a))

theorem SymAlg.unsym_mul {α : Type u_1} [Mul α] [Add α] [One α] [OfNat α 2] [Invertible 2] (a b : αˢʸᵐ) : unsym (a * b) = ⅟2 * (unsym a * unsym b + unsym b * unsym a)

theorem SymAlg.sym_mul_sym {α : Type u_1} [Mul α] [Add α] [One α] [OfNat α 2] [Invertible 2] (a b : α) : sym a * sym b = sym (⅟2 * (a * b + b * a))

@[simp]

theorem SymAlg.sym_inv {α : Type u_1} [Inv α] (a : α) : sym a⁻¹ = (sym a)⁻¹

@[simp]

theorem SymAlg.unsym_inv {α : Type u_1} [Inv α] (a : αˢʸᵐ) : unsym a⁻¹ = (unsym a)⁻¹

@[simp]

theorem SymAlg.sym_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : α) : sym (c • a) = c • sym a

@[simp]

theorem SymAlg.unsym_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : αˢʸᵐ) : unsym (c • a) = c • unsym a

@[simp]

theorem SymAlg.unsym_eq_one_iff {α : Type u_1} [One α] (a : αˢʸᵐ) : unsym a = 1 ↔ a = 1

@[simp]

theorem SymAlg.unsym_eq_zero_iff {α : Type u_1} [Zero α] (a : αˢʸᵐ) : unsym a = 0 ↔ a = 0

@[simp]

theorem SymAlg.sym_eq_one_iff {α : Type u_1} [One α] (a : α) : sym a = 1 ↔ a = 1

@[simp]

theorem SymAlg.sym_eq_zero_iff {α : Type u_1} [Zero α] (a : α) : sym a = 0 ↔ a = 0

theorem SymAlg.unsym_ne_one_iff {α : Type u_1} [One α] (a : αˢʸᵐ) : unsym a ≠ 1 ↔ a ≠ 1

theorem SymAlg.unsym_ne_zero_iff {α : Type u_1} [Zero α] (a : αˢʸᵐ) : unsym a ≠ 0 ↔ a ≠ 0

theorem SymAlg.sym_ne_one_iff {α : Type u_1} [One α] (a : α) : sym a ≠ 1 ↔ a ≠ 1

theorem SymAlg.sym_ne_zero_iff {α : Type u_1} [Zero α] (a : α) : sym a ≠ 0 ↔ a ≠ 0

instance SymAlg.addCommSemigroup {α : Type u_1} [AddCommSemigroup α] : AddCommSemigroup αˢʸᵐ

Equations

• SymAlg.addCommSemigroup = Function.Injective.addCommSemigroup ⇑SymAlg.unsym ⋯ ⋯

instance SymAlg.addMonoid {α : Type u_1} [AddMonoid α] : AddMonoid αˢʸᵐ

Equations

• SymAlg.addMonoid = Function.Injective.addMonoid ⇑SymAlg.unsym ⋯ ⋯ ⋯ ⋯

instance SymAlg.addGroup {α : Type u_1} [AddGroup α] : AddGroup αˢʸᵐ

Equations

• SymAlg.addGroup = Function.Injective.addGroup ⇑SymAlg.unsym ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SymAlg.addCommMonoid {α : Type u_1} [AddCommMonoid α] : AddCommMonoid αˢʸᵐ

Equations

• SymAlg.addCommMonoid = AddCommMonoid.mk ⋯

instance SymAlg.addCommGroup {α : Type u_1} [AddCommGroup α] : AddCommGroup αˢʸᵐ

Equations

• SymAlg.addCommGroup = AddCommGroup.mk ⋯

instance SymAlg.instModule {α : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid α] [Module R α] : Module R αˢʸᵐ

Equations

• SymAlg.instModule = Function.Injective.module R { toFun := ⇑SymAlg.unsym, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance SymAlg.instInvertibleCoeEquivSym {α : Type u_1} [Mul α] [AddMonoidWithOne α] [Invertible 2] (a : α) [Invertible a] : Invertible (sym a)

Equations

• SymAlg.instInvertibleCoeEquivSym a = { invOf := SymAlg.sym ⅟a, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem SymAlg.invOf_sym {α : Type u_1} [Mul α] [AddMonoidWithOne α] [Invertible 2] (a : α) [Invertible a] : ⅟(sym a) = sym ⅟a

instance SymAlg.nonAssocSemiring {α : Type u_1} [Semiring α] [Invertible 2] : NonAssocSemiring αˢʸᵐ

Equations

• SymAlg.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance SymAlg.instNonAssocRingOfInvertibleOfNat {α : Type u_1} [Ring α] [Invertible 2] : NonAssocRing αˢʸᵐ

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

Equations

• SymAlg.instNonAssocRingOfInvertibleOfNat = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

The squaring operation coincides for both multiplications

theorem SymAlg.unsym_mul_self {α : Type u_1} [Semiring α] [Invertible 2] (a : αˢʸᵐ) : unsym (a * a) = unsym a * unsym a

theorem SymAlg.sym_mul_self {α : Type u_1} [Semiring α] [Invertible 2] (a : α) : sym (a * a) = sym a * sym a

theorem SymAlg.mul_comm {α : Type u_1} [Mul α] [AddCommSemigroup α] [One α] [OfNat α 2] [Invertible 2] (a b : αˢʸᵐ) : a * b = b * a

instance SymAlg.instCommMagmaOfInvertibleOfNat {α : Type u_1} [Ring α] [Invertible 2] : CommMagma αˢʸᵐ

Equations

• SymAlg.instCommMagmaOfInvertibleOfNat = CommMagma.mk ⋯

instance SymAlg.instIsCommJordan {α : Type u_1} [Ring α] [Invertible 2] : IsCommJordan αˢʸᵐ