Typeclasses on module

Stream: general

[Yaël Dillies]

Why does the definition of module require such strong typeclasses? Is it because somehow those are forced by the rest anyway?

[Adam Topaz]

what do you consider "strong" in this case?

[Yaël Dillies]

semiring instead of monoid + add_monoid for example

[Adam Topaz]

For the action of a monoid, you can just use mul_action.

[Adam Topaz]

Oh I see.... you want the action compatible with addition in the add_monoid

[Adam Topaz]

We have docs#distrib_mul_action .

[Yaël Dillies]

All in all, the instance jump from distrib_mul_action/mul_action_with_zero is high.

[Yaël Dillies]

I usually find myself wanting distrib_mul_action_with_zero (#9123), but that's not what I meant here.

[Yaël Dillies]

As long as we're at it, there should be a typeclass smul_with_zero_right which would unify docs#smul_zero' and docs#smul_zero

[Adam Topaz]

ping @Eric Wieser

[Adam Topaz]

What examples do you have in mind? If we start adding classes for everything under the sun, we'll be doing nonsense forever.

[Yaël Dillies]

Eric had an instance of a distrib_mul_action_with_zero which was not a module. smul_with_zero_right is just here to be the intersection of two things which are used a lot.

[Reid Barton]

ah yes, the classic combinatorics question of how many different sets of legs can you pull off a caterpillar

[Yaël Dillies]

But again that's not what my question is about. I'm asking why module is taking semiring and not monoid + add_monoid

[Adam Topaz]

Can you deduce (a + b) \smul c = a \smul c + b \smul c without it?

[Reid Barton]

It makes no math difference because the endomorphisms of an add_comm_monoid form a semiring anyways. So instead of a module over a semiring you would have a module over the semiring presented by something that might not be a semiring yet.

[Adam Topaz]

I'm confused. Say $M$ is a commutative additive monoid, then yes $End(M)$ is a semiring, and giving a module structure is equivalent to giving a morphism of semirings $R \to End(M)$, but now you're suggesting to just give a morphism of monoids $R \to End(M)$?

[Reid Barton]

No, a morphism of has_add/zero/mul/ones

[Adam Topaz]

Oh ok..

[Reid Barton]

But I can't think of any instances where you construct a semiring by starting with something that doesn't satisfy distributivity and then imposing distributivity as a relation. But perhaps such a thing is out there?

[Adam Topaz]

Right, I can't think of any examples where this would be useful.

[Yaël Dillies]

So do the axioms of module \a \b imply semiring \a?

[Adam Topaz]

No, not in general

[Adam Topaz]

For example if $M$ is trivial, you won't be able to get any info about R.

[Eric Wieser]

@Yaël Dillies, can you be clear about exactly what alternate definition you're proposing for module, in the form of a class declaration?

[Yaël Dillies]

@[protect_proj] class module' (R M : Type*) [monoid R] [add_monoid R]
  [add_comm_monoid M] extends distrib_mul_action R M :=
(add_smul : ∀(r s : R) (x : M), (r + s) • x = r • x + s • x)
(zero_smul : ∀x : M, (0 : R) • x = 0)

[Adam Topaz]

That would probably work (for essentially the same reason that Reid mentioned above, as the map R \to End(M) would be both a morphism of monoids and of add_monoids)

[Reid Barton]

you also don't need to stop there, you could have [has_zero R] [has_add R] [has_one R] [has_mul R], maybe after making corresponding changes to the superclasses

[Adam Topaz]

These are haskell's semirings right ;)?

[Reid Barton]

module over a Num

[Reid Barton]

What are the examples that you want to support this way?

[Reid Barton]

In some sense there can't be any because a module' over a whatever R is "the same" as an ordinary module over some other ring constructed from R (which is R itself if R was already a ring).

[Yaël Dillies]

It just felt wrong to bump my instances for the sake of using module and I wanted an explanation.

[Reid Barton]

Fair enough! Did you get one? :upside_down:

[Yaël Dillies]

I guess I did!

[Reid Barton]

My explanation was rather compressed, and I could give a more expanded one. Let's instead take the simpler question of why mul_action has [monoid α] and not just [has_one α] [has_mul α].

If I have [has_one M] [has_mul M] and a mul_action of M on a set X, I certainly can't prove that M is actually a monoid (e.g. for a b c : M, we have (a * b) * c = a * (b * c)) from that because, as Adam noted, the set X could be a singleton and all the laws for an action would hold automatically. However, I do know that for any a b c : M and x : X, we must have
((a * b) * c) • x = (a * (b * c)) • x
because the laws for an action imply that both are equal to
a • (b • (c • x)).

[Reid Barton]

So I could form a quotient of M where we impose the relations (a * b) * c = a * (b * c) for all a b c, and the action of M on X will descend to the quotient. For the same reason, I might as well also impose the relations 1 * a = a = a * 1. Once I do that, I made M into a monoid.

[Reid Barton]

And because of the way I formed this quotient, say N, giving an action of the monoid N on X is equivalent to giving an action of the original thing M on X.

[Reid Barton]

So, there's not really any point in considering actions by things that aren't monoids.

[Reid Barton]

Same in the additive context for semirings.