Contractions #

Given modules $M, N$ over a commutative ring $R$, this file defines the natural linear maps: $M^* \otimes M \to R$, $M \otimes M^* \to R$, and $M^* \otimes N → Hom(M, N)$, as well as proving some basic properties of these maps.

It also constructs linear equivalences between tensor products of hom modules and hom modules of tensor products:

lTensorHomEquivHomLTensor: P ⊗ Hom(M, Q) ≃ₗ Hom(M, P ⊗ Q) for M finite projective
rTensorHomEquivHomRTensor: Hom(M, P) ⊗ Q ≃ₗ Hom(M, P ⊗ Q) for M finite projective
TensorProduct.homTensorHomEquiv: Hom(M, P) ⊗ Hom(N, Q) ≃ₗ Hom(M ⊗ N, P ⊗ Q) for M, N finite projective
TensorProduct.dualDistribEquiv: Dual M ⊗ Dual N ≃ₗ Dual (M ⊗ N) for M, N finite projective

Tags #

contraction, dual module, tensor product

source

def contractLeft (R : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] :

TensorProduct R (Module.Dual R M) M →ₗ[R] R

The natural left-handed pairing between a module and its dual.

Equations

contractLeft R M = (TensorProduct.uncurry (RingHom.id R) (Module.Dual R M) M R).toFun LinearMap.id

Instances For

source

def contractRight (R : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] :

TensorProduct R M (Module.Dual R M) →ₗ[R] R

The natural right-handed pairing between a module and its dual.

Equations

contractRight R M = (TensorProduct.uncurry (RingHom.id R) M (Module.Dual R M) R).toFun LinearMap.id.flip

Instances For

source

def dualTensorHom (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct R (Module.Dual R M) N →ₗ[R] M →ₗ[R] N

The natural map associating a linear map to the tensor product of two modules.

Equations

dualTensorHom R M N = (TensorProduct.uncurry (RingHom.id R) (Module.Dual R M) N (M →ₗ[R] N)) LinearMap.smulRightₗ

Instances For

source

@[simp]

theorem contractLeft_apply {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :

(contractLeft R M) (f ⊗ₜ[R] m) = f m

source

@[simp]

theorem contractRight_apply {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :

(contractRight R M) (m ⊗ₜ[R] f) = f m

source

@[simp]

theorem dualTensorHom_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (m : M) (n : N) :

((dualTensorHom R M N) (f ⊗ₜ[R] n)) m = f m • n

source

theorem dualTensorHom_comp_lTensor {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) :

dualTensorHom R M P ∘ₗ LinearMap.lTensor (Module.Dual R M) f = LinearMap.compRight R f ∘ₗ dualTensorHom R M N

source

theorem dualTensorHom_comp_rTensor_dualMap {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N) :

dualTensorHom R M P ∘ₗ LinearMap.rTensor P f.dualMap = LinearMap.lcomp R P f ∘ₗ dualTensorHom R N P

source

@[simp]

theorem transpose_dualTensorHom {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :

Module.Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) = (dualTensorHom R (Module.Dual R M) (Module.Dual R M)) ((Module.Dual.eval R M) m ⊗ₜ[R] f)

source

@[simp]

theorem dualTensorHom_prodMap_zero {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) :

((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)

source

@[simp]

theorem zero_prodMap_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : Module.Dual R N) (q : Q) :

LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)

source

theorem map_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) :

TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (TensorProduct R M N) (TensorProduct R P Q)) ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))

source

@[simp]

theorem comp_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) :

(dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)

source

theorem toMatrix_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {m : Type u_7} {n : Type u_8} [Fintype m] [Finite n] [DecidableEq m] [DecidableEq n] (bM : Module.Basis m R M) (bN : Module.Basis n R N) (j : m) (i : n) :

(LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1

As a matrix, dualTensorHom evaluated on a basis element of M* ⊗ N is a matrix with a single one and zeros elsewhere

source

theorem Module.Finite.of_one_mem_range_dualTensorHom {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (h : 1 ∈ (dualTensorHom R M M).range) :

Module.Finite R M

If the identity linear map lies in the range of the canonical map M* ⊗[R] M → Hom_R(M, M), then M is a finite projective R-module (finite part).

source

theorem Module.Projective.of_one_mem_range_dualTensorHom {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (h : 1 ∈ (dualTensorHom R M M).range) :

Projective R M

If the identity linear map lies in the range of the canonical map M* ⊗[R] M → Hom_R(M, M), then M is a finite projective R-module (projective part).

source

noncomputable def dualTensorHomEquivOfBasis {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) :

TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N

If M is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function provides this equivalence in return for a basis of M.

Equations

dualTensorHomEquivOfBasis b = LinearEquiv.ofLinearMap (dualTensorHom R M N) (∑ i : ι, (TensorProduct.mk R (Module.Dual R M) N) (b.dualBasis i) ∘ₗ LinearMap.applyₗ (b i)) ⋯ ⋯

Instances For

source

theorem coe_dualTensorHomEquivOfBasis {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) :

⇑(dualTensorHomEquivOfBasis b) = ⇑(dualTensorHom R M N)

source

@[simp]

theorem dualTensorHomEquivOfBasis_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) :

(dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x

source

@[simp]

theorem dualTensorHomEquivOfBasis_toLinearMap {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) :

↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N

source

@[simp]

theorem dualTensorHomEquivOfBasis_symm_cancel_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) :

(dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x

source

@[simp]

theorem dualTensorHomEquivOfBasis_symm_cancel_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : M →ₗ[R] N) :

(dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x

source

theorem dualTensorHom_self_right {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] :

dualTensorHom R M R = ↑(TensorProduct.rid R (Module.Dual R M))

source

theorem dualTensorHom_finsupp {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] :

dualTensorHom R M (ι →₀ N) = LinearMap.finsuppLinearMap R ∘ₗ Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(TensorProduct.finsuppRight R R (Module.Dual R M) N ι)

source

theorem dualTensorHom_finsupp_bijective {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (fin : Finite ι ∨ Module.Finite R M) (h : Function.Bijective ⇑(dualTensorHom R M N)) :

Function.Bijective ⇑(dualTensorHom R M (ι →₀ N))

source

theorem dualTensorHom_bijective_of_comp_eq_id_right {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (g : P →ₗ[R] N) (comp_eq_id : g ∘ₗ f = LinearMap.id) (h : Function.Bijective ⇑(dualTensorHom R M P)) :

Function.Bijective ⇑(dualTensorHom R M N)

source

theorem dualTensorHom_fun_bijective {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Finite ι] (h : Function.Bijective ⇑(dualTensorHom R M N)) :

Function.Bijective ⇑(dualTensorHom R M (ι → N))

source

theorem dualTensorHom_bijective_of_finite_projective_right {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R N] [Module.Projective R N] :

Function.Bijective ⇑(dualTensorHom R M N)

source

theorem dualTensorHom_bijective_of_finite_left_projective_right {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R N] :

Function.Bijective ⇑(dualTensorHom R M N)

source

theorem dualTensorHom_bijective {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] :

Function.Bijective ⇑(dualTensorHom R M N)

source

noncomputable def dualTensorHomEquiv (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] :

TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N

If M is finite projective, the natural map $M^* ⊗ N → Hom(M, N)$ is an equivalence.

Equations

dualTensorHomEquiv R M N = LinearEquiv.ofBijective (dualTensorHom R M N) ⋯

Instances For

source

@[simp]

theorem toLinearMap_dualTensorHomEquiv {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] :

↑(dualTensorHomEquiv R M N) = dualTensorHom R M N

source

@[simp]

theorem dualTensorHomEquiv_tmul {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] (f : Module.Dual R M) (m : M) (n : N) :

((dualTensorHomEquiv R M N) (f ⊗ₜ[R] n)) m = f m • n

source

@[simp]

theorem dualTensorHomEquiv_symm_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] (x : TensorProduct R (Module.Dual R M) N) :

(dualTensorHomEquiv R M N).symm ((dualTensorHom R M N) x) = x

source

@[simp]

theorem dualTensorHom_dualTensorHomEquiv_symm {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] (x : M →ₗ[R] N) :

(dualTensorHom R M N) ((dualTensorHomEquiv R M N).symm x) = x

source

@[simp]

theorem dualTensorHomEquivOfBasis_eq_dualTensorHomEquiv {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Projective R M] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) :

dualTensorHomEquivOfBasis b = dualTensorHomEquiv R M N

source

@[deprecated dualTensorHomEquivOfBasis_eq_dualTensorHomEquiv (since := "2026-08-31")]

theorem dualTensorHomEquiv_eq_dualTensorHomEquivOfBasis {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) [DecidableEq ι] [Fintype ι] :

have this := ⋯; have this_1 := ⋯; dualTensorHomEquiv R M N = dualTensorHomEquivOfBasis b

source

noncomputable def lTensorHomEquivHomLTensor (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] :

TensorProduct R P (M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] TensorProduct R P Q

When M is a finite projective module, the map lTensorHomToHomLTensor is an equivalence. Note that lTensorHomEquivHomLTensor is not defined directly in terms of lTensorHomToHomLTensor, but the equivalence between the two is given by lTensorHomEquivHomLTensor_toLinearMap and lTensorHomEquivHomLTensor_apply.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def rTensorHomEquivHomRTensor (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] :

TensorProduct R (M →ₗ[R] P) Q ≃ₗ[R] M →ₗ[R] TensorProduct R P Q

When M is a finite projective module, the map rTensorHomToHomRTensor is an equivalence. Note that rTensorHomEquivHomRTensor is not defined directly in terms of rTensorHomToHomRTensor, but the equivalence between the two is given by rTensorHomEquivHomRTensor_toLinearMap and rTensorHomEquivHomRTensor_apply.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem lTensorHomEquivHomLTensor_toLinearMap {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] :

↑(lTensorHomEquivHomLTensor R M P Q) = TensorProduct.lTensorHomToHomLTensor (RingHom.id R) M P Q

source

@[simp]

theorem rTensorHomEquivHomRTensor_toLinearMap {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] :

↑(rTensorHomEquivHomRTensor R M P Q) = TensorProduct.rTensorHomToHomRTensor (RingHom.id R) M P Q

source

@[simp]

theorem lTensorHomEquivHomLTensor_apply {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] (x : TensorProduct R P (M →ₗ[R] Q)) :

(lTensorHomEquivHomLTensor R M P Q) x = (TensorProduct.lTensorHomToHomLTensor (RingHom.id R) M P Q) x

source

@[simp]

theorem rTensorHomEquivHomRTensor_apply {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] (x : TensorProduct R (M →ₗ[R] P) Q) :

(rTensorHomEquivHomRTensor R M P Q) x = (TensorProduct.rTensorHomToHomRTensor (RingHom.id R) M P Q) x

source

noncomputable def homTensorHomEquiv (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] [Module.Projective R N] [Module.Finite R N] :

TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q) ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P Q

When M and N are finite projective R modules, the map homTensorHomMap is an equivalence.

Equations

homTensorHomEquiv R M N P Q = LinearEquiv.ofBijective (TensorProduct.homTensorHomMap (RingHom.id R) M N P Q) ⋯

Instances For

source

@[simp]

theorem homTensorHomEquiv_toLinearMap {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] [Module.Projective R N] [Module.Finite R N] :

↑(homTensorHomEquiv R M N P Q) = TensorProduct.homTensorHomMap (RingHom.id R) M N P Q

source

@[simp]

theorem homTensorHomEquiv_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Projective R M] [Module.Finite R M] [Module.Projective R N] [Module.Finite R N] (x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)) :

(homTensorHomEquiv R M N P Q) x = (TensorProduct.homTensorHomMap (RingHom.id R) M N P Q) x

source

noncomputable def TensorProduct.dualDistribEquiv (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] :

TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct R M N)

A linear equivalence between Dual M ⊗ Dual N and Dual (M ⊗ N) when M and N are finite projective modules. It sends f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Note that dualDistribEquiv is not defined directly in terms of dualDistri, but the equivalence between the two is given by toLinearMap_dualDistribEquiv and dualDistribEquiv_tmul_tmul.

Equations

TensorProduct.dualDistribEquiv R M N = (homTensorHomEquiv R M N R R).trans (TensorProduct.rid R R).congrRight

Instances For

source

@[simp]

theorem TensorProduct.toLinearMap_dualDistribEquiv {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] :

↑(dualDistribEquiv R M N) = dualDistrib R M N

source

@[simp]

theorem TensorProduct.dualDistribEquiv_tmul_tmul {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (f : Module.Dual R M) (g : Module.Dual R N) (m : M) (n : N) :

((dualDistribEquiv R M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = g n * f m

source

@[deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

noncomputable def TensorProduct.dualDistribInvOfBasis {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) :

Module.Dual R (TensorProduct R M N) →ₗ[R] TensorProduct R (Module.Dual R M) (Module.Dual R N)

An inverse to TensorProduct.dualDistrib given bases.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

theorem TensorProduct.dualDistribInvOfBasis_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (f : Module.Dual R (TensorProduct R M N)) :

(dualDistribInvOfBasis b c) f = ∑ i : ι, ∑ j : κ, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis j

source

@[deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) :

dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

source

@[deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) :

dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id

source

@[deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

noncomputable def TensorProduct.dualDistribEquivOfBasis {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) :

TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct R M N)

A linear equivalence between Dual M ⊗ Dual N and Dual (M ⊗ N) given bases for M and N. It sends f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Equations

TensorProduct.dualDistribEquivOfBasis b c = LinearEquiv.ofLinearMap (TensorProduct.dualDistrib R M N) (TensorProduct.dualDistribInvOfBasis b c) ⋯ ⋯

Instances For

source

@[simp, deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

theorem TensorProduct.dualDistribEquivOfBasis_apply_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (x : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (x✝ : TensorProduct R M N) :

((dualDistribEquivOfBasis b c) x) x✝ = (TensorProduct.lid R R) (((homTensorHomMap (RingHom.id R) M N R R) x) x✝)

source

@[simp, deprecated TensorProduct.dualDistribEquiv (since := "2026-09-01")]

theorem TensorProduct.dualDistribEquivOfBasis_symm_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_7} {κ : Type u_8} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (a : Module.Dual R (TensorProduct R M N)) :

(dualDistribEquivOfBasis b c).symm a = (dualDistribInvOfBasis b c) a

Documentation

Mathlib.LinearAlgebra.Contraction

Contractions #

Tags #