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]

source

def SymAlg (α : Type u_1) :

Type u_1

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

Equations

αˢʸᵐ = α

Instances For

source

def «term_ˢʸᵐ» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[match_pattern]

def SymAlg.sym {α : Type u_1} :

α ≃ αˢʸᵐ

The element of SymAlg α that represents a : α.

Equations

SymAlg.sym = Equiv.refl α

Instances For

source

def SymAlg.unsym {α : Type u_1} :

αˢʸᵐ ≃ α

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

Equations

SymAlg.unsym = Equiv.refl αˢʸᵐ

Instances For

source

@[simp]

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

SymAlg.unsym (SymAlg.sym a) = a

source

@[simp]

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

SymAlg.sym (SymAlg.unsym a) = a

source

@[simp]

theorem SymAlg.sym_comp_unsym {α : Type u_1} :

⇑SymAlg.sym ∘ ⇑SymAlg.unsym = id

source

@[simp]

theorem SymAlg.unsym_comp_sym {α : Type u_1} :

⇑SymAlg.unsym ∘ ⇑SymAlg.sym = id

source

@[simp]

theorem SymAlg.sym_symm {α : Type u_1} :

SymAlg.sym.symm = SymAlg.unsym

source

@[simp]

theorem SymAlg.unsym_symm {α : Type u_1} :

SymAlg.unsym.symm = SymAlg.sym

source

theorem SymAlg.sym_bijective {α : Type u_1} :

Function.Bijective ⇑SymAlg.sym

source

theorem SymAlg.unsym_bijective {α : Type u_1} :

Function.Bijective ⇑SymAlg.unsym

source

theorem SymAlg.sym_injective {α : Type u_1} :

Function.Injective ⇑SymAlg.sym

source

theorem SymAlg.sym_surjective {α : Type u_1} :

Function.Surjective ⇑SymAlg.sym

source

theorem SymAlg.unsym_injective {α : Type u_1} :

Function.Injective ⇑SymAlg.unsym

source

theorem SymAlg.unsym_surjective {α : Type u_1} :

Function.Surjective ⇑SymAlg.unsym

source

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

SymAlg.sym a = SymAlg.sym b ↔ a = b

source

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

SymAlg.unsym a = SymAlg.unsym b ↔ a = b

source

instance SymAlg.instNontrivialSymAlg {α : Type u_1} [Nontrivial α] :

Nontrivial αˢʸᵐ

Equations

(_ : Nontrivial αˢʸᵐ) = (_ : Nontrivial αˢʸᵐ)

source

instance SymAlg.instInhabitedSymAlg {α : Type u_1} [Inhabited α] :

Inhabited αˢʸᵐ

Equations

SymAlg.instInhabitedSymAlg = { default := SymAlg.sym default }

source

instance SymAlg.instSubsingletonSymAlg {α : Type u_1} [Subsingleton α] :

Subsingleton αˢʸᵐ

Equations

(_ : Subsingleton αˢʸᵐ) = (_ : Subsingleton αˢʸᵐ)

source

instance SymAlg.instUniqueSymAlg {α : Type u_1} [Unique α] :

Unique αˢʸᵐ

Equations

SymAlg.instUniqueSymAlg = Unique.mk' αˢʸᵐ

source

instance SymAlg.instIsEmptySymAlg {α : Type u_1} [IsEmpty α] :

IsEmpty αˢʸᵐ

Equations

(_ : IsEmpty αˢʸᵐ) = (_ : IsEmpty αˢʸᵐ)

source

instance SymAlg.instZeroSymAlg {α : Type u_1} [Zero α] :

Zero αˢʸᵐ

Equations

SymAlg.instZeroSymAlg = { zero := SymAlg.sym 0 }

source

instance SymAlg.instOneSymAlg {α : Type u_1} [One α] :

One αˢʸᵐ

Equations

SymAlg.instOneSymAlg = { one := SymAlg.sym 1 }

source

instance SymAlg.instAddSymAlg {α : Type u_1} [Add α] :

Add αˢʸᵐ

Equations

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

source

instance SymAlg.instSubSymAlg {α : Type u_1} [Sub α] :

Sub αˢʸᵐ

Equations

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

source

instance SymAlg.instNegSymAlg {α : Type u_1} [Neg α] :

Neg αˢʸᵐ

Equations

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

source

instance SymAlg.instMulSymAlg {α : Type u_1} [Add α] [Mul α] [One α] [OfNat α 2] [Invertible 2] :

Mul αˢʸᵐ

Equations

SymAlg.instMulSymAlg = { mul := fun (a b : αˢʸᵐ) => SymAlg.sym (⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)) }

source

instance SymAlg.instInvSymAlg {α : Type u_1} [Inv α] :

Inv αˢʸᵐ

Equations

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

source

instance SymAlg.instSMulSymAlg {α : Type u_1} (R : Type u_2) [SMul R α] :

SMul R αˢʸᵐ

Equations

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

source

@[simp]

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

SymAlg.sym 0 = 0

source

@[simp]

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

SymAlg.sym 1 = 1

source

@[simp]

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

SymAlg.unsym 0 = 0

source

@[simp]

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

SymAlg.unsym 1 = 1

source

@[simp]

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

SymAlg.sym (a + b) = SymAlg.sym a + SymAlg.sym b

source

@[simp]

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

SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b

source

@[simp]

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

SymAlg.sym (a - b) = SymAlg.sym a - SymAlg.sym b

source

@[simp]

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

SymAlg.unsym (a - b) = SymAlg.unsym a - SymAlg.unsym b

source

@[simp]

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

SymAlg.sym (-a) = -SymAlg.sym a

source

@[simp]

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

SymAlg.unsym (-a) = -SymAlg.unsym a

source

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

a * b = SymAlg.sym (⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a))

source

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

SymAlg.unsym (a * b) = ⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)

source

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

SymAlg.sym a * SymAlg.sym b = SymAlg.sym (⅟2 * (a * b + b * a))

source

@[simp]

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

SymAlg.sym a⁻¹ = (SymAlg.sym a)⁻¹

source

@[simp]

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

SymAlg.unsym a⁻¹ = (SymAlg.unsym a)⁻¹

source

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

source

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

source

@[simp]

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

SymAlg.unsym a = 0 ↔ a = 0

source

@[simp]

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

SymAlg.unsym a = 1 ↔ a = 1

source

@[simp]

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

SymAlg.sym a = 0 ↔ a = 0

source

@[simp]

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

SymAlg.sym a = 1 ↔ a = 1

source

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

SymAlg.unsym a ≠ 0 ↔ a ≠ 0

source

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

SymAlg.unsym a ≠ 1 ↔ a ≠ 1

source

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

SymAlg.sym a ≠ 0 ↔ a ≠ 0

source

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

SymAlg.sym a ≠ 1 ↔ a ≠ 1

source

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

AddCommSemigroup αˢʸᵐ

Equations

SymAlg.addCommSemigroup = Function.Injective.addCommSemigroup ⇑SymAlg.unsym (_ : Function.Injective ⇑SymAlg.unsym) (_ : ∀ (a b : αˢʸᵐ), SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b)

source

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

AddMonoid αˢʸᵐ

Equations

One or more equations did not get rendered due to their size.

source

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

AddGroup αˢʸᵐ

Equations

One or more equations did not get rendered due to their size.

source

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

AddCommMonoid αˢʸᵐ

Equations

SymAlg.addCommMonoid = let src := SymAlg.addCommSemigroup; let src_1 := SymAlg.addMonoid; AddCommMonoid.mk (_ : ∀ (a b : αˢʸᵐ), a + b = b + a)

source

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

AddCommGroup αˢʸᵐ

Equations

SymAlg.addCommGroup = let src := SymAlg.addCommMonoid; let src_1 := SymAlg.addGroup; AddCommGroup.mk (_ : ∀ (a b : αˢʸᵐ), a + b = b + a)

source

instance SymAlg.instModuleSymAlgAddCommMonoid {α : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid α] [Module R α] :

Module R αˢʸᵐ

Equations

One or more equations did not get rendered due to their size.

source

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

Invertible (SymAlg.sym a)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

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

⅟(SymAlg.sym a) = SymAlg.sym ⅟a

source

instance SymAlg.nonAssocSemiring {α : Type u_1} [Semiring α] [Invertible 2] :

NonAssocSemiring αˢʸᵐ

Equations

SymAlg.nonAssocSemiring = let src := SymAlg.addCommMonoid; NonAssocSemiring.mk (_ : ∀ (x : αˢʸᵐ), 1 * x = x) (_ : ∀ (x : αˢʸᵐ), x * 1 = x)

source

instance SymAlg.instNonAssocRingSymAlg {α : Type u_1} [Ring α] [Invertible 2] :

NonAssocRing αˢʸᵐ

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

Equations

SymAlg.instNonAssocRingSymAlg = let src := SymAlg.nonAssocSemiring; let src_1 := SymAlg.addCommGroup; NonAssocRing.mk (_ : ∀ (a : αˢʸᵐ), 1 * a = a) (_ : ∀ (a : αˢʸᵐ), a * 1 = a)