Zulip Chat Archive

Stream: maths

Topic: naming: lie_smul


view this post on Zulip Johan Commelin (Oct 10 2020 at 08:45):

Currently, in mathlib, we have

@[simp] lemma lie_smul  (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L]
  (t : R) (x y : L) : x, t  y = t  x, y :=
 lie_algebra.lie_smul t x y

However, if we want to define a lie_action (which will be part of lie_module), then this is one of the axioms
image.png
which I assume would be called lie_smul.

Does anyone have a good suggestion for fixing this naming conflict?
The best I have come up with is a namespaced lie_action.lie_smul. But that's quite a mouthful.

view this post on Zulip Eric Wieser (Oct 10 2020 at 08:50):

Should the existing one be lie_smul_right, to distinguish from the case with t . x, y?

view this post on Zulip Johan Commelin (Oct 10 2020 at 10:18):

No, the latter would be smul_lie...

view this post on Zulip Johan Commelin (Oct 10 2020 at 10:18):

... in the current naming scheme.

view this post on Zulip Johan Commelin (Oct 10 2020 at 10:18):

But I guess we need a more sophisticated naming scheme to distinguish all the possible combinations

view this post on Zulip Eric Wieser (Oct 10 2020 at 10:28):

I thought the naming was assuming all functions were prefix notation

view this post on Zulip Eric Wieser (Oct 10 2020 at 10:29):

Ah I guess add_mul vs mul_add is the counterexample I need

view this post on Zulip Kenny Lau (Oct 10 2020 at 10:35):

@Johan Commelin the second one is called lie_smul', the third one lie_smul'', etc.

view this post on Zulip Kenny Lau (Oct 10 2020 at 10:45):

(/s)

view this post on Zulip Oliver Nash (Oct 10 2020 at 18:29):

@Johan Commelin am I confused or do we not already have a version of this here ?

view this post on Zulip Oliver Nash (Oct 10 2020 at 18:29):

(called lie_act)

view this post on Zulip Oliver Nash (Oct 10 2020 at 18:33):

(As it happens I have plans to refactor lie_module in my non-existent copious free time so that the action is an instance of has_scalar.)

view this post on Zulip Johan Commelin (Oct 10 2020 at 20:39):

@Oliver Nash Oooh cool! I didn't realise we already had this!

view this post on Zulip Johan Commelin (Oct 10 2020 at 20:39):

Thanks for the pointer

view this post on Zulip Oliver Nash (Oct 10 2020 at 21:15):

Let me know if there’s anything I can do to help. Perhaps I should just bump the priority of that refactor I mentioned?

view this post on Zulip Johan Commelin (Oct 12 2020 at 06:04):

@Oliver Nash If such a priority bumping feature is available... I would happily see the results :grinning:


Last updated: May 11 2021 at 15:12 UTC