tensorproduct with endomorphisms

Stream: Is there code for X?

[Johan Commelin]

I would be interested in knowing if we have constructions that allow to golf this.
Certainly, the first two decls should be generalized to the case of linear maps between two modules, instead of just endomorphisms. But that's orthogonal to my question.

import Mathlib

namespace LinearMap

variable (R A M : Type*) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M]

open Module
open scoped TensorProduct

noncomputable
def TensorProductEndₗ' : A ⊗[R] (End R M) →ₗ[R] End A (A ⊗[R] M) :=
  TensorProduct.lift <|
  { toFun := fun a ↦ a • baseChangeHom R A M M
    map_add' := by simp only [add_smul, forall_true_iff]
    map_smul' := by simp only [smul_assoc, RingHom.id_apply, forall_true_iff] }

noncomputable
def TensorProductEndₗ : A ⊗[R] (End R M) →ₗ[A] End A (A ⊗[R] M) :=
  { TensorProductEndₗ' R A M with
    map_smul' := by
      intros a f
      show TensorProductEndₗ' R A M (a • f) = a • TensorProductEndₗ' R A M f
      unfold TensorProductEndₗ'
      induction f using TensorProduct.induction_on with
      | zero => simp only [smul_zero, LinearMap.map_zero]
      | tmul b f =>
          simp only [TensorProduct.smul_tmul', TensorProduct.lift.tmul]
          dsimp only [coe_mk, AddHom.coe_mk, smul_apply, baseChangeHom_apply]
          rw [smul_assoc]
      | add f g hf hg => simp only [smul_add, LinearMap.map_add, hf, hg] }

noncomputable
def TensorProductEnd : A ⊗[R] (End R M) →ₐ[A] End A (A ⊗[R] M) :=
  Algebra.TensorProduct.algHomOfLinearMapTensorProduct
    (TensorProductEndₗ R A M)
    (fun a b f g ↦ by
      simp only [TensorProductEndₗ, TensorProductEndₗ', coe_mk, TensorProduct.lift.tmul',
        AddHom.coe_mk, mul_eq_comp, baseChangeHom_apply, smul_apply, baseChange_comp]
      apply LinearMap.ext
      intro x
      simp only [LinearMap.comp_apply, smul_apply, map_smul, mul_comm a b, mul_smul])
    (by
      simp only [TensorProductEndₗ, TensorProductEndₗ', coe_mk, TensorProduct.lift.tmul',
        AddHom.coe_mk, one_smul, baseChangeHom_apply]
      apply LinearMap.ext
      intro x
      erw [baseChange_eq_ltensor, lTensor_id, LinearMap.id_apply])

end LinearMap

[Eric Wieser]

I think you can merge the first two by using TensorProduct.AlgebraTensorModule.lift

[Antoine Chambert-Loir]

I don't think you can go much shorter, because it is really about the definition of a base change functor in various categories. Basically , one applies the universal property of the tensor product, and sone hypotheses have to be checked — they could have been checked elsewhere.

[Oliver Nash]

The key here is indeed docs#TensorProduct.AlgebraTensorModule.lift as @Eric Wieser suggests:

import Mathlib

namespace LinearMap

variable (R A M : Type*) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M]

open Module
open scoped TensorProduct

noncomputable
def TensorProductEndₗ : A ⊗[R] (End R M) →ₗ[A] End A (A ⊗[R] M) :=
  TensorProduct.AlgebraTensorModule.lift <|
  { toFun := fun a ↦ a • baseChangeHom R A M M
    map_add' := by simp only [add_smul, forall_true_iff]
    map_smul' := by simp only [smul_assoc, RingHom.id_apply, forall_true_iff] }

[Eric Wieser]

I would guess that linear map already exists too

[Eric Wieser]

(as the general form that SMul is a linear map)

[Johan Commelin]

I searched for it, but didn't find it. SMulOneHom isn't the right thing...

[Oliver Nash]

(Likewise I couldn't find it.)

[Johan Commelin]

But thanks for the pointer to TensorProduct.AlgebraTensorModule.lift!

[Eric Wieser]

It will be something like Module.toLinearMap

[Junyan Xu]

docs#LinearMap.toSpanSingleton (see also docs#LinearMap.ringLmapEquivSelf)

[Eric Wieser]

docs#Algebra.lsmul should give the last result, along with docs#Algebra.TensorProduct.lift

[Johan Commelin]

Which result?

[Eric Wieser]

Now that I'm at a computer, here's my spelling of all of them:

import Mathlib

namespace LinearMap

variable (R A M N : Type*) [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]

open Module
open scoped TensorProduct

-- these should be in mathlib
@[simp]
theorem baseChange_id : LinearMap.baseChange A (.id : M →ₗ[R] M) = .id := by simp [baseChange]

/-- On endomorphisms, `LinearMap.baseChangeHom` is an `AlgHom`. -/
@[simps!]
noncomputable
def _root_.Module.End.baseChangeHom : End R M →ₐ[R] End A (A ⊗[R] M) :=
  .ofLinearMap (LinearMap.baseChangeHom _ _ _ _) (baseChange_id _ _ _) (fun f g => baseChange_comp g f)


-- These are maybe more contrived
noncomputable
def TensorProductEndₗ : A ⊗[R] (M →ₗ[R] N) →ₗ[A] (A ⊗[R] M) →ₗ[A] (A ⊗[R] N):=
  TensorProduct.AlgebraTensorModule.lift <|
    (Algebra.lsmul A A _).toLinearMap.flip (baseChangeHom R A M N)

noncomputable
def TensorProductEnd : A ⊗[R] (End R M) →ₐ[A] End A (A ⊗[R] M) :=
  Algebra.TensorProduct.lift (Algebra.ofId _ _) (Module.End.baseChangeHom _ _ _) (fun _ _=> Algebra.commute_algebraMap_left _ _)

end LinearMap

[Eric Wieser]

Probably we should have AlgHom.baseChange that handles the lift (.ofId _ _) ?_ sorry pattern

[Eric Wieser]

#10928 adds the first two results

[Johan Commelin]

Thanks!