module vs submodule extending monoids

Stream: new members

[Martin C. Martin]

module does NOT extend add_comm_group:

@[ext, protect_proj] class module (R : Type u) (M : Type v) [semiring R]
  [add_comm_monoid M] extends distrib_mul_action R M :=

Yet submodule DOES extend add_submonoid:

structure submodule (R : Type u) (M : Type v) [semiring R]
  [add_comm_monoid M] [module R M] extends add_submonoid M, sub_mul_action R M : Type v.

Why this difference?

[Eric Wieser]

The "don't extend things with different number of parameters" rule only applies to class not structure

[Jireh Loreaux]

And Martin, the reason is that Lean doesn't do type class inference on structures, only on classes. So the issue I mentioned in the other thread never arises.

[Martin C. Martin]

Ah thanks to both of you!

So why don't we want type class inference on submodules? i.e. why is submodule a structure when module is a class? I guess submodule.module is the most useful structure, and submodule itself isn't used much?

Any guidance on when to use structure and when class?

[Eric Wieser]

What would you want example : submodule ℝ (ℝ × ℝ) := by apply_instance to find?

[Eric Wieser]

class should be used when by apply_instance makes sense, and it only makes sense when there's only one reasonable thing for it to produce

[Eric Wieser]

By comparison, example : module ℝ (ℝ × ℝ) := by apply_instance has an obvious answer; it finds the module defined by c • (x, y) = (c • x, c • y)

[Martin C. Martin]

Ah, because the carrier isn't a type, but rather a field.

[Martin C. Martin]

(Sorry, "field" in the sense of programming, not abstract algebra. :) )

[Jireh Loreaux]

Yes, note that submodule R M is the type of R-submodules of an R-module M, not a specific submodule. For that, a term of that type, namelyS : submodule R M, is what you want.

[Jireh Loreaux]

However, note that submodules can themselves be viewed as modules via docs#submodule.module. In doing this, the term S : submodule R M is promoted to a type ↥S (where the arrow comes from a docs#has_coe_to_sort instance).

[Jireh Loreaux]

This is somewhat backwards compared to the way textbooks usually introduce subobjects. A textbook generally says "a submodule is a subset which is also a module with the inherited operations", and then the book proves a lemma of the form: "a subset closed under + and • and containing 0 is a submodule". In Lean, we completely reverse this, and I think it's actually more sensible (because a term of type docs#submodule always carries around a reference to the ambient type, as it should).

[Martin C. Martin]

I agree. In practice, it's much more common to use the conditions to show your subset is indeed a subspace, rather than the other way around. At least from my hazy memory from years ago. :)

[Martin C. Martin]

Next question: why does subsemigroup take a magma and not a group? It seems it's possible to construct a subsemigroup where the operation isn't associative, and therefore isn't actually a semigroup?

[Martin C. Martin]

Is this like the module/vector space distinction, where once we define a module, no other definition is needed for a vector space, because it's just a restriction on R and doesn't change the module stuff?

[Jireh Loreaux]

Indeed, it's just because we think of subsemigroups as the more common use case, and thus they should inherit the name as opposed to submagma.