# Zulip Chat Archive

## 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,
add_lie := ring_commutator.add_left,
lie_add := ring_commutator.add_right,
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 `def`

s and not `instance`

s --- 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