linear_action

Stream: general

[Johan Commelin]

Should docs#linear_action be refactored to in terms of is_scalar_tower? (And replace act by smul, in particular)

variables (R : Type u) (M N : Type v)
variables [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]

/--
A binary operation representing one module acting linearly on another.
-/
class linear_action :=
(act      : M → N → N)
(add_act  : ∀ (m m' : M) (n : N), act (m + m') n = act m n + act m' n)
(act_add  : ∀ (m : M) (n n' : N), act m (n + n') = act m n + act m n')
(act_smul : ∀ (r : R) (m : M) (n : N), act (r • m) n = r • (act m n))
(smul_act : ∀ (r : R) (m : M) (n : N), act m (r • n) = act (r • m) n)

cc: @Kenny Lau @Oliver Nash

[Kenny Lau]

isn't this just linear_map.mk\2

[Johan Commelin]

But that's not a class

[Johan Commelin]

@Kenny Lau Put in a different way. Given the recent changes (e.g. is_scalar_tower) how would you formalize lie_module nowadays?

[Oliver Nash]

@Johan Commelin Yes! I keep meaning to get to this.

[Oliver Nash]

I've got a little free time coming up so I can commit to starting this refactor before the end of the week.

[Johan Commelin]

I need to explain what a semisimple Lie algebra is in my course, in the next couple of days...

[Oliver Nash]

Oooh really! That's something else I keep meaning to get to. There are a bunch of definitions that are all equivalent over field of char 0 so I need to be a bit careful with the actual definition but I think I know what I want to propose.

[Kenny Lau]

Johan Commelin said:

Kenny Lau Put in a different way. Given the recent changes (e.g. is_scalar_tower) how would you formalize lie_module nowadays?

I don't know; what do you think?

[Oliver Nash]

I'll push to get to this also though unfortunately will not be within couple of days.

[Johan Commelin]

So I'm looking into how we should organise:

• representation of Lie algebra (aka lie_module)
• subrepresentation
• subalgebra
• ideal
• the notation $[\mathfrak{a}, \mathfrak{b}]$, where $\mathfrak{a}, \mathfrak{b}$ are ideals

[Kenny Lau]

what's the difference between a g-module and, you know, [module g V]?

[Johan Commelin]

What is module g V? In lean that doesn't make sense, because g is not a ring.

[Kenny Lau]

oh, right (I thought algebra => ring but this is not associative)

[Kenny Lau]

I don't know, probably copy the definition of module

[Kenny Lau]

or maybe relax the definition thereof to forgo associativity

[Oliver Nash]

I made an attempt at refactoring linear_action / lie_module yesterday evening with view to using is_scalar_tower. I claim that this is not a promising way to go but I'm keen to hear any contrary opinions.

[Oliver Nash]

The point is that to use is_scalar_tower, we must unbundle linear_action.act into a has_scalar instance. Indeed this is a large part of the appeal since we can then use the associated notation. However once we think about lie_ideal there is a problem because these would require us to define a scalar self-action of lie_algebras (actually it would be lie_rings) and this would conflict with the same concept for associative rings.

[Oliver Nash]

To be more concrete, to use is_scalar_tower, we would have to define a has_scalar instance on lie_rings as x • y = ⁅x, y⁆ to make lie_ideals work. However this would lead to two mathematically different scalar actions when we are in the case that we are looking at the Lie ring associated to an associative ring.

[Oliver Nash]

I think a possible solution which I believe would work would be to change:

class has_bracket (L : Type v) := (bracket : L → L → L)

to:

class has_bracket (L M : Type v) := (bracket : L → M → M)

and then define a lie_module to include an unbundled has_bracket instance.

[Oliver Nash]

If we did this then lie_modules would be setup slightly differently to modules over an associative ring in the sense that the latter have has_mul and has_scalar whereas I am proposing using only has_bracket for the former. I haven't tried this but I _think_ it would work.

[Oliver Nash]

@Johan Commelin Would you like me to put together a PR (most likely tomorrow) implementing this approach?

[Johan Commelin]

So we would write [X, v] for the action of X on a vector v (where X : L lives in a Lie algebra, and v : V in some representation of L).

[Johan Commelin]

Whereas atm, we would be trying to use X \bu v.

[Johan Commelin]

I think having has_bracket depend on two type parameters makes sense (they can live in different universes, btw).

[Johan Commelin]

It works for has_scalar, and this will be it's Lie-theoretic cousin.

[Reid Barton]

I haven't followed the is_scalar_tower story but this sounds reasonable to me. Probably worth documenting on has_bracket itself that the reason for the type is that it will be used for both algebras and modules.

[Reid Barton]

I guess the disadvantage will be that sometimes you need more type annotations in things like bracket l 0 = 0.

[Oliver Nash]

Thank you both for the input. I'll have a go at this tomorrow and see how I get on.

[Oliver Nash]

(and I will document on has_bracket as suggested)

[Oliver Nash]

I finally took this up today and now have a refactored version of lie_modules working where the data of the action (i.e., the map L → M → M) is unbundled as an instance of has_bracket and so it is possible to use the notation ⁅x, m⁆ for x : L acting on an element of a module m : M.

[Oliver Nash]

I'll see if I can get a PR out this evening but it might have to be tomorrow evening till I have things tidy enough. For what it's worth, it occurred to me that we _could_ in fact have the action inhabit an instance of has_scalar despite the clash with the extant has_scalar action when regarding commutative rings as associative algebras over themselves. This was the inspiration for my question here https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/multiple.20solutions.20for.20typeclass.20search/near/216002921 (foo playing the role of has_scalar) but I think it is better not to shoot for this.