Documentation

Mathlib.LinearAlgebra.TensorProduct.Lift

Lifting linear maps from base-changed modules #

This file defines the lift of an R-linear map from M to an A-module N to an A-linear map from A ⊗[R] M to N.

source
def LinearMap.liftBaseChangeEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] :
(M →ₗ[R] N) ≃ₗ[A] TensorProduct R A M →ₗ[A] N

If M is an R-module and N is an A-module, then A-linear maps A ⊗[R] M →ₗ[A] N correspond to R-linear maps M →ₗ[R] N by composing with M → A ⊗[R] M, x ↦ 1 ⊗ₜ x.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LinearMap.liftBaseChange {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) :
    TensorProduct R A M →ₗ[A] N

    If N is an A-module, lift a linear map M →ₗ[R] N to A ⊗[R] M →ₗ[A] N.

    Equations
    Instances For
      source
      @[simp]
      theorem LinearMap.liftBaseChange_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) (x : A) (y : M) :
      (liftBaseChange A l) (x ⊗ₜ[R] y) = x • l y
      source
      theorem LinearMap.liftBaseChange_one_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) (y : M) :
      (liftBaseChange A l) (1 ⊗ₜ[R] y) = l y
      source
      @[simp]
      theorem LinearMap.liftBaseChangeEquiv_symm_apply {R : Type u_4} {M : Type u_2} {N : Type u_3} (A : Type u_1) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : TensorProduct R A M →ₗ[A] N) (x : M) :
      ((liftBaseChangeEquiv A).symm l) x = l (1 ⊗ₜ[R] x)
      source
      theorem LinearMap.liftBaseChange_comp {R : Type u_3} {M : Type u_4} {N : Type u_5} (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] {P : Type u_1} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P] (l : M →ₗ[R] N) (l' : N →ₗ[A] P) :
      l' ∘ₗ liftBaseChange A l = liftBaseChange A (↑R l' ∘ₗ l)
      source
      @[simp]
      theorem LinearMap.range_liftBaseChange {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) :
      (liftBaseChange A l).range = Submodule.span A ↑l.range