Zulip Chat Archive

Stream: maths

Topic: tensor product of modules


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 08 2020 at 14:49):

Application: branch flat-module

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Oct 15 2020 at 06:54):

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

view this post on Zulip Johan Commelin (Oct 15 2020 at 06:54):

Yes, but it's not a functor

view this post on Zulip Johan Commelin (Oct 15 2020 at 06:55):

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

view this post on Zulip 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 } },

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Oct 16 2020 at 15:30):

mathlib has monoidal closed and cartesian closed categories

view this post on Zulip Bhavik Mehta (Oct 16 2020 at 15:32):

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

view this post on Zulip Bhavik Mehta (Oct 16 2020 at 15:33):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 16 2020 at 15:34):

Merci!

view this post on Zulip Johan Commelin (Oct 16 2020 at 15:34):

I didn't know we had this


Last updated: May 11 2021 at 15:12 UTC