## 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.

Merci!

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

I didn't know we had this

Last updated: May 11 2021 at 15:12 UTC