G-submodules

Stream: maths

[Yaël Dillies]

This is half a maths question, half a formalisation question. I hope the location is somewhat accurate.

[Yaël Dillies]

leasen mathlib we have docs#Submodule which represents a submodule of a docs#Module under the action of a docs#Ring. Recall that a R-module M is an additive commutative monoid with an action • : R → M → M respecting:

• one_smul : 1 • x = x
• mul_smul : (a * b) • x = a • b • x
• smul_zero : a • 0 = 0
• smul_add : a • (x + y) = a • x + a • y
• zero_smul : 0 • x = 0
• add_smul : (a + b) • x = a • x + b • x

[Yaël Dillies]

... and a R-submodule is a set s : Set M respecting:

• zero_mem : 0 ∈ s
• add_mem : x ∈ s → y ∈ s → x + y ∈ s
• smul_mem : x ∈ s → a • x ∈ s

[Yaël Dillies]

In mathematics, there are two very similar notions of G-module and G-submodule, which in mathlib are encapsulated by docs#DistribMulAction and... well, we don't have G-submodules.

[Aaron Liu]

docs#SubMulAction (edit: apparently not)

[Yaël Dillies]

(it's not closed under addition, and please let me finish)

[Aaron Liu]

Sorry, I can't tell when you're finished

[Yaël Dillies]

Well, please don't jump to conclusions. If the answer to my question was a single declaration in mathlib, I would have found it. :smile:

[Yaël Dillies]

For a monoid G, mathlib defines a G-module M to be an additive commutative monoid with an action • : G → M → M respecting:

• one_smul : 1 • x = x
• mul_smul : (a * b) • x = a • b • x
• smul_zero : a • 0 = 0
• smul_add : a • (x + y) = a • x + a • y

ie we have dropped zero_smul and add_smul from Module

[Yaël Dillies]

We do not have G-submodules in mathlib in full generality, but we do have a special case in the form of docs#ConvexCone. There, G is set to be {r : R // 0 < r} where R is a strictly ordered ring.

[Yaël Dillies]

I need to prove results about cones in the context of Toric, and in particular I would like to use a result akin to docs#Submodule.span_eq_iUnion_nat.

[Yaël Dillies]

The precise result I want is that the G-span of a set s : Set M can be written as ⋃ n ≥ 1, ⋃ g : G, g • n • s. Motivation: If s is open, then n • s is open too, and so is g • n • s (assuming G acts by homeos, which is only true if G is a group!), therefore the whole span is open too. This is isOpen_hull in #24149.

[Yaël Dillies]

That result (the one writing the span as a union, not the one about the span being open) also holds for usual modules, so it got me thinking that actually docs#Submodule is basically the correct definition of a G-submodule already.

[Yaël Dillies]

The only issue is that I need to get rid of zero_mem : 0 ∈ s. But actually if I make the axioms of Submodule be

• add_mem : x ∈ s → y ∈ s → x + y ∈ s
• smul_mem : x ∈ s → a • x ∈ s

then zero_mem will automatically be true by smul_mem if I can set a := 0, ie if my scalars have a zero.

[Yaël Dillies]

This is therefore my
First proposal: Weaken docs#Submodule to not require R to be a semiring and to drop the zero_mem field

[Yaël Dillies]

However, there is now an issue: A G-submodule might not be a G-module! or at least not in the sense of docs#DistribMulAction: The field smul_zero : a • 0 = 0 would require my G-submodule to have a zero, but quite importantly I want the flexibility to not have a zero (eg isOpen_hull wouldn't hold if I were to force a zero in).

[Yaël Dillies]

Therefore come two questions:
1. Are you happy with docs#Submodule also standing for G-submodules by appropriately weakening the semiring assumption in places?
2. What is the correct definition of a G-module? Is docs#DistribMulAction supposed to encapsulate G-modules? If so, can we change it so that a G-submodule becomes a G-module?

[Yaël Dillies]

cc @Eric Wieser, as you are probably one of the only people to care about DistribMulAction

[Michael Stoll]

Do you want to allow the empty submodule? (Note that zero_mem forces it to be nonempty. One could replaces it by asking for the submodule to be nonempty; for modules over a ring (or a monoid with zero as long as zero_smul holds) this will imply zero_mem.)

[Yaël Dillies]

I have not yet found a reason to allow nor to disallow the empty submodule. From the Toric side of things, we certainly don't ever care about empty cones, and most (but not all!) of our cones will in fact be docs#PointedCone rather than ConvexCone.

[Andrew Yang]

@Kevin Buzzard this is the thing I was talking about in LLL today.

[Yaël Dillies]

Oh great! :heart: I didn't know whether you ended up talking or not. Sorry for ditching last minute.

[Yaël Dillies]

Actually... if we disallow the empty G-submodule, then it's not true anymore that G-submodules form a lattice. That's probably quite a sad fact to lose, no?

[Yaël Dillies]

Oh sorry, I get what you mean. If I want to interface with Submodule then I certainly need G-submodules to be nonempty :thinking:

[Kevin Buzzard]

Submodules aren't allowed to be empty in maths so that's a big problem

[Aaron Liu]

Do we want to have something like docs#DistribMulAction but changing [AddMonoid A] to [AddSemigroup A] (or even just [Add A])?

[Yaël Dillies]

That is more or less what my second question is offering

[Jireh Loreaux]

Kevin Buzzard said:

Submodules aren't allowed to be empty in maths so that's a big problem

But maths didn't generally allow for ⊥ : Filter α either (nor 0⁻¹), so I don't find that in and of itself to be a convincing argument.

[Eric Wieser]

I'm a little confused what you're asking for here. Can you just write a candidate definition of the thing you actually need, without the consideration of trying to make it fit into modifications of things we already have?

[Yaël Dillies]

I mean, the candidate already exists and it's docs#ConvexCone

[Scott Carnahan]

Should we rename docs#DistribMulAction to DistribMulActionWithZero and let docs#DistribMulAction just extend docs#MulAction with smul_add?

[Aaron Liu]

Scott Carnahan said:

Should we rename docs#DistribMulAction to DistribMulActionWithZero and let docs#DistribMulAction just extend docs#MulAction with smul_add?

But MulActionWithZero is a MulAction in which zero_smul and smul_zero, so calling it DistribMulActionWithZero when it doesn't have a zero_smul doesn't feel right to me.

[Scott Carnahan]

I see, it's more like docs#SMulZeroClass than docs#SMulWithZero. IsDistribMulActionZeroClass too long?

[Edward van de Meent]

personally i'd call it AddMulAction

[Yaël Dillies]

Scott Carnahan said:

I see, it's more like docs#SMulZeroClass than docs#SMulWithZero. IsDistribMulActionZeroClass too long?

That's a nice idea

[Edward van de Meent]

or actually, nvm. AddMulAction can cause confusion with docs#AddAction

[Antoine Chambert-Loir]

This feature is not much used in the Elements but Bourbaki has a notion of group with operators, that would just be an action by a type, and stable subgroups. This is used for modules/submodules, but also for normal subgroups which are stable subgroups when the group acts on itself by conjugation.

[Antoine Chambert-Loir]

So I would approve that submodule (and morphisms) rely on minimal assumptions on the nature of the action.

[Yaël Dillies]

Does Bourbaki allow empty submodules? empty G-submodules?

[Kevin Buzzard]

Definitely Bourbaki does not allow empty vector spaces but maybe in more generality this is OK?

[Antoine Chambert-Loir]

They only talk about stable subgroups. Monoids appear rarely.

[Adam Topaz]

IMO a G-submodule (aka a sub-G-module) should have the structure of a G-module and thus cannot be empty.

[Adam Topaz]

In general a sub-foo should be a foo…

[Adam Topaz]

I'm also confused about the lattice issue... we have docs#Submodule.completeLattice

[Adam Topaz]

A $G$-module $M$ is simply a module over the monoid algebra $\N[G]$

[Adam Topaz]

("is" in the mathematical sense, not the mathlib sense)

[Yaël Dillies]

No, not in the sense we need them for docs#ConvexCone. It's very important we do not require a G-module to have a zero, cf the argument in #maths > G-submodules @ 💬

[Adam Topaz]

I'm sorry, but if it doesn't have zero, then IMO you should not call it a submodule.

[Adam Topaz]

If you have a semiring $R$ and an $R$-module $M$, then you can talk about convex linear combinations, i.e. linear combinations of the form $a_1 m_1 + \cdots + a_n m_n$ where $a_1 + \cdots + a_n = 1$. I guess you want convex cone to be some subset which is closed under such combinations (and under scalar multiplication)? the current definition agrees with this notion in some cases, but why would you want to call it a submodule? The algebraic structure is completely different. In principle you can have an algebraic structure on $R$ where one could talk about such convex combinations, and this would be a module over that kind of algebraic object (in the sense of universal algebra).

[Andrew Yang]

I guess the conclusion is we could have SubSMulAdd but it shouldn’t and couldn’t replace submodules.

[Adam Topaz]

Yeah, that's exactly what it is, a sub-foo where foo is something with an smul and an add.

[Adam Topaz]

(I also don't completely agree with the name ConvexCone, but since we don't have a formalization of abstract convexity, this isn't an issue... yet)