Zulip Chat Archive

Stream: new members

Topic: Operator precedence


view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip Oliver Nash (Aug 10 2020 at 19:52):

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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Aug 10 2020 at 19:57):

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

view this post on Zulip 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