Definition of module

Stream: mathlib4

[Qi Ge]

Hi all, consider the following definition of modules

import Mathlib.Algebra.Category.Ring.Basic
import Mathlib.GroupTheory.GroupAction.Defs

class Module' (R : Type u) [Semiring R] (M : Type v) where
  isAddCommMonoid : AddCommMonoid M
  isDistribMulAction : DistribMulAction R M
  add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
  zero_smul : ∀ x : M, (0 : R) • x = 0

This allows us to use the Blundled APIs to construct the concrete category of modules in analogy to that of other algebraic stuctures

import Mathlib.CategoryTheory.ConcreteCategory.Bundled
open CategoryTheory
def ModuleCat' (R : Type u) [Semiring R] := Bundled (Module' R)

However one drawback is that it breaks the inheritance of Module' to DistribMulAction, is there other reasons why it shouldn't be done this way?

[Patrick Massot]

This is explained in https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html

[Qi Ge]

I understand why DistribMulAction and (for that nature AddCommMonoid) cannot be inferred from a module defined this way, but my point is exactly that! I think Blundled captures well the algebraic hierarchy of "sets with extra structures", and gives a natural way to construct their concrete categories and forgetful functors via CategoryTheory.BundledHom.mkHasForget₂. And thus shouldn't the typeclass for module be made to work with Bundled?

[Adam Topaz]

@Qi Ge As Patrick says there's a good reason why the AddCommMonoid instance is not bundled as part of the Module class, specifically because it would cause lengthy typeclass searches. That means that, unfortunately, you can't use the Bundled construction to construct the category of modules, but it's easy enough to make a bespoke structure for the category of modules (which is indeed what's done in the definition of docs#ModuleCat ).

[Adam Topaz]

Besides, I think that Bundled isn't as useful in Lean4 as it used to be in Lean3, and this has caused difficulties issues when porting some files involving algebraic categories.

[Qi Ge]

ModuleCat is more or less doing exactly the bundled approach above. What motivates my question is that it feels to me there are too many non-mathematical bookkeeping defeq lemmas dealing with coercion in Mathlib.Algebra.Category.ModuleCat.Basic. When I'm thinking about having a group acting on a ring and its module (and possibly topology comes into play) there is a long chain in the hierarchy, it seems highly inefficient having to add all the lemmas to make simplifiers work well(?) and I was hoping that Bundled reduces some redundancy. (I haven't really think this through though so maybe this is also not the case.)

[Adam Topaz]

It's probably correct to think of the algebraic categories as just wrappers around the algebraic constructions using the typeclass system. These wrappers are mostly just there so that the algebraic categories can interact with other categories and the category theory library in general. When you do actual algebra, you mostly just deal with types and classes, not categories. It's important to be able to go back and forth between the two approaches though, which is where all these boilerplate lemmas come into play.

[Qi Ge]

Imagine having to show that forgetful functor and "going to typeclass" need to commute with one another, on both objects and morphisms in a long of hierarchy... I hoped there is some elegant "functorial" way to construct categories from typeclasses. Sad to see that category really is hard :smiling_face_with_tear:

[Adam Topaz]

So if you have a group G and a ring R with a G-action, as well as an R-module with a compatible G action (as in the case of Galois representations that you know), then the right approach is probably to start by defining the typeclass, keeping in mind what's written in the section of mathematics in lean that Patrick mentioned since now there are three type parameters, and only then define the category.

[Adam Topaz]

What do you mean by "going to typeclass"? In practice the commutativity of all such things should be true "by rfl" if things are set up correctly.

[Qi Ge]

I have constructed the category of rings with group action with existing type class. I was trying to cheat with docs#Action and just showing that they are equivalent requires many of the rfl lemma. it feels messy. Maybe it just takes some getting used to it.

[Adam Topaz]

Aha, okay in this case I can imagine things getting tedious because you're going from category theory to algebra, whereas the rest of the library goes the other way around :)

[Kevin Buzzard]

In group cohomology we have to go in both directions and it's not always plain sailing