Right actions on tensor products (again)

Stream: mathlib4

[Kevin Buzzard]

RSMul R M with different notation and with r on the right. Because then I can have my right actions which my mathematics is demanding (I cannot get away from $A\otimes B$ being an $A$-module and a $B$-module)

[Eric Wieser]

In your hypothetical world, does Algebra R A imply RSMul R A?

[Eric Wieser]

And is $A \otimes_R B$ (with[Algebra R A] [Algebra R B]) an $A$-algebra? Because if the answer is yes to both, you're back in trouble all over again

[Kenny Lau]

I'll just remark that in the case where [CommRing R] [Ring A] [Ring B],
Algebra R A implies BiModule R R A (my notation),
and [Algebra R A] [Algebra R B] only implies BiModule R R (A ⊗[R] B) and Ring (A ⊗[R] B).

[Kenny Lau]

if A is also CommRing... then the situation would be more complicated

[Kenny Lau]

we would have [BiModule A A A] and [IsScalarTower₅ R R A A A] :upside_down:

[Kenny Lau]

I would dare to say that for the assumption [CommRing R] [CommRing A] [CommRing B], even A ⊗[R] B should only have the general instance [BiModule A B (A ⊗[R] B)], and the algebra instance is non-canonical and should be def not instance.

[Eric Wieser]

So how do we spell the tensor product of algebras or a base change?

[Kenny Lau]

They would have to be type synonyms

[Kenny Lau]

tensor product of algebra is fine, as long as your base is still R

[Kenny Lau]

we would have Left A B and Right A B be type synonyms of A ⊗[R] B, with instances:

• [Algebra A (Left A B)]
• [Algebra B (Right A B)]

[Eric Wieser]

This doesn't sound any better for Kevin, but that's not an argument against it either

[Kenny Lau]

The only canonical tensor product in mathematics is:

h1 : BiModule R₁ R₂ M
h2 : BiModule R₂ R₃ N
⊢ BiModule R₁ R₃ (M ⨂[R₂] N)

[Kenny Lau]

you could argue that having both left and right would be extra, since we could just have left as the default (and so without type synonym), and only do Right when necessary

[Kenny Lau]

which means:

• [Algebra A (A ⨂[R] B)]
• [Algebra B (Right A B)]

[Kenny Lau]

which I believe is close to how it's done currently?

[Matthew Jasper]

Currently there's a local instance and (almost) no API for Algebra B (A ⊗[R] B)

[Eric Wieser]

Either way it sounds like we could build Right today

[Eric Wieser]

(without doing anything with bimodules)

[Kenny Lau]

indeed

[Andrew Yang]

I thought the problem is that we sometimes want A ⨂[R] B as an algebra over both $A$ and $B$. If you add a new variant that only allows actions coming from the right, then how is that different from Right A B := B ⨂[R] A?

[Eric Wieser]

Indeed: is passing though canonical isomorphisms to and from Right any better than passing though comm?

[Kenny Lau]

@Andrew Yang when you say "sometimes", do you mean "for some specific values of A and B", or "for general A and B but only in specific contexts"?

Because if it's just some specific values, then type synonym would solve this issue.

But if it's some contexts... I think I would want to see an example

(and would we have [BiAlgebra A B S]?)

[Andrew Yang]

Some specific values. But are you suggesting we develop a theory of "right actions on tensor product" for every such "specific value" that we care about?

[Kenny Lau]

@Andrew Yang I'm not sure I understand, I'm proposing that we use a type synonym Right A B with an instance

[Kenny Lau]

type synonyms are good because the API should be (and are) different anyway

[Andrew Yang]

My question is, how is your suggestion different from Right A B := B ⨂[R] A and does it solve the problem of wanting A ⨂[R] B to be an algebra over both A and B?

[Kenny Lau]

it's different if we're dealing with bimodules; if you want both... is this mathematically sound? are you forming a category of (A,B)-bialgebra which would be the pushout category of A-algebra and B-algebra?

[Kenny Lau]

when you base change, you only base change to one new base right

[Andrew Yang]

This is just pushout in the category of rings.

I'm just trying to understand what is the problem that Right is intended to solve. If it is not intended to solve this problem (of wanting A ⨂[R] B to be an algebra over both A and B) then we should stop mentioning it in this context.

[Notification Bot]

30 messages were moved here from #mathlib4 > Generalizing Derivation module by Eric Wieser.

[Eric Wieser]

(We were quite a way from derivations)

[Kenny Lau]

@Andrew Yang I'm not sure we would want A ⨂[R] B to be an algebra over both A and B, because this would be problematic when A = B.

I know that in Kähler differential you want to be able to talk about the map ds := s ⊗ 1 - 1 ⊗ s where s : S and ds : S ⨂[R] S. In our combined proposal where Right B A is replaced with B ⨂[R] A, we could then define ds to be algebraMap S (S ⨂[R] S) s - TensorProduct.comm (algebraMap S (S ⨂[R] S) s). Is this what you mean?

[Andrew Yang]

One of the things I am trying to convey is that yes we currently cannot have that as an instance for the reasons you mentioned but there are cases where we do want such instances (such as we want $L \otimes_K \mathbb{A}_K$ to be both a $L$ and $\mathbb{A}_K$ algebra).

[Andrew Yang]

And I just want to know what problem Right is trying to solve. I am not insisting that it should solve this particular problem or anything. I just want to understand your proposal because I am currently very confused.

[Kenny Lau]

well, for one, it makes it so that you wouldn't have to use TensorProduct.comm everywhere

[Kenny Lau]

so the problem I was trying to solve is that sometimes we want A ⨂[R] B to be an A-module, and sometimes we want it to be a B-module

[Andrew Yang]

The point of type synonyms is to distinguish different between it and the orginal type. So type synonyms shouldn't be abbrevs and you shoudn't abuse the defeq of it between it and the original type (we are seeing lots of type synonyms getting turned to one field structures because of this). So you will still need to carry arround equivs like Left ≃ₗ[R] Right everywhere.

[Kenny Lau]

that is a good point; I guess TensorProduct.comm would act as this equivalence then

[Kenny Lau]

so is there any problem if we say that $L \otimes_K \mathbb{A}_K$ will be an $L$-algebra and $\mathbb{A}_K \otimes_K L$ will be an $\mathbb{A}_K$ algebra?

[Andrew Yang]

It is just very annoying and it being mathematically unnecessary makes it even more annoying. @Kevin Buzzard probably has a rant somewhere that he can just point you to it or copy paste it here.

[Kenny Lau]

OK, since this is now a specific instance (i.e. L ⨂[K] Adeles K), could we have an instance only for this specific pattern? This would avoid having a general instance for A ⨂[R] B which would cause problems when A = B. (Since I assume a number field cannot be equal to a ring of adèles)

[Kevin Buzzard]

I wrote a naive version of "X tensor adeles is an algebra over adeles if X is an algebra" and "X tensor adeles is a module over adeles if X is a module" and then I found out that I had a diamond :-/

[Andrew Yang]

We can develop material over docs#Algebra.TensorProduct.rightAlgebra (which should not be an instance) and do instance : Algebra (Adeles K) (L ⨂[K] Adeles K) := rightAlgebra (which could be an instance) if that is what you mean.

[Kevin Buzzard]

Currently I'm writing some API for "X tensor B is a B-algebra if X is an algebra" and I've just got to the point where I want X to be a module and now I'm a bit stuck

[Andrew Yang]

Kevin Buzzard said:

and then I found out that I had a diamond :-/

I guess this will go away if we make rightAlgebra also come from swap then smul.

[Kenny Lau]

@Andrew Yang yes, that is what I mean
@Kevin Buzzard the naive version won't work, that's why i'm saying that it's an instance only for this pattern

[Kenny Lau]

(and whatever you do, do not set X to be $\mathbb{A}_K$ :upside_down:

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/FLT/blob/1a5cc134559bae25b7e75d4113a492781cfd98f0/FLT/Hacks/RightAlgebraInstances.lean

[Kevin Buzzard]

X will never be A_K, A_K is always on the right

[Kenny Lau]

yeah then there shouldn't be a problem

[Kenny Lau]

i guess your "hacks" file is what Andrew is referring to by "develop material"

[Andrew Yang]

I guess this will go away if we make rightAlgebra also come from swap then smul.

By which I mean we should replace rightAlgebra to this: (not an instance ofc)

import Mathlib

variable {R S M A : Type*} [CommRing R] [CommRing S] [AddCommGroup M] [Algebra R S] [Module R M]
  [CommRing A] [Algebra R A]

open TensorProduct

noncomputable section

instance foo : SMul S (M ⊗[R] S) where
  smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e))

@[simp]
lemma smul_def (r : S) (m : M ⊗[R] S) :
    r • m = (TensorProduct.comm _ _ _).symm (r • (TensorProduct.comm _ _ _ m)) := rfl

instance : Module S (M ⊗[R] S) where
  smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e))
  one_smul _ := by simp
  mul_smul := by simp [mul_smul]
  smul_zero := by simp
  smul_add := by simp
  add_smul := by simp [add_smul]
  zero_smul := by simp

instance : Algebra S (A ⊗[R] S) where
  algebraMap := Algebra.TensorProduct.includeRight.toRingHom
  commutes' _ _ := Commute.all _ _
  smul_def' r x := by induction x <;> simp_all [smul_tmul', mul_add]

[Edison Xie]

Andrew Yang said:

instance : Module S (M ⊗[R] S) where
  smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e))
  one_smul _ := by simp
  mul_smul := by simp [mul_smul]
  smul_zero := by simp
  smul_add := by simp
  add_smul := by simp [add_smul]
  zero_smul := by simp

instance : Module S (M ⊗[R] S) where
  smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e))
  one_smul _ := by simp
  mul_smul := by simp [mul_smul]
  smul_zero := by simp
  smul_add := by simp
  add_smul := by simp [add_smul]
  zero_smul := by simp

Are these two instances the same?

[Andrew Yang]

I was wondering why my code was unnecessarily long... (edited now)

[Kevin Buzzard]

So my philosophy with "not an instance" is that it's only not an instance because of the A=B issue, meaning that it's fine to make it locally an instance (eg via open scoped RightAction in a file full of $V\otimes\mathbb{A}_K$ when V is countable and $\mathbb{A}_K$ is uncountable.

[Kenny Lau]

Kevin Buzzard said:

So my philosophy with "not an instance" is that it's only not an instance because of the A=B issue, meaning that it's fine to make it locally an instance (eg via open scoped RightAction in a file full of $V\otimes\mathbb{A}_K$ when V is countable and $\mathbb{A}_K$ is uncountable.

yes, it is fine to make it an instance here; it just wouldn't work if you use the "naive approach"

[Anatole Dedecker]

I still think the only future-proof way to work around this kind of things is named actions, but that’s a long term discussion

[Kevin Buzzard]

Andrew Yang said:

I guess this will go away if we make rightAlgebra also come from swap then smul.

By which I mean we should replace rightAlgebra to this: (not an instance ofc)

...

Sorry to take so long getting back to this. In my application A is not commutative (but it's still an algebra); is this a problem?

--import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
import Mathlib


/-

# Right module and algebra instances

TODO

This file enables you to write `open scoped Rightactions` and magically `A ⊗[R] B`
becomes a `B`-algebra as well as an `A`-algebra, and you get instances like
`[Module.Finite R A] → [Module.Finite B (A ⊗[R] B)]`.

Mathlib would not have this hack because `A ⊗[R] A` is now an `A`-algebra in two
different ways. But this situation will not arise in the cases where we use this,
and it's very convenient to open the scope temporarily in order to prove theorems
which can be used without the scope open.
-/

open scoped TensorProduct

namespace RightActions

noncomputable section

variable (R S M A B : Type*) [CommRing R] [CommRing S] [AddCommGroup M] [Algebra R S] [Module R M]
  [CommRing A] [Algebra R A]
  [Ring B] [Algebra R B] -- new

scoped instance : SMul S (M ⊗[R] S) where
  smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e))

@[simp]
lemma smul_def (r : S) (m : M ⊗[R] S) :
    r • m = (TensorProduct.comm _ _ _).symm (r • (TensorProduct.comm _ _ _ m)) := rfl

scoped instance : Module S (M ⊗[R] S) where
  smul s e := TensorProduct.comm _ _ _ (s • (TensorProduct.comm _ _ _ e))
  one_smul _ := by simp
  mul_smul := by simp [mul_smul]
  smul_zero := by simp
  smul_add := by simp
  add_smul := by simp [add_smul]
  zero_smul := by simp

scoped instance : Algebra S (B ⊗[R] S) where
  algebraMap := Algebra.TensorProduct.includeRight.toRingHom
  commutes' s bs := sorry
  smul_def' r x := sorry

/-- The A-algebra isomorphism A ⊗ B = B ⊗ A, available in the `RightAlgebra` scope. -/
def TensorProduct.comm : A ⊗[R] B ≃ₐ[A] B ⊗[R] A where
  __ := Algebra.TensorProduct.comm R A B
  commutes' _ := rfl

scoped instance [Module.Finite R B] : Module.Finite A (B ⊗[R] A) :=
  Module.Finite.equiv (TensorProduct.comm R A B).toLinearEquiv

scoped instance [Module.Free R B] : Module.Free A (B ⊗[R] A) :=
  Module.Free.of_equiv (TensorProduct.comm R A B).toLinearEquiv

/-- The module topology on a right algebra. -/
scoped instance [TopologicalSpace A] : TopologicalSpace (B ⊗[R] A) :=
  moduleTopology A (B ⊗[R] A)

scoped instance [TopologicalSpace A] : IsModuleTopology A (B ⊗[R] A) := ⟨rfl⟩

-- works with the FLT import

-- scoped instance [TopologicalSpace A] [IsTopologicalRing A] [Module.Finite R B] :
--     IsTopologicalRing (B ⊗[R] A) :=
--   IsModuleTopology.Module.topologicalRing A _

-- scoped instance [TopologicalSpace A] [IsTopologicalRing A]
--     [LocallyCompactSpace A] [Module.Finite R B] :
--     LocallyCompactSpace (B ⊗[R] A) := IsModuleTopology.locallyCompactSpaceOfFinite A

end -- section

end RightActions

[Andrew Yang]

It should be fine. Did the diamond you mentioned before go away?

[Kevin Buzzard]

yeah I'm making good progress. I'll check the diamond after!

[Kevin Buzzard]

Oh what the heck, there's already a scope called RightActions?? I just noticed because suddenly there was wacky notation.

[Kevin Buzzard]

scoped instance : Algebra S (B ⊗[R] S) where
  algebraMap := Algebra.TensorProduct.includeRight.toRingHom
  commutes' s bs := by
    induction bs with
    | zero => simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
      Algebra.TensorProduct.includeRight_apply, mul_zero, zero_mul]
    | tmul x y =>
        simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul,
          mul_one, mul_comm]
    | add x y _ _ =>
        simp_all only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          Algebra.TensorProduct.includeRight_apply, mul_add, add_mul]
  smul_def' s bs := by
    induction bs with
    | zero => simp
    | tmul x y =>
        simp only [smul_def, TensorProduct.comm_tmul, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul]
        rw [TensorProduct.smul_tmul']
        simp only [smul_eq_mul, TensorProduct.comm_symm_tmul]
    | add x y hx hy =>
        simp_all only [smul_def, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          Algebra.TensorProduct.includeRight_apply, smul_add, ← hx, ← hy, mul_add]

(simp is quite slow so I squoze them)

[Eric Wieser]

Yes, it contains the notation for right actions!

[Kevin Buzzard]

Should this stuff above be in the same scope or am I doing something else? I feel like it's a bit different so I called it RightModuleActions for the moment.

[Eric Wieser]

TensorProduct.RightActions would be another option

[Kevin Buzzard]

yeah it looks like the diamond has gone away. For example

import FLT.Hacks.RightAlgebraInstances

namespace TensorProduct.RightActions

noncomputable def LinearMap.baseChange (R : Type*) [CommRing R] (V W : Type*) [AddCommGroup V] [Module R V]
    [AddCommGroup W] [Module R W] (A : Type*) [CommRing A] [Algebra R A]
    (φ : V →ₗ[R] W) : V ⊗[R] A →ₗ[A] W ⊗[R] A :=
  (Module.TensorProduct.comm R A W).toLinearMap ∘ₗ
    (_root_.LinearMap.baseChange A φ) ∘ₗ
    (Module.TensorProduct.comm R A V).symm.toLinearMap

noncomputable def AlgebraMap.baseChange (R : Type*) [CommRing R] (V W : Type*) [Ring V] [Algebra R V]
    [Ring W] [Algebra R W] (A : Type*) [CommRing A] [Algebra R A]
    (φ : V →ₐ[R] W) : V ⊗[R] A →ₐ[A] W ⊗[R] A where
  __ := LinearMap.baseChange R V W A φ
  map_one' := sorry
  map_mul' := sorry
  map_zero' := sorry
  commutes' := sorry

works fine. Thanks! I'll stick with this for now.

[Kevin Buzzard]

Andrew Yang said:

I guess this will go away if we make rightAlgebra also come from swap then smul.

By which I mean we should replace rightAlgebra to this: (not an instance ofc)

...

#25481 (WIP because I didn't fill in the proofs, I just wanted to assess mathlib breakage first; I have proofs in FLT but they don't compile in mathlib, presumably because I have more imports (indeed right now I have import Mathlib)

[Kevin Buzzard]

PS is my description of the PR accurate? It seemed to me that if we stuck with the current mathlib definition of rightAlgebra and then attempted to define rightModule then I would have to start by writing the "opposite" of this mathlib code

instance leftHasSMul : SMul R' (M ⊗[R] N) :=
  ⟨fun r =>
    (addConGen (TensorProduct.Eqv R M N)).lift (SMul.aux r : _ →+ M ⊗[R] N) <|
      AddCon.addConGen_le fun x y hxy =>
        match x, y, hxy with
        | _, _, .of_zero_left n =>
          (AddCon.ker_rel _).2 <| by simp_rw [map_zero, SMul.aux_of, smul_zero, zero_tmul]
        | _, _, .of_zero_right m =>
          (AddCon.ker_rel _).2 <| by simp_rw [map_zero, SMul.aux_of, tmul_zero]
        | _, _, .of_add_left m₁ m₂ n =>
          (AddCon.ker_rel _).2 <| by simp_rw [map_add, SMul.aux_of, smul_add, add_tmul]
        | _, _, .of_add_right m n₁ n₂ =>
          (AddCon.ker_rel _).2 <| by simp_rw [map_add, SMul.aux_of, tmul_add]
        | _, _, .of_smul s m n =>
          (AddCon.ker_rel _).2 <| by rw [SMul.aux_of, SMul.aux_of, ← smul_comm, smul_tmul]
        | _, _, .add_comm x y =>
          (AddCon.ker_rel _).2 <| by simp_rw [map_add, add_comm]⟩

I think Andrew's approach (change the definition of rightAlgebra) is much better.

[Eric Wieser]

I think pulling through comm is going to cause trouble in an eventual bimodule world, where you can't commute without also moving to MulOpposite

[Kevin Buzzard]

Will it cause more or less trouble than the current definition of rightAlgebra?

[Calle Sönne]

I'm joining this discussion a bit late, but have people already considered making a type synonym for the right factor? So whenever you expect problems you can instead write M ⊗[R] (right S). And when there are no issues with ambiguity you can just write M ⊗[R] Sas normal? (and then for symmetry you can define the type synonym left also)

[Oliver Nash]

I’m travelling at the moment (trying to catch up on threads at the airport) so I’m also late here but I might highlight this old discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change