Documentation

Mathlib.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 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 #

def SymAlg (α : Type u_1) :
Type u_1

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

Equations
Instances For
    @[match_pattern]
    def SymAlg.sym {α : Type u_1} :

    The element of SymAlg α that represents a : α.

    Equations
    Instances For
      def SymAlg.unsym {α : Type u_1} :

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

      Equations
      Instances For
        @[simp]
        theorem SymAlg.unsym_sym {α : Type u_1} (a : α) :
        SymAlg.unsym (SymAlg.sym a) = a
        @[simp]
        theorem SymAlg.sym_unsym {α : Type u_1} (a : α) :
        SymAlg.sym (SymAlg.unsym a) = a
        @[simp]
        theorem SymAlg.sym_comp_unsym {α : Type u_1} :
        SymAlg.sym SymAlg.unsym = id
        @[simp]
        theorem SymAlg.unsym_comp_sym {α : Type u_1} :
        SymAlg.unsym SymAlg.sym = id
        @[simp]
        theorem SymAlg.sym_symm {α : Type u_1} :
        SymAlg.sym.symm = SymAlg.unsym
        @[simp]
        theorem SymAlg.unsym_symm {α : Type u_1} :
        SymAlg.unsym.symm = SymAlg.sym
        theorem SymAlg.sym_bijective {α : Type u_1} :
        Function.Bijective SymAlg.sym
        theorem SymAlg.unsym_bijective {α : Type u_1} :
        Function.Bijective SymAlg.unsym
        theorem SymAlg.sym_injective {α : Type u_1} :
        Function.Injective SymAlg.sym
        theorem SymAlg.sym_surjective {α : Type u_1} :
        Function.Surjective SymAlg.sym
        theorem SymAlg.unsym_injective {α : Type u_1} :
        Function.Injective SymAlg.unsym
        theorem SymAlg.unsym_surjective {α : Type u_1} :
        Function.Surjective SymAlg.unsym
        theorem SymAlg.sym_inj {α : Type u_1} {a : α} {b : α} :
        SymAlg.sym a = SymAlg.sym b a = b
        theorem SymAlg.unsym_inj {α : Type u_1} {a : αˢʸᵐ} {b : αˢʸᵐ} :
        SymAlg.unsym a = SymAlg.unsym b a = b
        Equations
        • =
        Equations
        • SymAlg.instInhabited = { default := SymAlg.sym default }
        Equations
        • =
        instance SymAlg.instUnique {α : Type u_1} [Unique α] :
        Equations
        instance SymAlg.instIsEmpty {α : Type u_1} [IsEmpty α] :
        Equations
        • =
        instance SymAlg.instZero {α : Type u_1} [Zero α] :
        Equations
        • SymAlg.instZero = { zero := SymAlg.sym 0 }
        instance SymAlg.instOne {α : Type u_1} [One α] :
        Equations
        • SymAlg.instOne = { one := SymAlg.sym 1 }
        instance SymAlg.instAdd {α : Type u_1} [Add α] :
        Equations
        • SymAlg.instAdd = { add := fun (a b : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a + SymAlg.unsym b) }
        instance SymAlg.instSub {α : Type u_1} [Sub α] :
        Equations
        • SymAlg.instSub = { sub := fun (a b : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a - SymAlg.unsym b) }
        instance SymAlg.instNeg {α : Type u_1} [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] :
        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 α] :
        Equations
        • SymAlg.instInv = { inv := fun (a : αˢʸᵐ) => SymAlg.sym (SymAlg.unsym a)⁻¹ }
        instance SymAlg.instSMul {α : Type u_1} (R : Type u_2) [SMul R α] :
        Equations
        @[simp]
        theorem SymAlg.sym_zero {α : Type u_1} [Zero α] :
        SymAlg.sym 0 = 0
        @[simp]
        theorem SymAlg.sym_one {α : Type u_1} [One α] :
        SymAlg.sym 1 = 1
        @[simp]
        theorem SymAlg.unsym_zero {α : Type u_1} [Zero α] :
        SymAlg.unsym 0 = 0
        @[simp]
        theorem SymAlg.unsym_one {α : Type u_1} [One α] :
        SymAlg.unsym 1 = 1
        @[simp]
        theorem SymAlg.sym_add {α : Type u_1} [Add α] (a : α) (b : α) :
        SymAlg.sym (a + b) = SymAlg.sym a + SymAlg.sym b
        @[simp]
        theorem SymAlg.unsym_add {α : Type u_1} [Add α] (a : αˢʸᵐ) (b : αˢʸᵐ) :
        SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b
        @[simp]
        theorem SymAlg.sym_sub {α : Type u_1} [Sub α] (a : α) (b : α) :
        SymAlg.sym (a - b) = SymAlg.sym a - SymAlg.sym b
        @[simp]
        theorem SymAlg.unsym_sub {α : Type u_1} [Sub α] (a : αˢʸᵐ) (b : αˢʸᵐ) :
        SymAlg.unsym (a - b) = SymAlg.unsym a - SymAlg.unsym b
        @[simp]
        theorem SymAlg.sym_neg {α : Type u_1} [Neg α] (a : α) :
        SymAlg.sym (-a) = -SymAlg.sym a
        @[simp]
        theorem SymAlg.unsym_neg {α : Type u_1} [Neg α] (a : αˢʸᵐ) :
        SymAlg.unsym (-a) = -SymAlg.unsym a
        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))
        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)
        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))
        @[simp]
        theorem SymAlg.sym_inv {α : Type u_1} [Inv α] (a : α) :
        SymAlg.sym a⁻¹ = (SymAlg.sym a)⁻¹
        @[simp]
        theorem SymAlg.unsym_inv {α : Type u_1} [Inv α] (a : αˢʸᵐ) :
        SymAlg.unsym a⁻¹ = (SymAlg.unsym a)⁻¹
        @[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
        @[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
        @[simp]
        theorem SymAlg.unsym_eq_zero_iff {α : Type u_1} [Zero α] (a : αˢʸᵐ) :
        SymAlg.unsym a = 0 a = 0
        @[simp]
        theorem SymAlg.unsym_eq_one_iff {α : Type u_1} [One α] (a : αˢʸᵐ) :
        SymAlg.unsym a = 1 a = 1
        @[simp]
        theorem SymAlg.sym_eq_zero_iff {α : Type u_1} [Zero α] (a : α) :
        SymAlg.sym a = 0 a = 0
        @[simp]
        theorem SymAlg.sym_eq_one_iff {α : Type u_1} [One α] (a : α) :
        SymAlg.sym a = 1 a = 1
        theorem SymAlg.unsym_ne_zero_iff {α : Type u_1} [Zero α] (a : αˢʸᵐ) :
        SymAlg.unsym a 0 a 0
        theorem SymAlg.unsym_ne_one_iff {α : Type u_1} [One α] (a : αˢʸᵐ) :
        SymAlg.unsym a 1 a 1
        theorem SymAlg.sym_ne_zero_iff {α : Type u_1} [Zero α] (a : α) :
        SymAlg.sym a 0 a 0
        theorem SymAlg.sym_ne_one_iff {α : Type u_1} [One α] (a : α) :
        SymAlg.sym a 1 a 1
        Equations
        instance SymAlg.addMonoid {α : Type u_1} [AddMonoid α] :
        Equations
        instance SymAlg.addGroup {α : Type u_1} [AddGroup α] :
        Equations
        Equations
        Equations
        instance SymAlg.instModule {α : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid α] [Module R α] :
        Equations
        instance SymAlg.instInvertibleCoeEquivSym {α : Type u_1} [Mul α] [AddMonoidWithOne α] [Invertible 2] (a : α) [Invertible a] :
        Invertible (SymAlg.sym a)
        Equations
        @[simp]
        theorem SymAlg.invOf_sym {α : Type u_1} [Mul α] [AddMonoidWithOne α] [Invertible 2] (a : α) [Invertible a] :
        (SymAlg.sym a) = SymAlg.sym a
        Equations

        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 : αˢʸᵐ) :
        SymAlg.unsym (a * a) = SymAlg.unsym a * SymAlg.unsym a
        theorem SymAlg.sym_mul_self {α : Type u_1} [Semiring α] [Invertible 2] (a : α) :
        SymAlg.sym (a * a) = SymAlg.sym a * SymAlg.sym a
        theorem SymAlg.mul_comm {α : Type u_1} [Mul α] [AddCommSemigroup α] [One α] [OfNat α 2] [Invertible 2] (a : αˢʸᵐ) (b : αˢʸᵐ) :
        a * b = b * a
        Equations
        Equations
        • =