constructing modules in abstarct algebra

Stream: new members

[Esteban Estupinan]

hi, vector space is a kind of module, when we using a field instead a ring or semiring, I believe. I have two questions, why to construct a module we need a commutative group or monoid, instead a simple group or monoid? Why this commutative group or monoid must be only additive ?

[Kevin Buzzard]

This is the definition of a module. I'm not sure what kind of answer you're looking for here

[Kyle Miller]

Maybe this is a reason to believe that modules over semirings should be commutative monoids. More generally, a monoid object in an appropriate kind of category (a monoidal category to be precise) is an object $A$ along with morphisms $\mu:A\times A\to A$ and $\eta:1\to A$, where all the diagrams associated to the axioms of a monoid commute. A left module $M$ over the monoid is another object along with a morphism $\alpha:A\times M\to M$ such that the diagrams associated to the axioms of a monoid action commute. A semiring is a monoid object in the category of commutative monoids, so a module is defined to be a commutative monoid.

One observation is that since you'd want something like $(a+b)m = am+bm$ out of a module, and $a+b=b+a$ is true for the semiring, then you'd have $am+bm=bm+am$. You may as well require $m+n=n+m$ for all $m$ and $n$ in $M$.

[Kyle Miller]

From this point of view, modules are additive (rather than multiplicative) monoids because semirings are additive monoids (with additional multiplicative structure from $\mu$).

[David Wärn]

Indeed for any module over any semiring, left- and right- distributivity means $(m+n) + (m+n) = (1+1)(m+n) = (m+m) + (n+n)$. Assuming addition in the module is cancellative and associative we get $n+m = m+n$, so commutativity is automatic (same argument works for addition in semirings). Still, Lean could conceivable only require [add_group M] to say module R M, and prove commutativity from this.

[Sebastien Gouezel]

There is a catch that you could not use typeclass inference to deduce commutativity of the addition from [module R M] since Lean would not know which R it should look for.

[Esteban Estupinan]

every vector space is an additive abelian group. Its ok, but the scalar operation forms 4 axioms more, where do these operations come from? do they have to do with some groups or fields? where I can find information about the origin of these operations with the scalar ?

[Esteban Estupinan]

imagen.png

[Eric Wieser]

In mathlib, you can use docs#mul_action to get axioms 1 and 2; docs#distrib_mul_action to get axioms 1 2 and 3, and docs#module to get all four (plus some axioms about zero that only follow from the other axioms if V is an additive group and not just an additive monoid)

[Adam Topaz]

Let me reiterate what Kyle said above. A (semi)ring is a monoid object in a specific monoidal category, and a module over a (semi)ring is an object with an action of said monoid object.

If you work with the category of sets, you get the usual notion of a monoid acting on a set.

If you work with the category Ab of abelian groups, you recover the usual notion of a module over a ring.