Zulip Chat Archive

Stream: general

Topic: Typeclasses on module


Yaël Dillies (Jan 11 2022 at 18:50):

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

Adam Topaz (Jan 11 2022 at 19:17):

what do you consider "strong" in this case?

Yaël Dillies (Jan 11 2022 at 19:28):

semiring instead of monoid + add_monoid for example

Adam Topaz (Jan 11 2022 at 19:30):

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

Adam Topaz (Jan 11 2022 at 19:31):

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

Adam Topaz (Jan 11 2022 at 19:32):

We have docs#distrib_mul_action .

Yaël Dillies (Jan 11 2022 at 19:33):

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

Yaël Dillies (Jan 11 2022 at 19:33):

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

Yaël Dillies (Jan 11 2022 at 19:34):

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 (Jan 11 2022 at 19:35):

ping @Eric Wieser

Adam Topaz (Jan 11 2022 at 19:36):

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 (Jan 11 2022 at 19:37):

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 (Jan 11 2022 at 19:37):

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

Yaël Dillies (Jan 11 2022 at 19:38):

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 (Jan 11 2022 at 19:39):

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

Reid Barton (Jan 11 2022 at 19:40):

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 (Jan 11 2022 at 19:42):

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

Reid Barton (Jan 11 2022 at 19:42):

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

Adam Topaz (Jan 11 2022 at 19:43):

Oh ok..

Reid Barton (Jan 11 2022 at 19:43):

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 (Jan 11 2022 at 19:44):

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

Yaël Dillies (Jan 11 2022 at 19:45):

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

Adam Topaz (Jan 11 2022 at 19:45):

No, not in general

Adam Topaz (Jan 11 2022 at 19:46):

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

Eric Wieser (Jan 11 2022 at 19:46):

@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 (Jan 11 2022 at 19:47):

@[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 (Jan 11 2022 at 19:48):

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 (Jan 11 2022 at 19:49):

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 (Jan 11 2022 at 19:50):

These are haskell's semirings right ;)?

Reid Barton (Jan 11 2022 at 19:50):

module over a Num

Reid Barton (Jan 11 2022 at 19:51):

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

Reid Barton (Jan 11 2022 at 19:52):

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 (Jan 11 2022 at 19:53):

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

Reid Barton (Jan 11 2022 at 19:56):

Fair enough! Did you get one? :upside_down:

Yaël Dillies (Jan 11 2022 at 19:56):

I guess I did!

Reid Barton (Jan 11 2022 at 20:05):

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 (Jan 11 2022 at 20:06):

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 (Jan 11 2022 at 20:08):

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 (Jan 11 2022 at 20:08):

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

Reid Barton (Jan 11 2022 at 20:08):

Same in the additive context for semirings.


Last updated: Dec 20 2023 at 11:08 UTC