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).

Note

See SymmetricAlgebra instead if you are looking for the symmetric algebra of a module.

References

• [Hanche-Olsen and Størmer, Jordan Operator Algebras][hancheolsenstormer1984]

def SymAlg (α : Type u_1) : Type u_1

The symmetrized algebra (denoted as αˢʸᵐ) has the same underlying space as the original algebra α.

def «term_ˢʸᵐ» : Lean.TrailingParserDescr

The symmetrized algebra (denoted as αˢʸᵐ) has the same underlying space as the original algebra α.

@[match_pattern]

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

The element of SymAlg α that represents a : α.

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

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

@[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 αˢʸᵐ

@[implicit_reducible]

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

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance SymAlg.instInv {α : Type u_1} [Inv α] : Inv αˢʸᵐ

@[implicit_reducible]

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

@[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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

@[implicit_reducible]

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

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