ModuleCat.isModule not defeq

Stream: mathlib4

[Jon Eugster]

In the library ModuleCat has this comment about instances:

/-- The category of R-modules and their morphisms.

 Note that in the case of `R = ℤ`, we can not
impose here that the `ℤ`-multiplication field from the module structure is defeq to the one coming
from the `isAddCommGroup` structure (contrary to what we do for all module structures in
mathlib), which creates some difficulties down the road. -/
structure ModuleCat where
  /-- the underlying type of an object in `ModuleCat R` -/
  carrier : Type v
  [isAddCommGroup : AddCommGroup carrier]
  [isModule : Module R carrier]

Is there any way to work around these "difficulties down the road"? In particular I tried to define an isomorphism between the category of ℤ-Modules and the category of abelian groups

import Mathlib
universe u
open CategoryTheory

example : ModuleCat.{u} (ULift.{u} ℤ) ≅ Ab.{u} where
  hom := forget₂ (ModuleCat.{u} (ULift.{u} ℤ)) Ab.{u} |>.obj -- in here we have `ModuleCat.isModule`
  inv := (ModuleCat.of (ULift.{u} ℤ) ·) -- This implicitely uses `ULift.module`
  hom_inv_id := by
    ext ⟨A⟩
    rw [types_id_apply, types_comp_apply, @ModuleCat.forget₂_obj]
    -- From now on it's all debugging
    change ModuleCat.of (ULift ℤ) ↑(AddCommGroupCat.of ↑(ModuleCat.mk A)) = ModuleCat.mk A
    change ModuleCat.of (ULift ℤ) ↑(AddCommGroupCat.of A) = ⟨A⟩
    have : ModuleCat.of (ULift ℤ) A = ⟨A⟩
    · rfl
    convert this
    -- THIS SUCKS
    sorry -- ULift.module = isModule✝
    done
  inv_hom_id := by
    ext (A : Ab.{u}) --BUG? When I do `ext A` instead, I get `A : ?α` when I hover over it.
    simp?
    sorry

I tried to read the file's docstring, but I'm not quite sure what to do. I guess the inverse inv does not work like that because it uses ULift.module which will eventually not be defeq to the instance bundled into an A : ModuleCat

[Yury G. Kudryashov]

Do we have an ext for ModuleCat?

[Yury G. Kudryashov]

It should say that projections to AddCommGroupCat and SMul.smul agree.

[Yury G. Kudryashov]

Then you can use docs#zsmul_eq_smul_cast

[Yury G. Kudryashov]

See also docs#AddCommGroup.intModule.unique

[Yury G. Kudryashov]

You may need a version with ULift Int

[Yury G. Kudryashov]

BTW, why not use modules over Int, not ULift Int?

[Yury G. Kudryashov]

Then you can have a generic isomorphism between modules over R and ULift R (or, more generally, modules over two isomorphic rings), if needed.

[Jon Eugster]

Yury G. Kudryashov said:

BTW, why not use modules over Int, not ULift Int?

I mean I used that because we have an instance #synth MonoidalCategory <| ModuleCat.{u} (ULift.{u} ℤ) which I wanted to transport to Ab.{u} using Monoidal.transport, but you're saying I should start from ModuleCat.{u} ℤ?

We do not have an instance #synth MonoidalCategory <| ModuleCat.{u} ℤ yet though.

[Jon Eugster]

Yury G. Kudryashov said:

See also docs#AddCommGroup.intModule.unique

Thanks, havent had this result on the radar

[Jon Eugster]

Yury G. Kudryashov said:

Do we have an ext for ModuleCat?
It should say that projections to AddCommGroupCat and SMul.smul agree.

Hmm wouldn't know of it, but that means nothing

[Yury G. Kudryashov]

docs#AddCommGroup.intModule.unique lets you prove that two docs#Module over docs#Int are equal. You should add a similar lemma about docs#ModuleCat

[Jon Eugster]

Ill try, thanks!

[Jon Eugster]

So I got this working with @Yury G. Kudryashov 's hint to use AddCommGroup.intModule.unique :tada:

Now, is there a fundamental reason I should generally work with ModuleCat.{u, 0} ℤ instead of ModuleCat.{u, u} (ULift.{u, 0} ℤ)? As mentioned, I only used the latter because it has all the instances I need, while they are missing for the former. But am I right that the difference between the two is purely tautological?

So would it be better if I added all the instances I need for ModuleCat.{u, 0} ℤ copying/generalising what there is for ModuleCat.{u, u} (ULift.{u, 0} ℤ)?

[Yury G. Kudryashov]

I suggest that you construct your isomorphism for ULift Int in two steps:

• the existing isomorphism for Int;
• isomorphism between module categories over isomorphic rings.

[Yury G. Kudryashov]

Note: I know nothing about category theory in mathlib.

[Kevin Buzzard]

I would not make data-carrying instances on a category by saying "oh these instances are already on some equivalent category, I'll just push them over"; I would define the data directly and then copy over the proofs.

[Jon Eugster]

Kevin Buzzard said:

I would not make data-carrying instances on a category by saying "oh these instances are already on some equivalent category, I'll just push them over"; I would define the data directly and then copy over the proofs.

Hmm, concretely the tensor product for ℤ-modules (in mathlib) is the one coming from linear maps: ModuleCat.of R (M ⊗[ℤ] N) and I'd hoped that the transport would end up being the same thing. If I defined the tensor product of abelian groups directly, I'd probably still define it by regarding my group as ℤ-module. Is there a more direct way?

Are you therefore suggesting that docs#CategoryTheory.Monoidal.transport should generally not be used?

[Kevin Buzzard]

Perhaps @Amelia Livingston has something to add, but this was something I learnt from her: I think she tried using this to move a monoidal category structure between two categories in representation theory and ended up refactoring later because it was just hard to use. If the transport really is "the same thing" and rfl can prove it then maybe it's OK. But "the same thing" can mean all sorts of other things too.

[Jon Eugster]

I see. So I'll read up on what we actually want the tensor product of abelian groups to look like and see if that's defeq to the defined transport

[Kevin Buzzard]

I think that would be a wise way to start thinking about this design decision

[Amelia Livingston]

I think transporting a monoidal structure across an equivalence can be okay, certainly if it gives a structure defeq to what you want. It was transporting a monoidal closed instance across an equivalence that ended up very slow for me.
A complication in this instance is that the equivalence between ℤ-modules and abelian groups is defined by showing that the forgetful functor is full, faithful and essentially surjective instead of constructing an explicit inverse, so the ℤ-module corresponding to an abelian group X isn't definitionally isomorphic to ModuleCat.of ℤ X. Edit: I was talking about the mathlib equivalence - yours looks like it might be nicer to transport.

[Jon Eugster]

That's a good heads up, thanks!

Mines now this: which is sorry-free:

def moduleCat_int_equiv_ab : ModuleCat.{u} ℤ ≅ Ab.{u} where
  -- data
  hom := forget₂ (ModuleCat.{u} ℤ) Ab.{u} |>.obj
  inv := (ModuleCat.of ℤ ·)
  -- props
  hom_inv_id := by
    -- TODO: Golf this proof
    ext ⟨A⟩
    rw [types_id_apply, types_comp_apply, @ModuleCat.forget₂_obj]
    change ModuleCat.of ℤ ↑(AddCommGroupCat.of ↑(ModuleCat.mk A)) = ModuleCat.mk A
    change ModuleCat.of ℤ ↑(AddCommGroupCat.of A) = ⟨A⟩
    have : ModuleCat.of ℤ A = ⟨A⟩
    · rfl
    convert this
    -- Here we use that all instances `Module ℤ A` are identical
    have g := AddCommGroup.intModule.unique (M := A) |>.uniq
    rw [g <| AddCommGroup.intModule ↑(AddCommGroupCat.of A)]
    rename_i a _b _c
    rw [g a]
    done
  inv_hom_id := by
    ext ⟨A⟩
    rw [types_id_apply, types_comp_apply, @ModuleCat.forget₂_obj]
    rfl

in particular, I think both hom and inv are just re-bundling things in an explicit way. Therefore I was hopeful that things should be reasonably close to being defeq.

I thought about redefining the tensor product on abelian groups (monoids) but I'm a bit reluctant to copy that much API just to remove

  | of_smul : ∀ (r : R) (m : M) (n : N), Eqv (.of (r • m, n)) (.of (m, r • n))

in the equivalence relation defining the tensor product :thinking: