Zulip Chat Archive

Stream: general

Topic: Module refactor

Kenny Lau (Jan 08 2019 at 14:29):

I have refactored modules in order to make it possible for a module to be based on two rings. However, there is a small part in analysis/normed_space written by @Patrick Massot and @Johannes Hölzl which I do not know how to fix. I would be grateful if they could kindly offer their assistance.

Kenny Lau (Jan 26 2019 at 03:41):

I am rebasing it to the current mathlib; I would appreciate it if we could pause merging module-related stuff for a while (that would include my recent #625)

Kenny Lau (Jan 26 2019 at 03:41):

@Mario Carneiro do you think this is a good time?

Mario Carneiro (Jan 26 2019 at 03:42):

sure, what's the status?

Kenny Lau (Jan 26 2019 at 03:43):

expect a PR in 10 minutes

Kenny Lau (Jan 26 2019 at 03:46):

make that 1 hour

Kenny Lau (Jan 26 2019 at 04:38):

#626

Patrick Massot (Jan 26 2019 at 09:10):

I'm sorry I didn't find the right time to think about this thread. @Kenny Lau did you manage to fix your normed space issue?

Kenny Lau (Jan 26 2019 at 10:23):

yes

Kenny Lau (Jan 26 2019 at 11:38):

@Mario Carneiro pi_instance fails for smul because pi_instance tries to apply has_scalar.smul but it fails because the instance cannot be synthesized

Kenny Lau (Jan 26 2019 at 14:52):

  • The first parameters of has_scalar, semimodule, module, and vector_space are no longer out_params. The implication is that the base ring will have to be inferred either from being provided explicitly or from context.
  • The base ring of linear maps are now specified via β →ₗ[α] γ, alongside the original notation β →ₗ γ. A similar notation has been introduced for tensor products.
  • The base ring in some definitions/theorems are made explicit.

Kenny Lau (Jan 26 2019 at 14:52):

do you guys have any suggestions / objections?

Kenny Lau (Jan 26 2019 at 15:00):

@Kevin Buzzard

Kevin Buzzard (Jan 26 2019 at 20:09):

In real life one often sees phrases like "RR-linear maps from MM to NN" so I'm very happy. I live in a world where one often can consider both RR-linear and SS-linear maps between two modules.

Kenny Lau (Jan 26 2019 at 21:40):

I am rebasing it to the current mathlib; I would appreciate it if we could pause merging module-related stuff for a while (that would include my recent #625)

Kenny Lau, 2019 Jan 26 03:41 (UTC) :point_up:

I hope I didn't start a one-month module hiatus

Last updated: Dec 20 2023 at 11:08 UTC