Base change for modules over an algebra

Stream: Is there code for X?

[Stepan Nesterov]

If $A$ is a $k$-algebra, and $M$ is an $A$-module, I would like to consider, for a $k'$-algebra $k$, the $k'$-module $k' \otimes_k M$ as a $k' \otimes_k A$ module via $(\lambda \otimes a) (\mu \otimes m) = \lambda \mu \otimes a m$. Is there an easy way to do this?

import mathlib

open scoped TensorProduct

variable (k A M : Type*) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid M]
    [Module A M] [Module k M] [IsScalarTower k A M]
variable (k' : Type*) [CommRing k'] [Algebra k k']

#synth Module (k' ⊗[k] A) (k' ⊗[k] M) -- fails

[Kevin Buzzard]

(typo $k$-algebra $k'$)

[Kevin Buzzard]

Do we already have an $A$-action on $k'\otimes_kM$? If so then you're in trouble with the mathlib diamond mafia because $M=k'\otimes_kA$ is allowed in your setup. Conversely if we don't then your construction will make it never to be allowed if yours makes it into mathlib. This sort of nonsense needs a robust solution because it's blocking progress.

[Kevin Buzzard]

In FLT I've been taking the opposite approach and just making actions when I need them and disabling them otherwise and this has simultaneously enabled me to prove theorems and confuse other users

[Andrew Yang]

docs#TensorProduct.Algebra.module should be useful here.

[Kevin Buzzard]

Well yes if you want to define it locally, but not if you want this in mathlib, because given an $A$-action on $M$, mathlib will not allow an $A$-action on $k'\otimes_kM$ because what if $k'=M$ as well?

It's these objections which I think are creating a barrier to growth in algebra which I think is becoming more and more unsustainable. I found it impossible to stick to Mathlib's rules about what can and can't be made an instance when I wanted to develop enough theory to write down the isomorphism $L\otimes_K\mathbb{A}_K\cong\mathbb{A}_L$ in a way which is both $L$-linear and $\mathbb{A}_K$-linear and also a topological isomorphism for the $\mathbb{A}_K$-module topologies, which is why I just gave up in FLT and allowed instances which would not be allowed in mathlib; it didn't matter because we put them in a scope, ultimately things compiled, we used them to deduce finiteness results and then you can use the finiteness results without opening the scope (the entire theory was developed just so I could prove results about $\mathbb{A}_K$ by reducing them to results about $\mathbb{A}_\mathbb{Q}$ where explicit computations were much easier; we then turn the instances off again). I know it's a hack but I don't know of a mathlib-certified way to proceed with these kinds of questions.

[Kevin Buzzard]

@Stepan Nesterov the answer to your question is "is there an easy way to do this" is "it depends on where your work is going". If you are just making it locally, then make the instance if it's not there using Andrew's hint. If you want it in FLT then it's a bit easier: just import FLT.Hacks.RightActionInstances and open scoped TensorProduct.RightActions to get the action of $A$ on $k'\otimes_kM$ and then use Andrew's suggestion. If you want to get it into mathlib then you either have to battle the diamond mafia, solve a hard problem (analogous to https://github.com/leanprover-community/mathlib4/issues/7152) or do something completely different like e.g. making a new kind of action map or something (again probably not feasible without solving a hard problem) or completely rethinking how actions work in mathlib. I am very unclear about how to proceed.

[Kevin Buzzard]

I think one way of making progress is asking the simplest form of the question. If $k'$ is a commutative $k$-algebra then $k'\otimes_kk'$ admits two natural left actions of $k'$ and they are different. We cannot close our eyes to the fact that mathematicians want both (and want to talk about maps which are linear wrt to one or the other of the actions etc). In a paper where both are used, different notations would be used. But we only have one way of saying "X acts on Y". What do we do? A type synonym def ActingOnTheRightOfTensorProducts (R : Type*) [CommRing R] := R?

[Sébastien Gouëzel]

You can have two different scopes with the two different actions, none of them active by default. I think that in general it's the right thing to do for instances that could create diamonds like the other one you mention above: have them only in scopes, and activate them locally when it's useful.

[Kevin Buzzard]

Well $k'\otimes_kk'$ is already a $k'$-algebra in mathlib in no scope, it's docs#Algebra.TensorProduct.leftAlgebra

[Artie Khovanov]

(Thinking out loud)
To robustly solve the problem Kevin is describing of having too many actions, we need some way of having multiple smul instances without them clashing. Perhaps we could dynamically register a list of syntactically distinct smuls? Like, copy the way it's done in informal maths and allow defining "clashing" smul instances with different notation but the same API (within a scope). Then we can write common instances of this pattern (eg tensor product) in more generic scopes. So we would end up with •ₗ and •ᵣ available and it would all elaborate/deliberate nicely to/from the more generic smul instances. I do not know how technically difficult this would be to do.

[Aaron Liu]

Kevin Buzzard said:

I think one way of making progress is asking the simplest form of the question. If $k'$ is a commutative $k$-algebra then $k'\otimes_kk'$ admits two natural left actions of $k'$ and they are different.

Objection: one of them is a right action

[Michael Stoll]

This reminds me of #mathlib4 > Too many 'Smul's @ 💬 (see also #mathlib4 > SMul diamond on subsets @ 💬, where it turned out that some diamonds are more equal than others...)

[Kevin Buzzard]

Aaron Liu said:

Kevin Buzzard said:

I think one way of making progress is asking the simplest form of the question. If $k'$ is a commutative $k$-algebra then $k'\otimes_kk'$ admits two natural left actions of $k'$ and they are different.

Objection: one of them is a right action

No good. I definitely want to allow linear maps $k'\otimes_kk'\to M$ where $M$ is a left $k'$-module and $k'\otimes_kk'$ has the right action of $k'$. Why? Because if we can't do arbitrary things then mathematicians are going to say "it's broken". And what about $k'^{op}\times_kk'$ etc?

I do not believe that we can just attempt to solve this general problem by left actions by R^{op} or right actions. I like the idea of scoping all decisions and seeing how far this gets us; the problem is that a lot of our actions are not in a scope.

[Stepan Nesterov]

Kevin Buzzard said:

Stepan Nesterov the answer to your question is "is there an easy way to do this" is "it depends on where your work is going". If you are just making it locally, then make the instance if it's not there using Andrew's hint. If you want it in FLT then it's a bit easier: just import FLT.Hacks.RightActionInstances and open scoped TensorProduct.RightActions to get the action of $A$ on $k'\otimes_kM$ and then use Andrew's suggestion. If you want to get it into mathlib then you either have to battle the diamond mafia, solve a hard problem (analogous to https://github.com/leanprover-community/mathlib4/issues/7152) or do something completely different like e.g. making a new kind of action map or something (again probably not feasible without solving a hard problem) or completely rethinking how actions work in mathlib. I am very unclear about how to proceed.

What I wanted to do is to prove that an absolutely irreducible representation of an abelian group is 1-dimensional. Then I thought then the right generality for this is you take a commutative k-algebra A, and say that an absolutely simple module (not sure if this is the standard terminology) is 1-dimensional. But then I ran into an issue that I don't know how to define this action of a base changed algebra on a base changed module.

[Kevin Buzzard]

Just do the base change on the other side?

[Stepan Nesterov]

Like this?

import mathlib

open scoped TensorProduct

variable {k A M : Type*} [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid M]
    [Module A M] [Module k M] [IsScalarTower k A M]
variable {k' : Type*} [CommRing k'] [Algebra k k']

#synth Module (A ⊗[k] k') (M ⊗[k] k')

It still fails

[Stepan Nesterov]

But it's true that we do need this result (absolutely irreducible representation of an abelian group is 1-dimensional) in FLT, for example, for proving the main theorem in ModThree.lean. If someone were to try and PR this result into FLT, would you prefer that they do the 'module over the commutative algebra' version, which we don't need for FLT but it's morally correct, or just the group version?

[Stepan Nesterov]

Or if mathlib doesn't have a way of base changing modules, does it mean that I should just PR the group version in mathlib, and not worry about the generalization?

[Andrew Yang]

You could also do Module (A ⊗[k] k') ((A ⊗[k] k') ⊗[A] M) if you want to delay the problem to later but again I don't think it is unreasonable to add this as a local instance to mathlib via docs#TensorProduct.Algebra.module

[Kevin Buzzard]

It causes a diamond if $M=A\otimes_kk'$ right? (even if it's this way around)

[Andrew Yang]

Module (A ⊗[k] k') ((A ⊗[k] k') ⊗[A] M) should be unambiguous.
But Module (A ⊗[k] k') (M ⊗[k] k') indeed clashes with other instances so it should be scoped/local.

[Kevin Buzzard]

I feel like we have a big problem to solve here but for FLT if you can get away with the group version then that'll do for now!

[Aaron Liu]

Kevin Buzzard said:

I definitely want to allow linear maps $k'\otimes_kk'\to M$ where $M$ is a left $k'$-module and $k'\otimes_kk'$ has the right action of $k'$. Why? Because if we can't do arbitrary things then mathematicians are going to say "it's broken".

We also don't have a way to directly do a group homomorphism from a multiplicative group to an additive group, you have to make the multiplicative group additive or make the additive group multiplicative. I think we can try a similar thing.

[Aaron Liu]

Kevin Buzzard said:

And what about $k'^{op}\times_kk'$ etc?

What about it?

[Kevin Buzzard]

Aaron Liu said:

I think we can try a similar thing.

Kevin Buzzard said:

def ActingOnTheRightOfTensorProducts (R : Type*) [CommRing R] := R?

:point_up: ?

[Aaron Liu]

no, I mean add a thing that swaps the left and right actions in general

[Aaron Liu]

not just specifically for tensor products

[Aaron Liu]

but I guess if you only need it on tensor products for now then that's fine too

[Antoine Chambert-Loir]

Note that one might genuinely wish to compare actions of the same object A on the same object B. The proof of the Skolem-Noether theorem works like this.

[Eric Wieser]

I don't think in those cases it is important that the objects are type-theoretically the same: you can always compare how fooAct A acts on B with how A acts on B, especially when fooAct is an isomorphism to a type synonym

[Eric Wieser]

With the scoping approach you can also write something like (open scoped Act1 in A • B) = (open scoped Act2 in A • B)

[Eric Wieser]

Note that scopes only go so far; when it comes to inheriting actions, scopes are like saying "you can follow every edge of this color in my graph", not "you must follow this precise path"

[Kevin Buzzard]

The elephant in the room here is that there is already an action of $A$ on $A\otimes A$ and it's not in a scope.

[Andrew Yang]

I don't think this is solvable at all (nor do I really think this is an issue). You already need to choose how $R$ acts on $M \otimes N$, via $r \cdot (a \otimes b) = (r \cdot a) \otimes b$ or $a \otimes (r \cdot b)$, which are not defeq. By choosing one you also choose which action $A$ on $A \otimes A$ should be.

[Kevin Buzzard]

Sure, but one could scope both choices rather than forcing everyone to have to deal with (or sometimes avoid) one of them.

[Andrew Yang]

Are you proposing that $M \otimes_R N$ should not be an $R$-module globally?

[Stepan Nesterov]

Kevin Buzzard said:

The elephant in the room here is that there is already an action of $A$ on $A\otimes A$ and it's not in a scope.

For $A$ commutative or in general?

[Stepan Nesterov]

If for general $A$, then I would agree that this seems undesirable

[Eric Wieser]

The extreme outcome here is also that $R$ is not an $R$-module globally

[Stepan Nesterov]

Is is possible to create a situation, where, e.g. $R$ is not an $R$-module golbally, but something like $R^{\mathrm{Fin} 1}$ is an $R$-module globally? So you can talk about $R$ as an $R$-module, but you'd have to write like a few extra symbols.

Eric Wieser said:

The extreme outcome here is also that $R$ is not an $R$-module globally

[Stepan Nesterov]

Or in my original situation, can you create a separate notation like M.BaseChange k' which is defeq to the tensor product, and then have M.BaseChange k' be an A.BaseChange k'-module, but not have all the other instances for this particular notation? Or does Lean see through defeqs?

[Andrew Yang]

I still don't understand why can't you just make the instance and turn it on locally.

[Stepan Nesterov]

Because as far as I understood, Kevin thinks it's not mathlib-approved (?)

[Stepan Nesterov]

It's possible I am misinterpreting how serious this all is

[Stepan Nesterov]

Well and also there's way too much 'failed to synthesize errors' when I try to just apply TensorProduct.Algebra.module and maybe it's all fixable with some hacks from the FLT project but I gave up after a few tries

[Andrew Yang]

Something like

open TensorProduct

abbrev baseChangeModule : Module (k' ⊗[k] A) (k' ⊗[k] M) :=
  let : Module A (k' ⊗[k] M) := (TensorProduct.comm _ _ _).toAddEquiv.module _
  have : IsScalarTower k A (k' ⊗[k] M) := .of_algebraMap_smul fun _ x ↦ by
    induction x <;> simp_all [this, ← tmul_smul, ← @IsScalarTower.algebraMap_smul k A M,
      -algebraMap_smul]; rfl
  have : SMulCommClass k' A (k' ⊗[k] M) :=
    ⟨fun _ _ x ↦ by induction x; exacts [by simp, rfl, by simp_all]⟩
  TensorProduct.Algebra.module

attribute [local instance] baseChangeModule

But those lets and haves should be their own scoped instances, generalizing what Kevin has in the hacks file.

[Aaron Liu]

Andrew Yang said:

Are you proposing that $M \otimes_R N$ should not be an $R$-module globally?

I don't see how $M \otimes_R N$ is always an R-module, unless one of M or N is an R-bimodule, which happens for example when R is commutative.

[Andrew Yang]

$M \otimes_R N$ in this context means that $R$ is commutative because of how docs#TensorProduct is defined. If you need tensor products over non-commutative rings this is another can of worms which is tangential to this discussion.

[Andrew Yang]

I think the only thing in this thread that cannot be solved with scoped instances is when you want $A \otimes A$ to be an $A$-algebras in two ways at once, e.g. when you want to talk about the $A$-linear map $A \otimes A \to A \otimes A, a \otimes b \mapsto b \otimes a$ (where the $A$ act on different sides on the two tensor products).
The only way to do this is that I am aware of is to use @SemilinearMap and fill in the instances manually, which is very bad.

[Aaron Liu]

Andrew Yang said:

If you need tensor products over non-commutative rings this is another can of worms which is tangential to this discussion.

I feel like distinguishing the left and right actions would solve many problems here though...

[Andrew Yang]

I feel like there are lots of problems you need to solve first before you get to solve the problems listed here.

[Andrew Yang]

And in the end you don't get two algebra instances of $A$ on $A \otimes A$; you get none.

[Aaron Liu]

you at least get two A-modules I think

[Aaron Liu]

so you can talk about left- and right- A-linear maps

[Kevin Buzzard]

Yes, the point is that $A\otimes A$ is an $A$-module (and an $A$-algebra) in two different ways, and right now one of them is being forced on us, and I'm saying that this is quite inconvenient when you want the other one.

[Andrew Yang]

Do you want "the other one" or do you want both of them at once?
For the former, does attribute [local instance] TensorProduct.rightAlgebra solve the problem?
For the latter I have no solution and perhaps this is a fundamental limitation of typeclasses?
You can introduce typeclass synonyms that partially solves the problem (e.g. if you can allow "different" $A \otimes A$ then you do a typeclass synonym on tensor product that always does right action; if you can allow "different" $A$ acting on the same tensor product then you could do def Copy := R and work with A ⊗ Copy A), but nothing satisfactory.

[Kevin Buzzard]

It's not really what I want -- it's what it would not be unreasonable for a mathematician to want, in general. Obviously it's becoming clear that there are these random reasons why one can't have certain instances because of some exotic special case causing a diamond, and I think that this might become complicated to deal with in the future. Observations like Eric's "Oh SMul X Y -> SMul (F X) (F Y) is a bad idea" might be some theoretically true statement about how mathlib has got algebra set up, but this has concrete consequences such as "if K and L are number fields and L is a K-algebra then $\mathbb{A}_L$ is not allowed to be an $\mathbb{A}_K$-algebra in mathlib unless you switch it on locally and then be super-wary about the case K=L because it will cause time-outs". Similarly here we're basically saying that $A\otimes A$ is only allowed to be an $A$-algebra in one way and whilst we've worked around this so far, this is not something which a mathematician is going to expect to be hearing.

[Kevin Buzzard]

But to get back to the point, the answer to Stepan's question is "yes you can make this module instance (thanks Andrew for doing it), there might be technical reasons why it's not allowed to be a global instance but if you just switch it on locally and cross your fingers you'll probably be OK".

[Kevin Buzzard]

I'll remark that allowing $M\otimes N$ to be an $A$-module if $N$ is an $A$-module has not caused me any problems yet; what has caused me problems is $\mathbb{A}_L$ being an $\mathbb{A}_K$-algebra and also letting $\mathbb{A}_L$ be a $K$-algebra because then you get two $K$-actions on $\mathbb{A}_K$. So there are some design patterns I'm learning to avoid and perhaps this is how things will go in the future; you carefully switch things on and hope for the best.

[Stepan Nesterov]

Can you do something like bundled modules in mathlib? Like saying “Let WithRightAction A be an A-module with carrier A otimes A and action on the right” without making an instance?

[Yaël Dillies]

Kevin Buzzard said:

what has caused me problems is $\mathbb{A}_L$ being an $\mathbb{A}_K$-algebra and also letting $\mathbb{A}_L$ be a $K$-algebra because then you get two $K$-actions on $\mathbb{A}_K$.

I thought I had solved this specific problem?

[Yaël Dillies]

IIRC it was due to there being a special $K$-algebra instance on $\mathbb A_K$ on top of the generic $K$-algebra instance on $\mathbb A_L$ for $L$ a $K$-algebra.

[Yaël Dillies]

... but your description of the situation doesn't contain the first instance, so either your description is wrong or it is incomplete or the problem does not exist anymore.

[Yaël Dillies]

I will remark that the main alternative to typeclasses that we know of is locales, ans turning on and off instances is more or less what a locale is. The two differences I can see are

1. It's possible (and easy!) to turn on and off a locale for specific types, while instances can only be turned on and off for all types at once (unless you redeclare them one by one for the specific types you want them to be on on, which is NOT easy).
2. It's possible to change the notation of a locale to use two conflicting locales on the same type. Meanwhile, conflicting instances are a no-go, except in a few places like measure theory where we have spent a lot of time making the API usable for non-canonical instances.

[Yaël Dillies]

I personally believe that locales are a more accurate representation of mathematician thinking than typeclasses, and this thread is screaming "Please someone implement locales in Lean" to me. I foresee a few issues though:

1. Although locales have been successfully used in other libraries, such as Isabelle/HOL, said libraries are nowhere close to where mathlib is in terms of eg commutative algebra, and therefore it is unclear whether the success of locales will continue when the harder parts of commutative algebra are reached.
2. The typeclass system is unlikely to change again in Lean.

[Yaël Dillies]

To me, this means a potential implementation of locales would need to be a lightweight system over the existing instance system, and would need to first be tried out in the advanced commutative algebra projects like FLT.

[Yaël Dillies]

A potential implementation I envision is the combination of:

1. an attribute putting instances in a locale
2. a tactic to turn on the instances tagged with a locale's attribute on a given type locally to a proof
3. a command to turn on the instances tagged with a locale's attribute on a given type locally to a file

[Yaël Dillies]

Note that open scoped fits the bill, except for the "on a given type" constraint

[Yaël Dillies]

I would love to be involved in implementing such a design, because I have Thoughts, but I am too busy to do it by myself.