mathlib documentation

algebra.symmetrized

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 sym_alg α, with notation αˢʸᵐ.

Implementation notes #

The approach taken here is inspired by algebra.opposites. We use Oxford Spellings (IETF en-GB-oxendict).

References #

def sym_alg.sym {α : Type u_1} :
α → αˢʸᵐ

The element of sym_alg α that represents a : α.

Equations
Instances for sym_alg.sym
def sym_alg.unsym {α : Type u_1} :
αˢʸᵐ → α

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

Equations
@[simp]
theorem sym_alg.unsym_sym {α : Type u_1} (a : α) :
@[simp]
theorem sym_alg.sym_unsym {α : Type u_1} (a : α) :
@[simp]
@[simp]
@[simp]
def sym_alg.sym_equiv {α : Type u_1} :

The canonical bijection between α and αˢʸᵐ.

Equations
@[simp]
theorem sym_alg.sym_inj {α : Type u_1} {a b : α} :
@[simp]
theorem sym_alg.unsym_inj {α : Type u_1} {a b : αˢʸᵐ} :
@[protected, instance]
def sym_alg.nontrivial {α : Type u_1} [nontrivial α] :
@[protected, instance]
def sym_alg.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected, instance]
def sym_alg.subsingleton {α : Type u_1} [subsingleton α] :
@[protected, instance]
def sym_alg.unique {α : Type u_1} [unique α] :
Equations
@[protected, instance]
def sym_alg.is_empty {α : Type u_1} [is_empty α] :
@[protected, instance]
def sym_alg.has_zero {α : Type u_1} [has_zero α] :
Equations
@[protected, instance]
def sym_alg.has_one {α : Type u_1} [has_one α] :
Equations
@[protected, instance]
def sym_alg.has_add {α : Type u_1} [has_add α] :
Equations
@[protected, instance]
def sym_alg.has_sub {α : Type u_1} [has_sub α] :
Equations
@[protected, instance]
def sym_alg.has_neg {α : Type u_1} [has_neg α] :
Equations
@[protected, instance]
def sym_alg.has_mul {α : Type u_1} [has_add α] [has_mul α] [has_one α] [invertible 2] :
Equations
@[protected, instance]
def sym_alg.has_inv {α : Type u_1} [has_inv α] :
Equations
@[protected, instance]
def sym_alg.has_scalar {α : Type u_1} (R : Type u_2) [has_scalar R α] :
Equations
@[simp]
theorem sym_alg.sym_one {α : Type u_1} [has_one α] :
@[simp]
theorem sym_alg.sym_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem sym_alg.unsym_one {α : Type u_1} [has_one α] :
@[simp]
theorem sym_alg.unsym_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem sym_alg.sym_add {α : Type u_1} [has_add α] (a b : α) :
@[simp]
theorem sym_alg.unsym_add {α : Type u_1} [has_add α] (a b : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_sub {α : Type u_1} [has_sub α] (a b : α) :
@[simp]
theorem sym_alg.unsym_sub {α : Type u_1} [has_sub α] (a b : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_neg {α : Type u_1} [has_neg α] (a : α) :
@[simp]
theorem sym_alg.unsym_neg {α : Type u_1} [has_neg α] (a : αˢʸᵐ) :
theorem sym_alg.mul_def {α : Type u_1} [has_add α] [has_mul α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
theorem sym_alg.unsym_mul {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
theorem sym_alg.sym_mul_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : α) :
@[simp]
theorem sym_alg.sym_inv {α : Type u_1} [has_inv α] (a : α) :
@[simp]
theorem sym_alg.unsym_inv {α : Type u_1} [has_inv α] (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_smul {α : Type u_1} {R : Type u_2} [has_scalar R α] (c : R) (a : α) :
@[simp]
theorem sym_alg.unsym_smul {α : Type u_1} {R : Type u_2} [has_scalar R α] (c : R) (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.unsym_eq_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.unsym_eq_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_eq_one_iff {α : Type u_1} [has_one α] (a : α) :
sym_alg.sym a = 1 a = 1
@[simp]
theorem sym_alg.sym_eq_zero_iff {α : Type u_1} [has_zero α] (a : α) :
sym_alg.sym a = 0 a = 0
theorem sym_alg.unsym_ne_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
theorem sym_alg.unsym_ne_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
theorem sym_alg.sym_ne_one_iff {α : Type u_1} [has_one α] (a : α) :
theorem sym_alg.sym_ne_zero_iff {α : Type u_1} [has_zero α] (a : α) :
@[protected, instance]
def sym_alg.add_monoid {α : Type u_1} [add_monoid α] :
Equations
@[protected, instance]
def sym_alg.add_group {α : Type u_1} [add_group α] :
Equations
@[protected, instance]
def sym_alg.module {α : Type u_1} {R : Type u_2} [semiring R] [add_comm_monoid α] [module R α] :
Equations
@[protected, instance]
def sym_alg.sym.invertible {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a : α) [invertible a] :
Equations
@[simp]
theorem sym_alg.inv_of_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a : α) [invertible a] :
@[protected, instance]
Equations
@[protected, instance]
def sym_alg.non_assoc_ring {α : Type u_1} [ring α] [invertible 2] :

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

Equations

The squaring operation coincides for both multiplications

theorem sym_alg.unsym_mul_self {α : Type u_1} [semiring α] [invertible 2] (a : αˢʸᵐ) :
theorem sym_alg.sym_mul_self {α : Type u_1} [semiring α] [invertible 2] (a : α) :
theorem sym_alg.mul_comm {α : Type u_1} [has_mul α] [add_comm_semigroup α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
a * b = b * a