## Stream: new members

### Topic: Operator precedence

#### Nicolò Cavalleri (Aug 08 2020 at 10:56):

I need to prove the lemma at the bottom of this #mwe. My strategy is to prove it for functions and then write a simp lemma for for the behavior of the coercion from linear_map to functions, however I cannot manage to make the precedence of operators and coercions work. What is a standard solution for this? changing the precedence of the operator?

import algebra.lie_algebra

variables {A : Type*} {R : Type*} [comm_ring R] [ring A] [algebra R A] (L1 L2 : A →ₗ[R] A) (a : A)

@[priority 100]
instance asdfg (A : Type*) [ring A] : lie_ring A :=
{ bracket  := ring_commutator.commutator,
lie_self := ring_commutator.alternate,
jacobi   := ring_commutator.jacobi }

@[priority 100]
instance jnknj{A : Type*} [ring A] [algebra R A] :
lie_algebra R A :=
{ lie_smul := λ t x y,
by rw [lie_ring.of_associative_ring_bracket, lie_ring.of_associative_ring_bracket,
algebra.mul_smul_comm, algebra.smul_mul_assoc, smul_sub], }

lemma commutator_to_fun_coe : (⁅L1, L2⁆ : A → A) = ⁅(L1 : A → A), (L2 : A → A)⁆ :=
begin

end

lemma commutator_apply : ⁅L1, L2⁆ a = ⁅L1 a, L2 a⁆ := sorry


#### Nicolò Cavalleri (Aug 08 2020 at 15:11):

(Any other idea to prove the lemma at the bottom is welcome it does not need to follow my strategy. It's just that any attempt to do unfold ring_commutator.commutator failed and I do not know why!)

#### Oliver Nash (Aug 10 2020 at 19:52):

I've just seen this but a few things confuse me.

#### Oliver Nash (Aug 10 2020 at 19:53):

Firstly it looks like foo and bar are just copies of lie_ring.of_associative_ring and lie_algebra.of_associative_algebra so I think instead we should just use:

local attribute [instance] lie_ring.of_associative_ring
local attribute [instance] lie_algebra.of_associative_algebra


#### Oliver Nash (Aug 10 2020 at 19:55):

(There is also the issue of @[priority 100] which I am ignoring, this might be connected with the fact the *.of_associative_ring are defs and not instances --- I confess I am not sure what issues may lurk here.)

#### Oliver Nash (Aug 10 2020 at 19:56):

It is not clear to me that you need commutator_to_fun_coe because this is the sort of thing that we should be able to solve with lie_ring.of_associative_ring_bracket and indeed rw lie_ring.of_associative_ring_bracket serves as a proof and anyway the proof is rfl.

#### Oliver Nash (Aug 10 2020 at 19:57):

Finally I could be missing something but I just don't think commutator_apply is true!

#### Oliver Nash (Aug 10 2020 at 19:59):

Indeed if you start the would-be proof as:

  change L1 (L2 a) - L2 (L1 a) = (L1 a) * (L2 a) - (L2 a) * (L1 a),


It seems to me that the results is obviously false in general.

Last updated: May 11 2021 at 00:31 UTC