Skip to content

chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor #41550

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ScottCarnahan wants to merge 1 commit into
base: master
Choose a base branch
from
+14 −6
Open

chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor #41550

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions Mathlib/LinearAlgebra/TensorProduct/Map.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -595,21 +595,29 @@ def rTensor (f : N ≃ₗ[R] P) : N ⊗[R] M ≃ₗ[R] P ⊗[R] M := TensorProdu

variable (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (m : M) (n : N) (p : P) (x : M ⊗[R] N) (y : N ⊗[R] M)

@[simp] theorem symm_lTensor : (f.lTensor M).symm = f.symm.lTensor M := rfl

@[simp] theorem symm_rTensor : (f.rTensor M).symm = f.symm.rTensor M := rfl

@[simp] theorem coe_lTensor : lTensor M f = (f : N →ₗ[R] P).lTensor M := rfl
Comment thread
themathqueen marked this conversation as resolved.

@[simp] theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl
@[deprecated "use symm_lTensor and coe_lTensor" (since := "2026-07-04")]
theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl

@[simp] theorem coe_rTensor : rTensor M f = (f : N →ₗ[R] P).rTensor M := rfl

@[simp] theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl
@[deprecated "use symm_rTensor and coe_rTensor" (since := "2026-07-04")]
theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl

@[simp] theorem lTensor_tmul : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n := rfl

@[simp] theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl
@[deprecated "use symm_lTensor and lTensor_tmul" (since := "2026-07-04")]
theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl

@[simp] theorem rTensor_tmul : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m := rfl

@[simp] theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl
@[deprecated "use symm_rTensor and rTensor_tmul" (since := "2026-07-04")]
theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl

lemma comm_trans_rTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g :=
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,8 +73,8 @@ attribute [coassoc_simps] LinearMap.comp_id LinearMap.id_comp TensorProduct.map_
LinearEquiv.coe_trans LinearEquiv.trans_symm
LinearEquiv.refl_toLinearMap TensorProduct.toLinearMap_congr
LinearEquiv.comp_symm LinearEquiv.symm_comp LinearEquiv.symm_symm
LinearEquiv.coe_lTensor LinearEquiv.coe_lTensor_symm
LinearEquiv.coe_rTensor LinearEquiv.coe_rTensor_symm
LinearEquiv.coe_lTensor LinearEquiv.symm_lTensor
LinearEquiv.coe_rTensor LinearEquiv.symm_rTensor
IsCocomm.comm_comp_comul TensorProduct.AlgebraTensorModule.map_eq
TensorProduct.AlgebraTensorModule.assoc_eq TensorProduct.AlgebraTensorModule.rightComm_eq
TensorProduct.tensorTensorTensorComm TensorProduct.AlgebraTensorModule.tensorTensorTensorComm
Expand Down
Loading