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.
Tags #
contraction, dual module, tensor product
noncomputable def
contractLeft
(R : Type u)
(M : Type v₁)
[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 R (Module.Dual R M) M R).toFun LinearMap.id
Instances For
noncomputable def
contractRight
(R : Type u)
(M : Type v₁)
[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 R M (Module.Dual R M) R).toFun LinearMap.id.flip
Instances For
noncomputable def
dualTensorHom
(R : Type u)
(M : Type v₁)
(N : Type v₂)
[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 = let M' := Module.Dual R M; (TensorProduct.uncurry R M' N (M →ₗ[R] N)) LinearMap.smulRightₗ
Instances For
@[simp]
theorem
contractLeft_apply
{R : Type u}
{M : Type v₁}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(f : Module.Dual R M)
(m : M)
:
(contractLeft R M) (f ⊗ₜ[R] m) = f m
@[simp]
theorem
contractRight_apply
{R : Type u}
{M : Type v₁}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(f : Module.Dual R M)
(m : M)
:
(contractRight R M) (m ⊗ₜ[R] f) = f m
@[simp]
theorem
dualTensorHom_apply
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[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
@[simp]
theorem
transpose_dualTensorHom
{R : Type u}
{M : Type v₁}
[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)
@[simp]
theorem
dualTensorHom_prodMap_zero
{R : Type u}
{M : Type v₁}
{N : Type v₂}
{P : Type v₃}
{Q : Type v₄}
[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)
@[simp]
theorem
zero_prodMap_dualTensorHom
{R : Type u}
{M : Type v₁}
{N : Type v₂}
{P : Type v₃}
{Q : Type v₄}
[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)
theorem
map_dualTensorHom
{R : Type u}
{M : Type v₁}
{N : Type v₂}
{P : Type v₃}
{Q : Type v₄}
[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)
@[simp]
theorem
comp_dualTensorHom
{R : Type u}
{M : Type v₁}
{N : Type v₂}
{P : Type v₃}
[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)
theorem
toMatrix_dualTensorHom
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
{m : Type u_1}
{n : Type u_2}
[Fintype m]
[Finite n]
[DecidableEq m]
[DecidableEq n]
(bM : Basis m R M)
(bN : Basis n R N)
(j : m)
(i : n)
:
(LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.stdBasisMatrix 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
noncomputable def
dualTensorHomEquivOfBasis
{ι : Type w}
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[DecidableEq ι]
[Fintype ι]
(b : 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.ofLinear (dualTensorHom R M N) (∑ i : ι, (TensorProduct.mk R (Module.Dual R M) N) (b.dualBasis i) ∘ₗ LinearMap.applyₗ (b i)) ⋯ ⋯
Instances For
@[simp]
theorem
dualTensorHomEquivOfBasis_apply
{ι : Type w}
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[DecidableEq ι]
[Fintype ι]
(b : Basis ι R M)
(x : TensorProduct R (Module.Dual R M) N)
:
(dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x
@[simp]
theorem
dualTensorHomEquivOfBasis_toLinearMap
{ι : Type w}
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[DecidableEq ι]
[Fintype ι]
(b : Basis ι R M)
:
↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N
@[simp]
theorem
dualTensorHomEquivOfBasis_symm_cancel_left
{ι : Type w}
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[DecidableEq ι]
[Fintype ι]
(b : Basis ι R M)
(x : TensorProduct R (Module.Dual R M) N)
:
(dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
@[simp]
theorem
dualTensorHomEquivOfBasis_symm_cancel_right
{ι : Type w}
{R : Type u}
{M : Type v₁}
{N : Type v₂}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[DecidableEq ι]
[Fintype ι]
(b : Basis ι R M)
(x : M →ₗ[R] N)
:
(dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x
noncomputable def
dualTensorHomEquiv
(R : Type u)
(M : Type v₁)
(N : Type v₂)
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[Module.Free R M]
[Module.Finite R M]
:
TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N
If M is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an
equivalence.
Equations
Instances For
noncomputable def
lTensorHomEquivHomLTensor
(R : Type u)
(M : Type v₁)
(P : Type v₃)
(Q : Type v₄)
[CommRing R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
:
TensorProduct R P (M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] TensorProduct R P Q
When M is a finite free 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
noncomputable def
rTensorHomEquivHomRTensor
(R : Type u)
(M : Type v₁)
(P : Type v₃)
(Q : Type v₄)
[CommRing R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
:
TensorProduct R (M →ₗ[R] P) Q ≃ₗ[R] M →ₗ[R] TensorProduct R P Q
When M is a finite free 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
@[simp]
theorem
lTensorHomEquivHomLTensor_toLinearMap
(R : Type u)
(M : Type v₁)
(P : Type v₃)
(Q : Type v₄)
[CommRing R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
:
↑(lTensorHomEquivHomLTensor R M P Q) = TensorProduct.lTensorHomToHomLTensor R M P Q
@[simp]
theorem
rTensorHomEquivHomRTensor_toLinearMap
(R : Type u)
(M : Type v₁)
(P : Type v₃)
(Q : Type v₄)
[CommRing R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
:
↑(rTensorHomEquivHomRTensor R M P Q) = TensorProduct.rTensorHomToHomRTensor R M P Q
@[simp]
theorem
lTensorHomEquivHomLTensor_apply
{R : Type u}
{M : Type v₁}
{P : Type v₃}
{Q : Type v₄}
[CommRing R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
(x : TensorProduct R P (M →ₗ[R] Q))
:
(lTensorHomEquivHomLTensor R M P Q) x = (TensorProduct.lTensorHomToHomLTensor R M P Q) x
@[simp]
theorem
rTensorHomEquivHomRTensor_apply
{R : Type u}
{M : Type v₁}
{P : Type v₃}
{Q : Type v₄}
[CommRing R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
(x : TensorProduct R (M →ₗ[R] P) Q)
:
(rTensorHomEquivHomRTensor R M P Q) x = (TensorProduct.rTensorHomToHomRTensor R M P Q) x
noncomputable def
homTensorHomEquiv
(R : Type u)
(M : Type v₁)
(N : Type v₂)
(P : Type v₃)
(Q : Type v₄)
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
[Module.Free 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 free R modules, the map homTensorHomMap is an equivalence. Note that
homTensorHomEquiv is not defined directly in terms of homTensorHomMap, but the equivalence
between the two is given by homTensorHomEquiv_toLinearMap and homTensorHomEquiv_apply.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
homTensorHomEquiv_toLinearMap
(R : Type u)
(M : Type v₁)
(N : Type v₂)
(P : Type v₃)
(Q : Type v₄)
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
[Module.Free R N]
[Module.Finite R N]
:
↑(homTensorHomEquiv R M N P Q) = TensorProduct.homTensorHomMap R M N P Q
@[simp]
theorem
homTensorHomEquiv_apply
{R : Type u}
{M : Type v₁}
{N : Type v₂}
{P : Type v₃}
{Q : Type v₄}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[AddCommGroup P]
[AddCommGroup Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
[Module.Free R M]
[Module.Finite R M]
[Module.Free R N]
[Module.Finite R N]
(x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q))
:
(homTensorHomEquiv R M N P Q) x = (TensorProduct.homTensorHomMap R M N P Q) x