Zulip Chat Archive

Stream: general

Topic: linear_action


Johan Commelin (Nov 03 2020 at 16:07):

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 (Nov 03 2020 at 16:09):

isn't this just linear_map.mk\2

Johan Commelin (Nov 03 2020 at 16:11):

But that's not a class

Johan Commelin (Nov 03 2020 at 16:13):

@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 (Nov 03 2020 at 16:13):

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

Oliver Nash (Nov 03 2020 at 16:14):

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 (Nov 03 2020 at 16:14):

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

Oliver Nash (Nov 03 2020 at 16:15):

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 (Nov 03 2020 at 16:15):

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 (Nov 03 2020 at 16:16):

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

Johan Commelin (Nov 03 2020 at 16:16):

So I'm looking into how we should organise:

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

Kenny Lau (Nov 03 2020 at 16:18):

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

Johan Commelin (Nov 03 2020 at 16:21):

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

Kenny Lau (Nov 03 2020 at 16:23):

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

Kenny Lau (Nov 03 2020 at 16:24):

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

Kenny Lau (Nov 03 2020 at 16:24):

or maybe relax the definition thereof to forgo associativity

Oliver Nash (Nov 06 2020 at 12:00):

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 (Nov 06 2020 at 12:03):

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 (Nov 06 2020 at 12:07):

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 (Nov 06 2020 at 12:09):

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 (Nov 06 2020 at 12:11):

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 (Nov 06 2020 at 12:12):

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

Johan Commelin (Nov 06 2020 at 12:35):

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 (Nov 06 2020 at 12:36):

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

Johan Commelin (Nov 06 2020 at 12:37):

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

Johan Commelin (Nov 06 2020 at 12:37):

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

Reid Barton (Nov 06 2020 at 12:47):

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 (Nov 06 2020 at 12:48):

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

Oliver Nash (Nov 06 2020 at 13:05):

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

Oliver Nash (Nov 06 2020 at 13:05):

(and I will document on has_bracket as suggested)

Oliver Nash (Nov 08 2020 at 20:22):

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 (Nov 08 2020 at 20:25):

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.


Last updated: Dec 20 2023 at 11:08 UTC