Zulip Chat Archive

Stream: Is there code for X?

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


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

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:46):

Anyone know where this is?

view this post on Zulip Kenny Lau (Aug 04 2020 at 09:46):

this will require generalizing docs#is_algebra_tower

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:48):

Why is that?

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:48):

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

view this post on Zulip Markus Himmel (Aug 04 2020 at 09:48):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 09:49):

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

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 09:49):

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:49):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 09:50):

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:50):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 09:50):

cf. src#is_algebra_tower.comap

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

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:51):

but I won't :-)

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

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 09:54):

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

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

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

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 11:17):

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 11:17):

But I think we'd have to just try.

view this post on Zulip Markus Himmel (Aug 04 2020 at 12:00):

I tried it, and the result is #3687

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

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

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

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

view this post on Zulip Reid Barton (Aug 04 2020 at 12:52):

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

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

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

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

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

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