pull back an R module along `S ->+* R`

Stream: Is there code for X?

[Scott Morrison]

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]

Anyone know where this is?

[Kenny Lau]

this will require generalizing docs#is_algebra_tower

[Scott Morrison]

Why is that?

[Scott Morrison]

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

[Markus Himmel]

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

[Kenny Lau]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Scott Morrison]

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

[Kenny Lau]

cf. src#is_algebra_tower.comap

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

but I won't :-)

[Markus Himmel]

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]

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]

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

[Markus Himmel]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

But I think we'd have to just try.

[Markus Himmel]

I tried it, and the result is #3687

[Reid Barton]

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]

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]

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]

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]

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

[Reid Barton]

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]

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]

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]

@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]

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