base change adjunction for linear maps

Stream: Is there code for X?

[Antoine Chambert-Loir]

Does this code already exist in mathlib? Or can it be golfed significantly?
Ideally, I would like to have this equiv as a linear equiv, (S ⊗[R] M →ₗ[S] N) ≃ₗ[S] (M →ₗ[R] N).

import Mathlib.RingTheory.TensorProduct.Basic

open scoped TensorProduct

variable (R : Type*) [CommRing R]
  (S : Type*) [CommRing S] [Algebra R S]
  (M : Type*) [AddCommMonoid M] [Module R M]
  (N : Type*) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]

noncomputable def LinearMap.baseChangeEquiv : (S ⊗[R] M →ₗ[S] N) ≃ (M →ₗ[R] N) where
  toFun g := LinearMap.comp (g.restrictScalars R) ({
    toFun := fun m ↦ 1 ⊗ₜ[R] m
    map_add' := fun x y ↦ by simp only [TensorProduct.tmul_add]
    map_smul' := fun r x ↦ by
      simp only [TensorProduct.tmul_smul, RingHom.id_apply] } : M →ₗ[R] S ⊗[R] M)
  invFun f := by
    apply TensorProduct.AlgebraTensorModule.lift
    exact {
      toFun := fun s ↦ s • f
      map_add' := fun x y ↦ by ext m; simp only [smul_apply, add_apply, add_smul]
      map_smul' := fun s s' ↦ by
        ext m; simp only [smul_eq_mul, smul_apply, RingHom.id_apply, mul_smul] }
  left_inv g := by ext m; simp
  right_inv f := by ext m; simp

[Adam Topaz]

It seems that the classes involved in docs#Algebra.TensorProduct.includeRight should be relaxed a bit.

[Kevin Buzzard]

How can they be relaxed if you want an algebra morphism?

[Matthew Ballard]

Do we need the by apply ... exact here?

[Adam Topaz]

you can get a linear map with only one side of the tensor product being a (commutative) algebra.

[Adam Topaz]

Sorry, "relaxed" isn't exactly right, it's more that I'm surprised that we don't have the linear version of this.

[Antoine Chambert-Loir]

So am I…

[Richard Copley]

The invfun is

invFun f := TensorProduct.AlgebraTensorModule.lift ((LinearMap.lsmul S (M →ₗ[R] N)).flip f)

[Adam Topaz]

right now docs#Algebra.TensorProduct.includeRight is just defined directly (and includeLeft is defined in terms of docs#Algebra.TensorProduct.includeLeftRingHom ). I think it would be more useful to introduce linear versions of both of these (with the appropriate "relaxed" typeclasses) and build these algebra homs on top of those.

[Adam Topaz]

Do we not have the adjunction formulated in categorical terms?

[Adam Topaz]

We do: ModuleCat.extendRestrictScalarsAdj

[Antoine Chambert-Loir]

How is the category part of mathlib supposed to interact with the rest? There's a risk of fragmentation and/or duplication if things can be/have to be done twice in an unspecified way.

[Joël Riou]

Antoine Chambert-Loir said:

How is the category part of mathlib supposed to interact with the rest? There's a risk of fragmentation and/or duplication if things can be/have to be done twice in an unspecified way.

I think that the definitions should be done first (1) for types equipped with [Module...] instances and secondly (2) in the language of categories ModuleCat by using the API (1). Mostly, it should not be in the other direction.

If, for some reason, the categorical version of something entered mathlib first, the unbundled version should be added and the category theory definition changed in order to use the unbundled version.

[Richard Copley]

I'm not sure how much of an improvement this is :)

noncomputable def LinearMap.baseChangeEquiv': (S ⊗[R] M →ₗ[S] N) ≃ (M →ₗ[R] N) where
  toFun g :=
    g.restrictScalars R ∘ₗ
      ((LinearMap.lsmul R S).flip 1).rTensor M ∘ₗ
        (TensorProduct.lid R M).symm.toLinearMap
  invFun f := TensorProduct.AlgebraTensorModule.lift <| (LinearMap.lsmul S (M →ₗ[R] N)).flip f
  left_inv g := by ext m; simp
  right_inv f := by ext m; simp

[Amelia Livingston]

Joël Riou said:

Antoine Chambert-Loir said:

How is the category part of mathlib supposed to interact with the rest? There's a risk of fragmentation and/or duplication if things can be/have to be done twice in an unspecified way.

I think that the definitions should be done first (1) for types equipped with [Module...] instances and secondly (2) in the language of categories ModuleCat by using the API (1). Mostly, it should not be in the other direction.

If, for some reason, the categorical version of something entered mathlib first, the unbundled version should be added and the category theory definition changed in order to use the unbundled version.

Interesting - could you expand on why this is the best approach? I've wanted e.g. non-categorical representation morphisms myself but I'd hoped that someday this wouldn't be the case. And I'd assumed it'd be nice to be able to use the category theory library to get non-category theory API when possible.

[Joël Riou]

One of the reasons is that in the category theory context, there are more restrictions on universes, for example, the unbundled notion of linear map is more general than the notion of morphisms in the category ModuleCat. Otherwise, I would obviously promote category theory more!

(Then, of course, if unbundled/bundled versions of new definitions are equally general, and if it is much easier to use category theory, there is no reason not to use it.)

[Amelia Livingston]

Fair enough. I guess the category theory typeclass assumptions are also less general sometimes too, like ModuleCat requiring an AddCommGroup and a ring rather than AddCommMonoid and semiring