Zulip Chat Archive

Stream: maths

Topic: tensor product of modules

Johan Commelin (Oct 08 2020 at 14:44):

@Scott Morrison @Markus Himmel I think that mathlib knows that R-modules are a monoidal category.

  • Does it know the Tensor-Hom adjunction?
  • I've shown that every module M is the union of its fin.gen. submodules. Can we now deduce (easily) that M \otimes N is the colimit of P \otimes N, where P ranges over the fin.gen submodules of M?

Johan Commelin (Oct 08 2020 at 14:49):

Application: branch flat-module

Johan Commelin (Oct 13 2020 at 13:35):

@Scott Morrison @Markus Himmel would one of you have time to help me a bit with this?

Johan Commelin (Oct 15 2020 at 06:52):

How far are we from having an internal hom for the category of modules? I guess this needs (self)-enriched categories, if we want to do it properly...

Kenny Lau (Oct 15 2020 at 06:54):

isn't M \rl[R] N already a module?

Johan Commelin (Oct 15 2020 at 06:54):

Yes, but it's not a functor

Johan Commelin (Oct 15 2020 at 06:55):

Module.of R (M \rl[R] N) is pretty usable locally, but doesn't really scale

Johan Commelin (Oct 15 2020 at 06:56):

I can define the functor easily:

  { obj := λ N, Module.of R (M →ₗ[R] N),
    map := λ N P f, linear_map.llcomp R M N P f,
    map_id' := by { intros X, ext1, dsimp at *, ext1, refl },
    map_comp' := by { intros X Y Z f g, refl } },

Johan Commelin (Oct 15 2020 at 06:56):

But if we want to do it the right way it probably needs to be generalised to a setting that I'm not that familiar with.

Bhavik Mehta (Oct 16 2020 at 14:17):

I'm sure I'm missing something but how does what you want differ from the cartesian closed (or monoidal closed) structure? Or is your question, how hard is it currently to define this structure

Johan Commelin (Oct 16 2020 at 15:28):

@Bhavik Mehta Does mathlib already have internal homs? I wasn't aware of this... but I sort of lost track of some of the stuff that happened.

Bhavik Mehta (Oct 16 2020 at 15:30):

mathlib has monoidal closed and cartesian closed categories

Bhavik Mehta (Oct 16 2020 at 15:32):

https://leanprover-community.github.io/mathlib_docs/category_theory/closed/monoidal.html

Bhavik Mehta (Oct 16 2020 at 15:33):

I could be wrong about if this is what you're looking for though

Johan Commelin (Oct 16 2020 at 15:34):

Yup, that looks good. Of course it would still be nice to have an internal hom that is defeq to linear_map R M N. But I don't need it for the application at hand.

Johan Commelin (Oct 16 2020 at 15:34):

Merci!

Johan Commelin (Oct 16 2020 at 15:34):

I didn't know we had this

Last updated: Dec 20 2023 at 11:08 UTC