mathlib3 documentation

algebra.symmetrized

Symmetrized algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
def sym_alg (α : Type u_1) :
Type u_1

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

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

The element of sym_alg α that represents a : α.

Equations
source
def sym_alg.unsym {α : Type u_1} :
αˢʸᵐ ≃ α

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

Equations
source
@[simp]
theorem sym_alg.unsym_sym {α : Type u_1} (a : α) :
⇑sym_alg.unsym (⇑sym_alg.sym a) = a
source
@[simp]
theorem sym_alg.sym_unsym {α : Type u_1} (a : α) :
⇑sym_alg.sym (⇑sym_alg.unsym a) = a
source
@[simp]
theorem sym_alg.sym_comp_unsym {α : Type u_1} :
⇑sym_alg.sym ∘ ⇑sym_alg.unsym = id
source
@[simp]
theorem sym_alg.unsym_comp_sym {α : Type u_1} :
⇑sym_alg.unsym ∘ ⇑sym_alg.sym = id
source
@[simp]
theorem sym_alg.sym_symm {α : Type u_1} :
sym_alg.sym.symm = sym_alg.unsym
source
@[simp]
theorem sym_alg.unsym_symm {α : Type u_1} :
sym_alg.unsym.symm = sym_alg.sym
source
theorem sym_alg.sym_bijective {α : Type u_1} :
function.bijective ⇑sym_alg.sym
source
theorem sym_alg.unsym_bijective {α : Type u_1} :
function.bijective ⇑sym_alg.unsym
source
theorem sym_alg.sym_injective {α : Type u_1} :
function.injective ⇑sym_alg.sym
source
theorem sym_alg.sym_surjective {α : Type u_1} :
function.surjective ⇑sym_alg.sym
source
theorem sym_alg.unsym_injective {α : Type u_1} :
function.injective ⇑sym_alg.unsym
source
theorem sym_alg.unsym_surjective {α : Type u_1} :
function.surjective ⇑sym_alg.unsym
source
@[simp]
theorem sym_alg.sym_inj {α : Type u_1} {a b : α} :
⇑sym_alg.sym a = ⇑sym_alg.sym b ↔ a = b
source
@[simp]
theorem sym_alg.unsym_inj {α : Type u_1} {a b : αˢʸᵐ} :
⇑sym_alg.unsym a = ⇑sym_alg.unsym b ↔ a = b
source
@[protected, instance]
def sym_alg.nontrivial {α : Type u_1} [nontrivial α] :
nontrivial αˢʸᵐ
source
@[protected, instance]
def sym_alg.inhabited {α : Type u_1} [inhabited α] :
inhabited αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.subsingleton {α : Type u_1} [subsingleton α] :
subsingleton αˢʸᵐ
source
@[protected, instance]
def sym_alg.unique {α : Type u_1} [unique α] :
unique αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.is_empty {α : Type u_1} [is_empty α] :
is_empty αˢʸᵐ
source
@[protected, instance]
def sym_alg.has_zero {α : Type u_1} [has_zero α] :
has_zero αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_one {α : Type u_1} [has_one α] :
has_one αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_add {α : Type u_1} [has_add α] :
has_add αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_sub {α : Type u_1} [has_sub α] :
has_sub αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_neg {α : Type u_1} [has_neg α] :
has_neg αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_mul {α : Type u_1} [has_add α] [has_mul α] [has_one α] [invertible 2] :
has_mul αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_inv {α : Type u_1} [has_inv α] :
has_inv αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.has_smul {α : Type u_1} (R : Type u_2) [has_smul R α] :
has_smul R αˢʸᵐ
Equations
source
@[simp]
theorem sym_alg.sym_one {α : Type u_1} [has_one α] :
⇑sym_alg.sym 1 = 1
source
@[simp]
theorem sym_alg.sym_zero {α : Type u_1} [has_zero α] :
⇑sym_alg.sym 0 = 0
source
@[simp]
theorem sym_alg.unsym_one {α : Type u_1} [has_one α] :
⇑sym_alg.unsym 1 = 1
source
@[simp]
theorem sym_alg.unsym_zero {α : Type u_1} [has_zero α] :
⇑sym_alg.unsym 0 = 0
source
@[simp]
theorem sym_alg.sym_add {α : Type u_1} [has_add α] (a b : α) :
⇑sym_alg.sym (a + b) = ⇑sym_alg.sym a + ⇑sym_alg.sym b
source
@[simp]
theorem sym_alg.unsym_add {α : Type u_1} [has_add α] (a b : αˢʸᵐ) :
⇑sym_alg.unsym (a + b) = ⇑sym_alg.unsym a + ⇑sym_alg.unsym b
source
@[simp]
theorem sym_alg.sym_sub {α : Type u_1} [has_sub α] (a b : α) :
⇑sym_alg.sym (a - b) = ⇑sym_alg.sym a - ⇑sym_alg.sym b
source
@[simp]
theorem sym_alg.unsym_sub {α : Type u_1} [has_sub α] (a b : αˢʸᵐ) :
⇑sym_alg.unsym (a - b) = ⇑sym_alg.unsym a - ⇑sym_alg.unsym b
source
@[simp]
theorem sym_alg.sym_neg {α : Type u_1} [has_neg α] (a : α) :
⇑sym_alg.sym (-a) = -⇑sym_alg.sym a
source
@[simp]
theorem sym_alg.unsym_neg {α : Type u_1} [has_neg α] (a : αˢʸᵐ) :
⇑sym_alg.unsym (-a) = -⇑sym_alg.unsym a
source
theorem sym_alg.mul_def {α : Type u_1} [has_add α] [has_mul α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
a * b = ⇑sym_alg.sym (⅟ 2 * (⇑sym_alg.unsym a * ⇑sym_alg.unsym b + ⇑sym_alg.unsym b * ⇑sym_alg.unsym a))
source
theorem sym_alg.unsym_mul {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
⇑sym_alg.unsym (a * b) = ⅟ 2 * (⇑sym_alg.unsym a * ⇑sym_alg.unsym b + ⇑sym_alg.unsym b * ⇑sym_alg.unsym a)
source
theorem sym_alg.sym_mul_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : α) :
⇑sym_alg.sym a * ⇑sym_alg.sym b = ⇑sym_alg.sym (⅟ 2 * (a * b + b * a))
source
@[simp]
theorem sym_alg.sym_inv {α : Type u_1} [has_inv α] (a : α) :
⇑sym_alg.sym a⁻¹ = (⇑sym_alg.sym a)⁻¹
source
@[simp]
theorem sym_alg.unsym_inv {α : Type u_1} [has_inv α] (a : αˢʸᵐ) :
⇑sym_alg.unsym a⁻¹ = (⇑sym_alg.unsym a)⁻¹
source
@[simp]
theorem sym_alg.sym_smul {α : Type u_1} {R : Type u_2} [has_smul R α] (c : R) (a : α) :
⇑sym_alg.sym (c • a) = c • ⇑sym_alg.sym a
source
@[simp]
theorem sym_alg.unsym_smul {α : Type u_1} {R : Type u_2} [has_smul R α] (c : R) (a : αˢʸᵐ) :
⇑sym_alg.unsym (c • a) = c • ⇑sym_alg.unsym a
source
@[simp]
theorem sym_alg.unsym_eq_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
⇑sym_alg.unsym a = 1 ↔ a = 1
source
@[simp]
theorem sym_alg.unsym_eq_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
⇑sym_alg.unsym a = 0 ↔ a = 0
source
@[simp]
theorem sym_alg.sym_eq_one_iff {α : Type u_1} [has_one α] (a : α) :
⇑sym_alg.sym a = 1 ↔ a = 1
source
@[simp]
theorem sym_alg.sym_eq_zero_iff {α : Type u_1} [has_zero α] (a : α) :
⇑sym_alg.sym a = 0 ↔ a = 0
source
theorem sym_alg.unsym_ne_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
⇑sym_alg.unsym a ≠ 1 ↔ a ≠ 1
source
theorem sym_alg.unsym_ne_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
⇑sym_alg.unsym a ≠ 0 ↔ a ≠ 0
source
theorem sym_alg.sym_ne_one_iff {α : Type u_1} [has_one α] (a : α) :
⇑sym_alg.sym a ≠ 1 ↔ a ≠ 1
source
theorem sym_alg.sym_ne_zero_iff {α : Type u_1} [has_zero α] (a : α) :
⇑sym_alg.sym a ≠ 0 ↔ a ≠ 0
source
@[protected, instance]
def sym_alg.add_comm_semigroup {α : Type u_1} [add_comm_semigroup α] :
add_comm_semigroup αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.add_monoid {α : Type u_1} [add_monoid α] :
add_monoid αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.add_group {α : Type u_1} [add_group α] :
add_group αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.add_comm_monoid {α : Type u_1} [add_comm_monoid α] :
add_comm_monoid αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.add_comm_group {α : Type u_1} [add_comm_group α] :
add_comm_group αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.module {α : Type u_1} {R : Type u_2} [semiring R] [add_comm_monoid α] [module R α] :
module R αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.sym.invertible {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a : α) [invertible a] :
invertible (⇑sym_alg.sym a)
Equations
source
@[simp]
theorem sym_alg.inv_of_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a : α) [invertible a] :
⅟ (⇑sym_alg.sym a) = ⇑sym_alg.sym (⅟ a)
source
@[protected, instance]
def sym_alg.non_assoc_semiring {α : Type u_1} [semiring α] [invertible 2] :
non_assoc_semiring αˢʸᵐ
Equations
source
@[protected, instance]
def sym_alg.non_assoc_ring {α : Type u_1} [ring α] [invertible 2] :
non_assoc_ring αˢʸᵐ

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

Equations

The squaring operation coincides for both multiplications

source
theorem sym_alg.unsym_mul_self {α : Type u_1} [semiring α] [invertible 2] (a : αˢʸᵐ) :
⇑sym_alg.unsym (a * a) = ⇑sym_alg.unsym a * ⇑sym_alg.unsym a
source
theorem sym_alg.sym_mul_self {α : Type u_1} [semiring α] [invertible 2] (a : α) :
⇑sym_alg.sym (a * a) = ⇑sym_alg.sym a * ⇑sym_alg.sym a
source
theorem sym_alg.mul_comm {α : Type u_1} [has_mul α] [add_comm_semigroup α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
a * b = b * a
source
@[protected, instance]
def sym_alg.is_comm_jordan {α : Type u_1} [ring α] [invertible 2] :
is_comm_jordan αˢʸᵐ
Equations