Operator precedence

Stream: new members

[Nicolò Cavalleri]

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]

(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]

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

[Oliver Nash]

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]

(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]

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]

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

[Oliver Nash]

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.

[Matt Yan]

where can I find a table of operator precedence and associativity in lean?
specifically, I'm having a hard time understanding this goal: $\vdash P \land Q \vee P \land R$, using left and right soon shows that lean implies $\vdash (P \land Q) \vee (P \land R)$, which is neither left nor right associativity. It seems to imply that $\land$ has higher precedence than $\vee$ ?