Symmetrized product of a real algebra

Stream: maths

[Christopher Hoskin]

Hello,

I've defined a non-unital, non-associative ring as:

@[protect_proj, ancestor add_comm_group non_unital_non_assoc_semiring ]
class non_unital_non_assoc_ring (α : Type*) extends
  add_comm_group α, non_unital_non_assoc_semiring α

Given an algebra α over ℝ, I'm trying to show that α is am instance of non_unital_non_assoc_ring (forgetting about the unit) under symmetrized product:

a∘b = 1/2(a*b+b*a).

Inspired by how mathlib implements the opposite multiplication (algebra.opposites) I've defined:

def sym_alg (α : Type*) : Type* := α

postfix `ˢʸᵐ`:std.prec.max_plus := sym_alg

It's then possible to show

noncomputable instance (α : Type*) [semiring α] [algebra ℝ α] : non_unital_non_assoc_ring (sym_alg  α)

except that two fields that are tripping me up are neg and add_left_neg as α is a semiring not a ring (alternatively, if I make α a ring, then I can't prove left_distrib and right_distrib).

It's easy to show that if α is a add_comm_group then so is αˢʸᵐ:

instance {α : Type*} [add_comm_group α] : add_comm_group (αˢʸᵐ) := {
  zero := sym 0,
  add := λ a b, a+b,
  add_assoc := λ a b c : α, add_assoc a b c,
  add_comm := λ a b : α, add_comm a b,
  zero_add := λ a, zero_add (unsym a),
  add_zero := λ a, add_zero (unsym a),
  neg := λ a, sym ( -(unsym a)),
  add_left_neg := λ a, add_left_neg (unsym a),
}

I know that module.add_comm_monoid_to_add_comm_group exists, but I've been warned off doing

instance  ring_module_has_add_comm_group : add_comm_group α := module.add_comm_monoid_to_add_comm_group R

as it leads to diamonds.

I can write:

#check (module.add_comm_monoid_to_add_comm_group ℝ).neg -- add_comm_group.neg : ?M_1 → ?M_1

But not:

variables [semiring α] [algebra ℝ α]

variables (a:α)

#check (module.add_comm_monoid_to_add_comm_group ℝ).neg a -- invalid field notation, function 'add_comm_group.neg' does not have explicit argument with type (add_comm_group ...)

I've run out of ideas about how to proceed at this point. Any suggestions?

Thanks,

Christopher

[Kevin Buzzard]

Can you post a MWE of your original question with everything other than the neg and add_left_neg thrown in? My guess is that you can just define neg x to be (-1) \bub x. I'm just a bit confused about what the question is though, because if alpha is an add_comm_group then you already have neg. This is why I'm asking for something where I can see exactly what is being assumed.

[Christopher Hoskin]

Trying to do that... but now left_distrib has stopped working. I'm sure it was working earlier. I must have changed something, but I can't figure out what.

[Kevin Buzzard]

Maybe post what you have with sorried problems? But just one piece of code rather than all the fragments above.

[Christopher Hoskin]

I did try defining neg as you suggest, but got in a hopeless tangle trying to prove add_left_neg.

[Christopher Hoskin]

This is the best I can do at the moment:

import algebra.ring.basic
import algebra.lie.of_associative
import data.real.basic
set_option old_structure_cmd true

/-- A not-necessarily-unital, not-necessarily-associative ring. -/
@[protect_proj, ancestor add_comm_group non_unital_non_assoc_semiring ]
class non_unital_non_assoc_ring (α : Type*) extends
  add_comm_group α, non_unital_non_assoc_semiring α

variables {A : Type*}

def sym_alg (α : Type*) : Type* := α

postfix `ˢʸᵐ`:std.prec.max_plus := sym_alg

namespace sym_alg

variables {α : Type*}

/-- The element of `sym_alg α` that represents `a : α`. -/
@[pp_nodot]
def sym : α → αˢʸᵐ := id

/-- The element of `α` represented by `x : αᵐᵒᵖ`. -/
@[pp_nodot]
def unsym : αˢʸᵐ → α := id

@[simp] lemma unsym_sym (x : α) : unsym (sym x) = x := rfl
@[simp] lemma sym_unsym (x : α) : sym (unsym x) = x := rfl


instance [has_add α] : has_add αˢʸᵐ :=
{ add := λ a b, sym (unsym a + unsym b) }

@[simp] lemma sym_add [has_add α] (a b : α) : sym (a + b) = sym a + sym b := rfl
@[simp] lemma unsym_add [has_add α] (x y : αˢʸᵐ) : unsym (x + y) = unsym x + unsym y := rfl


instance [has_neg α] : has_neg αˢʸᵐ :=
{ neg := λ a, sym ( -(unsym a)) }

instance {R : Type*} [has_scalar R α] : has_scalar R αˢʸᵐ := {
  smul := λ r a, sym (r•(unsym a))
}


@[simp] lemma sym_smul {R : Type*} [has_scalar R α] (c : R) (a : α) : sym (c • a) = c • sym a := rfl

lemma add_smul (α : Type*) [ring α] [algebra ℝ α] (a:α) (r s : ℝ): (r+s)•a = (r•a +s•a)   :=
begin
  unfold algebra.smul_def',
  rw ← add_mul,
  simp only [map_add, ring_hom.to_fun_eq_coe],
end

lemma smul_add' (α : Type*) [ring α] [algebra ℝ α] (a b:α) (r : ℝ): r•(a+b) = r•a + r•b   :=
begin
  unfold algebra.smul_def',
  rw ← mul_add,
end


instance {α : Type*} [add_comm_group α] : add_comm_group (αˢʸᵐ) := {
  zero := sym 0,
  add := λ a b, a+b,
  add_assoc := λ a b c : α, add_assoc a b c,
  add_comm := λ a b : α, add_comm a b,
  zero_add := λ a, zero_add (unsym a),
  add_zero := λ a, add_zero (unsym a),
  neg := λ a, sym ( -(unsym a)),
  add_left_neg := λ a, add_left_neg (unsym a),
}


noncomputable instance (α : Type*) [semiring α] [algebra ℝ α] : non_unital_non_assoc_ring (αˢʸᵐ) := {
  zero := sym 0,
  add := λ a b, a+b,
  add_assoc := λ a b c : α, add_assoc a b c,
  add_comm := λ a b : α, add_comm a b,
  zero_add := λ a, zero_add (unsym a),
  add_zero := λ a, add_zero (unsym a),
  neg := λ a, sorry,
  add_left_neg := λ a, sorry,
  mul := λ a b, (sym ((1/2:ℝ)•(unsym(a)*unsym(b)+unsym(b)*unsym(a)))),
  zero_mul := λ _, by simp,
  mul_zero :=  λ _, by simp,
  left_distrib := λ a b c, sorry,
  right_distrib := λ a b c, sorry,
}



end sym_alg

[Thomas Browning]

This is awful, but it seems to work (assuming ring rather than semiring).

noncomputable instance (α : Type*) [ring α] [algebra ℝ α] : non_unital_non_assoc_ring (αˢʸᵐ) := {
  zero := sym 0,
  add := λ a b, a+b,
  add_assoc := λ a b c : α, add_assoc a b c,
  add_comm := λ a b : α, add_comm a b,
  zero_add := λ a, zero_add (unsym a),
  add_zero := λ a, add_zero (unsym a),
  neg := λ a, -a,
  add_left_neg := λ a, add_left_neg (unsym a),
  mul := λ a b, (sym ((1/2:ℝ)•(unsym(a)*unsym(b)+unsym(b)*unsym(a)))),
  zero_mul := λ _, by simp,
  mul_zero :=  λ _, by simp,
  left_distrib := λ a b c, begin
    change (1/2:ℝ)•(unsym(a)*(unsym(b)+unsym(c))+(unsym(b)+unsym(c))*unsym(a)) =
      (1/2:ℝ)•(unsym(a)*unsym(b)+unsym(b)*unsym(a))+(1/2:ℝ)•(unsym(a)*unsym(c)+unsym(c)*unsym(a)),
    rw [mul_add, add_mul, smul_add, smul_add, smul_add, smul_add, smul_add],
    abel,
  end,
  right_distrib := λ a b c, begin
    change (1/2:ℝ)•((unsym(a)+unsym(b))*unsym(c)+unsym(c)*(unsym(a)+unsym(b))) =
      (1/2:ℝ)•(unsym(a)*unsym(c)+unsym(c)*unsym(a))+(1/2:ℝ)•(unsym(b)*unsym(c)+unsym(c)*unsym(b)),
    rw [mul_add, add_mul, smul_add, smul_add, smul_add, smul_add, smul_add],
    abel,
  end,
}

[Kevin Buzzard]

My guess is that a semiring which is an \R-algebra is a ring

[Christopher Hoskin]

Yes, that's true. We have module.add_comm_monoid_to_add_comm_group, but how to use it?

[Thomas Browning]

Here's one way:

noncomputable instance (α : Type*) [semiring α] [algebra ℝ α] : non_unital_non_assoc_ring (αˢʸᵐ) := {
  zero := sym 0,
  add := λ a b, a+b,
  add_assoc := λ a b c : α, add_assoc a b c,
  add_comm := λ a b : α, add_comm a b,
  zero_add := λ a, zero_add (unsym a),
  add_zero := λ a, add_zero (unsym a),
  neg := λ a, (-1:ℝ)•unsym(a),
  add_left_neg := λ a,
  calc (-1:ℝ)•unsym(a)+unsym(a) = (-1:ℝ)•unsym(a)+(1:ℝ)•(unsym(a)) : by rw one_smul
    ... = ((-1:ℝ)+(1:ℝ))•unsym(a) : by rw _root_.add_smul
    ... = (0:ℝ)•unsym(a) : by rw neg_add_self
    ... = 0 : by rw zero_smul,
  mul := λ a b, (sym ((1/2:ℝ)•(unsym(a)*unsym(b)+unsym(b)*unsym(a)))),
  zero_mul := λ _, by simp,
  mul_zero :=  λ _, by simp,
  left_distrib := λ a b c, begin
    change (1/2:ℝ)•(unsym(a)*(unsym(b)+unsym(c))+(unsym(b)+unsym(c))*unsym(a)) =
      (1/2:ℝ)•(unsym(a)*unsym(b)+unsym(b)*unsym(a))+(1/2:ℝ)•(unsym(a)*unsym(c)+unsym(c)*unsym(a)),
    rw [mul_add, add_mul, smul_add, smul_add, smul_add, smul_add, smul_add],
    abel,
  end,
  right_distrib := λ a b c, begin
    change (1/2:ℝ)•((unsym(a)+unsym(b))*unsym(c)+unsym(c)*(unsym(a)+unsym(b))) =
      (1/2:ℝ)•(unsym(a)*unsym(c)+unsym(c)*unsym(a))+(1/2:ℝ)•(unsym(b)*unsym(c)+unsym(c)*unsym(b)),
    rw [mul_add, add_mul, smul_add, smul_add, smul_add, smul_add, smul_add],
    abel,
  end,
}

[Eric Wieser]

Christopher Hoskin said:

Yes, that's true. We have module.add_comm_monoid_to_add_comm_group, but how to use it?

I can't help feeling this is an #xy problem - why do you want this vs the

noncomputable instance (α : Type*) [ring α] [algebra ℝ α] : non_unital_non_assoc_ring (αˢʸᵐ)

instance that was suggested above?

[Thomas Browning]

One advantage to assuming [ring α] [algebra ℝ α] (which isn't weaker, since it is implied by [semiring α] [algebra ℝ α]) is that negation on αˢʸᵐ is defeq to negation on α.

[Christopher Hoskin]

[ring α] is fine with me - it's a more natural way of thinking about it. I just couldn't get it to work before, but @Thomas Browning has shown that it can be done. Thanks!

[Eric Wieser]

I'd also recommend starting with:

instance [has_zero α] : has_zero (αˢʸᵐ) := { zero := sym 0 }
instance [has_add α] : has_add αˢʸᵐ := { add := λ a b, sym (unsym a + unsym b) }
instance [has_sub α] : has_sub αˢʸᵐ := { sub := λ a b, sym (unsym a - unsym b) }
instance [has_neg α] : has_neg αˢʸᵐ := { neg := λ a, sym (-unsym a) }
instance [has_scalar R α] : has_scalar R αˢʸᵐ := { smul := λ r a, sym (r•(unsym a)) }

-- add all the `sym_add` etc lemmas you already have here

lemma unsym_injective : function.injective (@unsym α) := λ _ _, id

-- build up all the proof structures:
instance [add_comm_semigroup α] : add_comm_semigroup (αˢʸᵐ) :=
unsym_injective.add_comm_semigroup _ (λ _ _, rfl)

instance [add_monoid α] : add_monoid (αˢʸᵐ) :=
unsym_injective.add_monoid_smul _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance [add_group α] : add_group (αˢʸᵐ) :=
unsym_injective.add_group_smul _ rfl
  (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [add_comm_monoid α] : add_comm_monoid (αˢʸᵐ) :=
{ ..sym_alg.add_comm_semigroup, ..sym_alg.add_monoid }

instance [add_comm_group α] : add_comm_group (αˢʸᵐ) :=
{ ..sym_alg.add_comm_monoid, ..sym_alg.add_group }

instance [semiring R] [add_comm_monoid α] [module R α] : module R αˢʸᵐ :=
function.injective.module R ⟨unsym, rfl, λ _ _, rfl⟩ (λ _ _, id) (λ _ _, rfl)

This will avoid ugly instance diamonds later, and also means you don't need your own add_smul and smul_add' lemmas.

[Christopher Hoskin]

Thanks. I'm now stuck trying to show that the squares of both multiplications coincide (up to identification):

lemma powers [ring α] [algebra ℝ α] (a: αˢʸᵐ) : unsym(a*a) = unsym a * unsym a :=
begin
  change (1/2:ℝ)•(unsym(a)*unsym(a)+unsym(a)*unsym(a)) = unsym(a)*unsym(a),
      abel,
      --rw smul_smul,
      unfold algebra.smul_def',
      rw ← mul_assoc,
      --rw ← map_mul,
      --rw ← algebra.to_ring_hom.map_mul' (1/2:ℝ) (2:ℤ),
      --rw ← (algebra_map ℝ α).map_mul' (1/2:ℝ) (2:ℤ),
      --rw ← mul_hom.map_mul' algebra.to_ring_hom,
      --rw ← map_mul algebra.to_ring_hom.to_fun (1/2:ℝ) (2:ℤ),
      sorry,
end

I get to

⊢ algebra.to_ring_hom.to_fun (1 / 2) * algebra.to_ring_hom.to_fun 2 * (unsym a * unsym a) = unsym a * unsym a

But then can't find the correct incantation to bring the 2 and 1/2 together so that they cancel out.

Christopher

[Eric Wieser]

At the point you introduced to_fun into the goal you made a wrong turn

[Christopher Hoskin]

Yes, the problem is I don't know how to convert the (2:ℤ) that abel gives me into (2:ℝ) so that I can invoke smul_smul.

Okay:

lemma test2 [ring α] [algebra ℝ α] (r :ℝ) (s: ℝ) (a:α) : r•(s•a) = (r*s)•a :=
begin
  rw smul_smul r s a,
end

Fails:

lemma test2 [ring α] [algebra ℝ α] (r :ℝ) (s: ℤ) (a:α) : r•(s•a) = (r*s)•a :=
begin
  rw smul_smul r s a,
end

[Yaël Dillies]

norm_cast, norm_num or docs#int.cast_two should all do the job.

[Eric Wieser]

docs#smul_assoc should apply there

[Christopher Hoskin]

Finally got there with:

theorem two_rmul [ring α] [algebra ℝ α]  (x:α) : (2 : ℝ) • x = x + x :=
begin
   rw [bit0, add_smul, one_smul],
end

lemma powers [ring α] [algebra ℝ α] (a: αˢʸᵐ) : unsym(a*a) = unsym a * unsym a :=
begin
  rw mul_def,
  rw unsym_sym,
  rw ← two_rmul,
  rw ← smul_assoc,
  simp,
end

[Eric Wieser]

Isn't that first lemma just docs#two_smul?

[Oliver Nash]

Catching up on this thread (and the corresponding PR #11073) I have a question: is there a Jordan equivalent of Poisson algebras? More precisely, is it ever necessary to be able to regard a type _simultaneously_ as a Jordan ring and an associative ring?

[Oliver Nash]

I couldn't quite figure out what right compatibility between the two structures would be but if these structures do arise then the proposed setup might be awkward because both operations are trying to own has_mul.