Stream: maths

Topic: naming: lie_smul

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.

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?

Johan Commelin (Oct 10 2020 at 10:18):

No, the latter would be smul_lie...

Johan Commelin (Oct 10 2020 at 10:18):

... in the current naming scheme.

Johan Commelin (Oct 10 2020 at 10:18):

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

Eric Wieser (Oct 10 2020 at 10:28):

I thought the naming was assuming all functions were prefix notation

Eric Wieser (Oct 10 2020 at 10:29):

Ah I guess add_mul vs mul_add is the counterexample I need

Kenny Lau (Oct 10 2020 at 10:35):

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

(/s)

Oliver Nash (Oct 10 2020 at 18:29):

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

Oliver Nash (Oct 10 2020 at 18:29):

(called lie_act)

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.)

Johan Commelin (Oct 10 2020 at 20:39):

Thanks for the pointer

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?

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