Ideals in tensor product of algebras

Stream: Is there code for X?

[Antoine Chambert-Loir]

If $f \colon A \to B$ is a morphism of $R$-algebras, and $I$ is an ideal of $B$, then the ideal generated by $I$ in $A \otimes_R B$ can be described as the image of $A \otimes_R I$.
This is not absolutely trivial but the following proof is way too big compared to what it should be.
Do you have ideas for how to golf it?

import Mathlib.LinearAlgebra.TensorProduct
import Mathlib.RingTheory.TensorProduct

local notation:100 M " ⊗[" R "] " N:100 => TensorProduct R M N

variable {R : Type _} [CommSemiring R]
  {A B : Type _} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
  (I : Ideal B)

example :
  (I.map (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B)).restrictScalars R =
    LinearMap.range (LinearMap.lTensor A (Submodule.subtype (I.restrictScalars R))) := by
  let J : Ideal (A ⊗[R] B) := {
    carrier := LinearMap.range (LinearMap.lTensor A (Submodule.subtype (I.restrictScalars R)))
    add_mem' := fun {x} {y} hx hy  ↦ Submodule.add_mem _ hx hy
    zero_mem' := by
      simp only [SetLike.mem_coe]
      apply zero_mem
    smul_mem' := fun x y ↦ by
      simp only [SetLike.mem_coe]
      rintro ⟨y, rfl⟩
      induction x using TensorProduct.induction_on with
      | zero =>
          rw [zero_smul]
          apply zero_mem
      | tmul a b =>
          induction y using TensorProduct.induction_on with
          | zero =>
              rw [map_zero]
              apply zero_mem
          | tmul x y =>
              simp only [LinearMap.lTensor_tmul, Submodule.coeSubtype, smul_eq_mul, tmul_mul_tmul]
              suffices h : b * ↑y ∈ Submodule.restrictScalars R I
              use (a * x) ⊗ₜ[R] ⟨b * ↑y, h⟩
              rfl
              simp only [Submodule.coe_restrictScalars, Submodule.restrictScalars_mem]
              apply Ideal.mul_mem_left
              exact y.prop
          | add x y hx hy =>
              rw [map_add, smul_add]
              exact Submodule.add_mem _ hx hy
      | add x x' hx hx' =>
          rw [add_smul]
          exact Submodule.add_mem _ hx hx' }
  suffices : Ideal.map includeRight I = J
  rw [this]
  rfl
  -- Ideal.map includeRight I = J
  apply le_antisymm
  · rw [Ideal.map, Ideal.span_le]
    rintro x ⟨b, hb, rfl⟩
    simp only [includeRight_apply, Submodule.coe_set_mk, AddSubmonoid.coe_set_mk, AddSubsemigroup.coe_set_mk,
      SetLike.mem_coe, LinearMap.mem_range]
    suffices hb' : _
    use 1 ⊗ₜ[R] ⟨b, hb⟩
    rfl
  · rintro x ⟨y, rfl⟩
    induction y using TensorProduct.induction_on with
    | zero =>
        rw [map_zero]
        apply zero_mem
    | tmul a b =>
        simp only [LinearMap.lTensor_tmul, Submodule.coeSubtype]
        suffices : a ⊗ₜ[R] (b : B) = (a ⊗ₜ[R] (1 : B)) * ((1 : A) ⊗ₜ[R] (b : B))
        rw [this]
        apply Ideal.mul_mem_left
        apply Ideal.mem_map_of_mem
        exact Submodule.coe_mem b
        simp only [Submodule.coe_restrictScalars, tmul_mul_tmul, mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Ideal.add_mem _ hx hy

[Eric Wieser]

As a general rule, you can make things a lot shorter if you try really hard to avoid induction, and do things point-free instead

[Eric Wieser]

(also, were you looking for open scoped TensorProduct instead of that notation line?)

[Anatole Dedecker]

Do we know that (using Antoine's notations) if $M$ is an $A$-module and $N$ is a $B$-module, then $M \otimes_{R} N$ is an $A \otimes_{R} B$-module? I would guess not because that would lead to terrible diamonds, but do we even have it as a def?

[Eric Wieser]

I think we don't, precisely because of the terrible diamond it would lead to. I agree it's a natural way to try to form the above though

[Eric Wieser]

We have a def that says if $M$ is both an $A$-module and a $B$-module (in a compatible way, then $M$ is an $A \otimes_{R} B$-module

[Eric Wieser]

Which provides a conclusion with the same type as what you requested, but the wrong implementation!

[Eric Wieser]

But you can still use Algebra.TensorProduct.map (Algebra.lsmul _ _) (Algebra.lsmul _ _) or something to get a bundled version of the (action induced by the) module you want

[Anatole Dedecker]

Because then we could write the rhs as the range of the obvious $A \otimes_R B$-linear map $A \otimes_R I \to A \otimes_R B$. Then we can stay in $A \otimes_R B$-submodules-land, and using docs#eq_of_forall_ge_iff you can reduce the thing to some usual Galois connection facts

[Eric Wieser]

You can locally create the module with module.compHom and my morphism above, I believe

[Anatole Dedecker]

The thing is I not only the module, I also need the corresponding version of docs#LinearMap.lTensor...

[Eric Wieser]

Or rather, of docs#TensorProduct.map, since lTensor is just a special case?

[Anatole Dedecker]

Yes of course

[Notification Bot]

Naruyoko has marked this topic as resolved.

[Notification Bot]

Naruyoko has marked this topic as unresolved.

[Antoine Chambert-Loir]

I tried the other night to. play with Algebra.TensorProduct.map but creating the right-structure of module on the tensor product, and rapidly, Lean and I were in complete misunderstanding about which action is which…

[Antoine Chambert-Loir]

On the branch branch#biTensorProduct, I managed to construct the relevant module structure by first constructing the map from $A\otimes_R B$ to the $R$-algebra of linear endomorphisms of $M \otimes_R N$. I don't whether that will help.

[Eric Wieser]

Your moduleOfRingHom is docs#Module.compHom

[Eric Wieser]

And toFun_aux should follow directly from TensorProduct.map

[Antoine Chambert-Loir]

Thanks, that helped!
Maybe another approach to all of this is to make use of @Oliver Nash 's docs#Subbimodule.mk

[Eric Wieser]

TensorProduct.moduleMap' should follow from composing TensorProduct.map with docs#TensorProduct.homTensorHomMap

[Eric Wieser]

Or to get more directly to your final result as an AlgHom, docs#Module.endTensorEndAlgHom

[Eric Wieser]

def Algebra.TensorProduct.moduleMap : (A ⊗[R] B) →ₐ[R] (M ⊗[R] N) →ₗ[R] (M ⊗[R] N) :=
  Module.endTensorEndAlgHom.comp <|
    Algebra.TensorProduct.map (Algebra.lsmul _ _) (Algebra.lsmul _ _)

[Eric Wieser]

The last instance is then just

lemma Algebra.TensorProduct.isScalarTowerModule' : IsScalarTower R (A ⊗[R] B) (M ⊗[R] N) where
  smul_assoc a ab := FunLike.congr_fun (map_smul Algebra.TensorProduct.moduleMap a ab)

[Sophie Morel]

Eric Wieser said:

We have a def that says if $M$ is both an $A$-module and a $B$-module (in a compatible way, then $M$ is an $A \otimes_{R} B$-module

I was trying to use that construction to get the $A\otimes_R B$-module structure on $M\otimes_R N$, and I ran into trouble like Antoine with the action of $B$: I can define it, but I cannot prove that it is compatible with the action of $R$, and I am not sure what happened. Here is a MWE:

import Mathlib.Tactic
import Mathlib.LinearAlgebra.TensorProduct

open scoped TensorProduct

variable (R : Type _) [CommSemiring R]
  (B : Type _) [Semiring B] [Algebra R B]
variable (M N : Type _) [AddCommMonoid N] [AddCommMonoid M] [Module B N]
  [Module R N] [IsScalarTower R B N] [Module R M]

def module_right : Module B (M ⊗[R] N) := sorry

def scalar_tower_right : @IsScalarTower R B (M ⊗[R] N) _ (module_right R B M N).toSMul _ :=
{smul_assoc := sorry}  -- Error: failed to synthesize instance SMul B (M ⊗[R] N)

What I don't get is how to tell Lean what the action of $B$ on $M\otimes_R N$ is in the proof of scalar_tower_right, as it doesn't even give me a chance to start the proof... I don't want to make module_right R B M N an instance because it leads to horrible trouble too.

[Sophie Morel]

Ok, Antoine gave me a hint in a PM.

[Kevin Buzzard]

I think that these are issues which we will begin to understand better as we start doing harder commutative algebra. I remember when we hadn't discovered is_scalar_tower. Maybe there are other tricks to discover

[Anatole Dedecker]

I haven’t tried using Antoine’s non-instances yet, but I’m starting to think that a possible solution here is to just have type aliases for the tensor product depending on wether we want to enrich the scalars by acting from the left, right, or both (and the basic tensor product over R would only would only be a module over R). How stupid does that sound?

[Yaël Dillies]

That sounds very reasonable and in line with what other places in mathlib have done, see eg docs#ConjAct

[Anatole Dedecker]

I’m worried that it would juste bring too much code duplication, but each time I was worried about that in the past things actually worked fine

[Anatole Dedecker]

So maybe this is the right thing to do!

[Yaël Dillies]

Code duplication is a small pain once. The alternative is big pain forever.

[Antoine Chambert-Loir]

Note that Eric as golfed my stuff to a few lines…

[Anatole Dedecker]

Yes, but the point is being able to make instances so that everything gets convenient again

[Johan Commelin]

The downside of type aliases is not only code duplication. It also means divergence from what we write on paper. But I always find it hard to judge how much of a problem that is until we have actually written the API and used it in various places.

[Antoine Chambert-Loir]

What frightens me these days, is that while Sébastien managed to prove advancec things in descriptive set theory using infinitely many topologies on the same space, basic notions of algebra make Lean in total panic.

[Antoine Chambert-Loir]

(See the other thread on quotients, for an example)

[Oliver Nash]

I confess that I have not read this thread in detail but a quick scan suggests to me that we will indeed need some type aliases, to remove the pain here.

I furthermore claim that even informally there is a bit of a mess in situations like this, and some care can be needed to avoid confusion. For the simplest example, suppose we have a real vector space $V$ and a complex vector space $W$, then everyone agrees that $V \otimes_{\mathbb{R}} W$ is a complex vector space. Likewise if we reverse the roles and make $V$ a complex vector space and $W$ and real vector space. But what about if both $V$ and $W$ are complex vector spaces? Then there are two different actions of $\mathbb{C}$ on $V \otimes_{\mathbb{R}} W$.

Informally we would just say that what's really happening in this last case is that $V \otimes_{\mathbb{R}} W$ is a module over $\mathbb{C} \otimes_{\mathbb{R}} \mathbb{C}$ but this is a bit inconsistent with the first two cases where we pretended the actions are canonical. But they're only canonical if we implicitly say something crazy like "and there's no complex action on the other space".

I think if I were really pushed I'd probably say something like "well in the first case the scalars are $\mathbb{R} \otimes_{\mathbb{R}} \mathbb{C}$ and in the second case they're $\mathbb{C} \otimes_{\mathbb{R}} \mathbb{R}$". Of course both of these are canonically just $\mathbb{C}$ so we see that by silently invoking this isomorphism we lose some type information ("is it the left $\mathbb{C}$ or the right one?").

I proposed a solution to this in a very old thread here which I still think would work.

[Anatole Dedecker]

I agree with Oliver that this is already a problem in informal maths, although in my (very limited) experience people tend to either not care about it or just explicit the action all the time (and yes, I have totally been annoying my algebra teachers with it…). Indeed Oliver’s proposal is the kind of things I had in mind, although probably in greater detail. I used to think we could avoid it and just using the left action all the time would be fine, but this thread shows that it clearly isn’t, so I’m all in favor for this refactor.

[Anatole Dedecker]

One thing I would change to Oliver’s proposal is that I don’t think we have to specify which ring we want to "enrich" the tensor product with, just if it comes from the left, right, or both. That way if the left module is a module over a thousand rings (in an R-compatible way) then the tensor product "enriched from the left" would automatically be a module over all of these rings (like is the case currently). I can’t think of a case where that would cause any troubles, but maybe I’m wrong?

[Antoine Chambert-Loir]

Just a remark: these coincidences of the various module structures are explicitly addressed in math books, albeit at the very beginning of the elaboration of the theory and the stuff is completely hushed after that.
In complicated cases (though none comes to my mind right now), mathematicians use words to say, for this structure, the action of a on m is given by blahBlah, while for the natural structure it is given by bleep, and we have blahBlah = bleep because of…

[Antoine Chambert-Loir]

So I feel we ought to pull up our sleeves and try to find a solution that will be practical.
The standard approach is very good, because most of the time it suffices. Maybe there could be a way to decorate the bullets. In some sense, the case of tensor product is a nice one: for an A-module M and a B-modume N, it should be easy to say that M \otimes_R Nis anA-module on the left and a B-module on the right, hence a A \otimes_R B-module because the R-module structures agree.

[Antoine Chambert-Loir]

(You people have already thought a lot about it, I know…)

[Oliver Nash]

This can absolutely be solved, it just needs someone to put in the effort.

[Anatole Dedecker]

Antoine Chambert-Loir said:

So I feel we ought to pull up our sleeves and try to find a solution that will be practical.
The standard approach is very good, because most of the time it suffices. Maybe there could be a way to decorate the bullets. In some sense, the case of tensor product is a nice one: for an A-module M and a B-modume N, it should be easy to say that M \otimes_R Nis anA-module on the left and a B-module on the right, hence a A \otimes_R B-module because the R-module structures agree.

Just to make sure I understand right, you suggest having only one tensor product type, but having multiple smul notations indicating which module structure we want to use, right? I thought about this kind of solutions for totally unrelated things, and I don't see why it wouldn't work, however I'm a bit careful because we have never tried anything like that (I think). On the other hand the type-alias approach is quite common, as Yaël mentionned.

[Eric Wieser]

It's not clear to me whether the type alias belongs on the LHS or RHS of the smul (or both)

[Anatole Dedecker]

In that case I would definitely put it on the tensor product. For docs#ConjAct both would have been reasonable, but here in some sense we already have too much rings to deal with to put it on the ring :sweat_smile:

[Eric Wieser]

I think you run into trouble if you want $A \otimes_R B$ to simultaneously be an $R_A$ module (from $A$), an $R_B$ module (from $B$), and an $R$ module (from either, but which side gets the defeq?)

[Anatole Dedecker]

To be clear, the way I understand Antoine's suggestion is that a •ᵣ x would expand to the smul form the (non-instance) module structure coming from the right

[Anatole Dedecker]

Eric Wieser said:

I think you run into trouble if you want $A \otimes_R B$ to simultaneously be an $R_A$ module (from $A$), an $R_B$ module (from $B$), and an $R$ module (from either, but which side gets the defeq?)

I don't understand. What is $R_A$ here?

[Anatole Dedecker]

Oh you mean an $R$ module "trough" $A$ right?

[Eric Wieser]

No, I just mean two new rings $R_A, R_B$ such that $A$ is an $R_A$-module and $B$ is an $R_B$-module

[Anatole Dedecker]

Ah okay for the "type alias on the ring" approach

[Eric Wieser]

I'm not suggesting any approach or type aliases here; just "given three rings $R, R_A, R_B$ and two module $A, B$ how do we simultaneously make sense of these three actions?"

[Anatole Dedecker]

Oh okay sorry I completely misunderstood. It's clear that we can't have both left and right actions as instances since it already causes defeq-troubles when $R = R_A = R_B$ (note that right now the $R$-module structure already comes from the left. It doesn't matter propositionally, but it does definitionally)

[Antoine Chambert-Loir]

We must be ready to fill the module structures as @rguments, but one of the difficulty cones when the instances accumulate one over the other, like with ‘IsScalarTower‘. So maybe a structure that contains and which is easy to fill in might be useful.

[Eric Wieser]

Perhaps it's worth noting that with

def moduleMap : (A ⊗[R] B) →ₐ[R] (M ⊗[R] N) →ₗ[R] (M ⊗[R] N) :=
   sorry -- defined above

you automatically get the module structure Module moduleMap.range (M ⊗[R] N)

[Anatole Dedecker]

Antoine Chambert-Loir said:

We must be ready to fill the module structures as @rguments, but one of the difficulty cones when the instances accumulate one over the other, like with ‘IsScalarTower‘. So maybe a structure that contains and which is easy to fill in might be useful.

That’s what nice with the type aliases, you really can build your set of instances as you wish on the "new" types. However, note that the expanded type of docs#IsScalarTower does mention the module structure, so I think we could have the corresponding instances even if the modules are just definitions.