## Stream: Is there code for X?

### Topic: pull back an R module along S ->+* R

#### Scott Morrison (Aug 04 2020 at 09:46):

I was expecting for find something called map or comap that, given an R-module and a ring homomorphism from S to R, produced an S-module.

#### Scott Morrison (Aug 04 2020 at 09:46):

Anyone know where this is?

#### Kenny Lau (Aug 04 2020 at 09:46):

this will require generalizing docs#is_algebra_tower

Why is that?

#### Scott Morrison (Aug 04 2020 at 09:48):

That should only be about situations involving 3 rings. I only have two.

#### Markus Himmel (Aug 04 2020 at 09:48):

https://github.com/leanprover-community/mathlib/commit/bf43bffe6224560988775e29358d47e986bf0e6a#diff-426ea95b17d30988bbc8eb5e8dfbec76R225

#### Kenny Lau (Aug 04 2020 at 09:49):

the generalization is noting that in the definition we only need the transitive has_scalar instances

#### Scott Morrison (Aug 04 2020 at 09:49):

Perfect! I was just looking at src#ring_hom.to_semimodule, and wondering why what I wanted wasn't right there. :-)

#### Kenny Lau (Aug 04 2020 at 09:49):

what you proposed would make a scalar tower involving the two rings and the module

#### Scott Morrison (Aug 04 2020 at 09:49):

@Markus Himmel, is that commit part of some PR?

#### Kenny Lau (Aug 04 2020 at 09:50):

so to properly use it, we would need to generalize is_algebra_tower

#### Scott Morrison (Aug 04 2020 at 09:50):

oh, I see, you're doing it right now.

#### Scott Morrison (Aug 04 2020 at 09:51):

Okay. I just added ulift.semimodule_equiv, giving the R-linear equivalence between ulift M and M.

#### Scott Morrison (Aug 04 2020 at 09:51):

I was going to add the other equivalence, between M-as-a-ulift R-module, comapped via ulift.ring_equiv back to an R-module, and M itself.

but I won't :-)

#### Markus Himmel (Aug 04 2020 at 09:52):

Scott Morrison said:

oh, I see, you're doing it right now.

Yes, but I got sidetracked by trying to generalize the category of modules to take separate universe variables for the ring and the module. However, I'm afraid this doesn't work with the way concrete categories are set up.

#### Markus Himmel (Aug 04 2020 at 09:53):

Which is a shame, because I'd expect that all this ulift-juggling really shouldn't be necessary if we had these separate variables

#### Scott Morrison (Aug 04 2020 at 09:54):

Yes, I had a look at that a few days ago as well, and was sad. :-)

#### Markus Himmel (Aug 04 2020 at 09:56):

Is there an intrinsic reason for requiring large_category and putting C : Type (u+1) everywhere? Will something break if we releax it to category and C : Type v? My understanding of concrete categories and universe issues is very limited.

#### Scott Morrison (Aug 04 2020 at 11:17):

As far as I can recall right now, this was just done for simplicity, because most of the concrete categories are large categories.

#### Scott Morrison (Aug 04 2020 at 11:17):

Before universe inference worked as well as it does now, this probably saved a bunch of universe annotations.

#### Scott Morrison (Aug 04 2020 at 11:17):

But it may be that we can make it more flexible now at no cost.

#### Scott Morrison (Aug 04 2020 at 11:17):

But I think we'd have to just try.

#### Markus Himmel (Aug 04 2020 at 12:00):

I tried it, and the result is #3687

#### Reid Barton (Aug 04 2020 at 12:42):

Markus Himmel said:

Scott Morrison said:

oh, I see, you're doing it right now.

Yes, but I got sidetracked by trying to generalize the category of modules to take separate universe variables for the ring and the module. However, I'm afraid this doesn't work with the way concrete categories are set up.

I'd say it's not worth trying to support this. You'll end up paying the universe tax too many times.

#### Reid Barton (Aug 04 2020 at 12:43):

If you support this then you have no choice but to also support the case of u-modules over a v-ring where u < v, which is not an object of interest.

#### Markus Himmel (Aug 04 2020 at 12:48):

I'm note sure I understand what you mean. The non-category linear algebra section of mathlib supports this, and as far as I know it's not an issue.

#### Adam Topaz (Aug 04 2020 at 12:51):

I can think of some examples of this, e.g. of G is a group with universe v acting trivially on Z, then when you consider Z as a module over the group algebra...

#### Reid Barton (Aug 04 2020 at 12:52):

It does support it but I claim it's in fact basically useless

#### Reid Barton (Aug 04 2020 at 12:56):

Here is the next iteration of R-Mod vs Ab:

• R-Mod is a symmetric monoidal category in a way compatible with being an abelian category
• Ab is a symmetric monoidal category in a way compatible with being an abelian category
• :light_bulb: Let's exploit the equivalence between Ab and Z-Mod to reduce the second statement to the first one!
• Treat Ab.{v} as v-modules over the 0-ring Z
• Oh no, v-modules over a u-ring is only a symmetric monoidal category for v >= u (because the unit is u-sized not v-sized) and we have no way to express this in Lean.

#### Reid Barton (Aug 04 2020 at 12:58):

So now one could say "well technically, we could make max v u-modules over a u-ring into a symmetric monoidal category" by using ulift R as the unit object (while probably breaking universe inference because v does not appear on its own anywhere)

#### Reid Barton (Aug 04 2020 at 13:00):

but now this is an even worse situation than just assuming the rings and modules are in the same universe, because when v = u you have these stupid ulifts that won't just disappear

#### Johan Commelin (Aug 26 2020 at 12:12):

@Markus Himmel #3867 went off my radar due to holidays. Sorry for that. What do you think of Reid's comments above :up: ?

#### Markus Himmel (Aug 26 2020 at 12:33):

Johan Commelin said:

What do you think of Reid's comments above :up: ?

I certainly see the problem and I don't have a good solution. Personally, I believe that there is a possible compromise where we have independent universe variables but constrain them to be equal whenever we want to use that Module R is monoidal (indeed, this is exactly what #3687 does at the moment).

Last updated: May 17 2021 at 15:13 UTC