trivial lieringmodule

Stream: Is there code for X?

[Edison Xie]

Do we not have this instance?

import Mathlib
variable (R : Type*) [CommRing R]

instance : LieRingModule R Unit where
  bracket _ _ := Unit.unit
  add_lie _ _ _ := rfl
  lie_add _ _ _ := rfl
  leibniz_lie _ _ _ := rfl

[Eric Wieser]

I guess if #synth says no, we don't

[Eric Wieser]

Note we should have it for the more general PUnit

[Eric Wieser]

(and the whole hierarchy of Lies)

[Edison Xie]

Eric Wieser said:

I guess if #synth says no, we don't

yeah that's what I tried :(

[Edison Xie]

Eric Wieser said:

Note we should have it for the more general PUnit

adding a "P" in front of everything just works lol

instance : LieRingModule R PUnit where
  bracket _ _ := PUnit.unit
  add_lie _ _ _ := rfl
  lie_add _ _ _ := rfl
  leibniz_lie _ _ _ := rfl

[Edison Xie]

@Eric Wieser so should we PR this instance?

[Eric Wieser]

Yes, but let's have @Oliver Nash review it

[Ruben Van de Velde]

Eric Wieser said:

(and the whole hierarchy of Lies)

(How does one pronounce Lies?)

[Oliver Nash]

I think the instance should be:

instance (L : Type*) [LieRing L] : LieRingModule L PUnit where
  bracket _ _ := PUnit.unit
  add_lie _ _ _ := rfl
  lie_add _ _ _ := rfl
  leibniz_lie _ _ _ := rfl

partly because this is more general and partly because one day I'd like to demote docs#LieRing.ofAssociativeRing from being an instance.

[Oliver Nash]

In fact we should probably even generalise the above so that it doesn't just talk about the concrete type docs#PUnit but applies to any type with a unique element. I.e.,

instance (L M : Type*) [LieRing L] [Unique M] : LieRingModule L M := sorry

[Eric Wieser]

That looks like a diamond issue to me, I think best to stick with PUnit like we do for other algebraic structures

[Oliver Nash]

Oh indeed, that could be an issue. I guess it could be a def but then it's hardly worth it.

[Junyan Xu]

If we add a LieRing PUnit instance, do we get diamond with [LieRing L] : LieRingModule L PUnit when L = PUnit? (I guess not.)