English
The symmetrized algebra α^{sym} carries a (commutative) Jordan algebra structure when α is a ring with invertible 2.
Русский
Симметризованная алгебра α^{sym} обладает структурой коммутативной Джордановой алгебры, если α — кольцо с обратимостью 2.
LaTeX
$$IsCommJordan(α^{sym})$$
Lean4
instance [Ring α] [Invertible (2 : α)] : IsCommJordan αˢʸᵐ where
lmul_comm_rmul_rmul a
b :=
by
have commute_half_left := fun a : α =>
by
have := (Commute.one_left a).add_left (Commute.one_left a)
rw [one_add_one_eq_two] at this
exact this.invOf_left.eq
calc
a * b * (a * a)
_ =
sym
(⅟2 * ⅟2 *
(unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) +
unsym (a * a) * unsym a * unsym b +
unsym (a * a) * unsym b * unsym a)) :=
?_
_ =
sym
(⅟2 *
(unsym a * unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a)) :=
?_
_ = a * (b * (a * a)) :=
?_
-- Rearrange LHS
·
rw [mul_def, mul_def a b, unsym_sym, ← mul_assoc, ← commute_half_left (unsym (a * a)), mul_assoc, mul_assoc, ←
mul_add, ← mul_assoc, add_mul, mul_add (unsym (a * a)), ← add_assoc, ← mul_assoc, ← mul_assoc]
· rw [unsym_sym, sym_inj, ← mul_assoc, ← commute_half_left (unsym a), mul_assoc (⅟2) (unsym a),
mul_assoc (⅟2) _ (unsym a), ← mul_add, ← mul_assoc]
conv_rhs => rw [mul_add (unsym a)]
rw [add_mul, ← add_assoc, ← mul_assoc, ← mul_assoc]
rw [unsym_mul_self]
rw [← mul_assoc, ← mul_assoc, ← mul_assoc, ← mul_assoc, ← sub_eq_zero, ← mul_sub]
convert mul_zero (⅟(2 : α) * ⅟(2 : α))
rw [add_sub_add_right_eq_sub, add_assoc, add_assoc, add_sub_add_left_eq_sub, add_comm, add_sub_add_right_eq_sub,
sub_eq_zero]
-- Rearrange RHS
· rw [← mul_def, ← mul_def]
