Tensor product with free modules.

This file contains lemmas about tensoring with free modules.

noncomputable def Algebra.TensorProduct.equivPiOfFiniteBasis {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommSemiring A] [CommSemiring R] [Algebra R A] [AddCommGroup V] [Module R V] {ι : Type u_4} (b : Module.Basis ι R V) [Finite ι] : TensorProduct R A V ≃ₗ[A] ι → A

The A-algebra isomorphism A ⊗[R] V ≃ₗ[A] (ι → A) coming from an ι-indexed basis of a finite free R-module V.

Equations

• Algebra.TensorProduct.equivPiOfFiniteBasis A b = (LinearEquiv.baseChange R A V (ι → R) b.equivFun).trans (TensorProduct.piScalarRight R A A ι)

@[simp]

theorem Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommSemiring A] [CommSemiring R] [Algebra R A] [AddCommGroup V] [Module R V] {ι : Type u_4} (b : Module.Basis ι R V) [Finite ι] (a✝ : ι → A) : (equivPiOfFiniteBasis A b).symm a✝ = (LinearEquiv.baseChange R A V (ι → R) b.equivFun).symm ((TensorProduct.piScalarRight R A A ι).symm a✝)

@[simp]

theorem Algebra.TensorProduct.equivPiOfFiniteBasis_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommSemiring A] [CommSemiring R] [Algebra R A] [AddCommGroup V] [Module R V] {ι : Type u_4} (b : Module.Basis ι R V) [Finite ι] (a✝ : TensorProduct R A V) (a✝¹ : ι) : (equivPiOfFiniteBasis A b) a✝ a✝¹ = (TensorProduct.piScalarRightHom R A A ι) ((LinearMap.baseChange A ↑b.equivFun) a✝) a✝¹

noncomputable def Algebra.TensorProduct.equivFinsuppOfBasis {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommSemiring A] [CommSemiring R] [Algebra R A] [AddCommGroup V] [Module R V] {ι : Type u_4} (b : Module.Basis ι R V) : TensorProduct R A V ≃ₗ[A] ι →₀ A

The A-algebra isomorphism A ⊗[R] V ≃ₗ[A] (ι →₀ A) coming from an ι-indexed basis of a free R-module V.

Equations

• Algebra.TensorProduct.equivFinsuppOfBasis A b = (LinearEquiv.baseChange R A V (ι →₀ R) b.repr).trans (TensorProduct.finsuppScalarRight R A A ι)

@[simp]

theorem Algebra.TensorProduct.equivFinsuppOfBasis_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommSemiring A] [CommSemiring R] [Algebra R A] [AddCommGroup V] [Module R V] {ι : Type u_4} (b : Module.Basis ι R V) (a✝ : TensorProduct R A V) : (equivFinsuppOfBasis A b) a✝ = (TensorProduct.finsuppScalarRight R A A ι) ((LinearMap.baseChange A ↑b.repr) a✝)

@[simp]

theorem Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommSemiring A] [CommSemiring R] [Algebra R A] [AddCommGroup V] [Module R V] {ι : Type u_4} (b : Module.Basis ι R V) (a✝ : ι →₀ A) : (equivFinsuppOfBasis A b).symm a✝ = (LinearEquiv.baseChange R A V (ι →₀ R) b.repr).symm ((TensorProduct.finsuppScalarRight R A A ι).symm a✝)