Contractions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
def
contract_left
(R : Type u_2)
(M : Type u_3)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
tensor_product R (module.dual R M) M →ₗ[R] R
The natural left-handed pairing between a module and its dual.
Equations
- contract_left R M = (tensor_product.uncurry R (module.dual R M) M R).to_fun linear_map.id
def
contract_right
(R : Type u_2)
(M : Type u_3)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
tensor_product R M (module.dual R M) →ₗ[R] R
The natural right-handed pairing between a module and its dual.
Equations
- contract_right R M = (tensor_product.uncurry R M (module.dual R M) R).to_fun linear_map.id.flip
def
dual_tensor_hom
(R : Type u_2)
(M : Type u_3)
(N : Type u_4)
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
tensor_product 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
- dual_tensor_hom R M N = let M' : Type (max u_3 u_2) := module.dual R M in ⇑(tensor_product.uncurry R M' N (M →ₗ[R] N)) linear_map.smul_rightₗ
@[simp]
theorem
contract_left_apply
{R : Type u_2}
{M : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(f : module.dual R M)
(m : M) :
@[simp]
theorem
contract_right_apply
{R : Type u_2}
{M : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(f : module.dual R M)
(m : M) :
@[simp]
theorem
dual_tensor_hom_apply
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : module.dual R M)
(m : M)
(n : N) :
@[simp]
theorem
transpose_dual_tensor_hom
{R : Type u_2}
{M : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(f : module.dual R M)
(m : M) :
⇑module.dual.transpose (⇑(dual_tensor_hom R M M) (f ⊗ₜ[R] m)) = ⇑(dual_tensor_hom R (module.dual R M) (module.dual R M)) (⇑(module.dual.eval R M) m ⊗ₜ[R] f)
@[simp]
theorem
dual_tensor_hom_prod_map_zero
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : module.dual R M)
(p : P) :
(⇑(dual_tensor_hom R M P) (f ⊗ₜ[R] p)).prod_map 0 = ⇑(dual_tensor_hom R (M × N) (P × Q)) (linear_map.comp f (linear_map.fst R M N) ⊗ₜ[R] ⇑(linear_map.inl R P Q) p)
@[simp]
theorem
zero_prod_map_dual_tensor_hom
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(g : module.dual R N)
(q : Q) :
0.prod_map (⇑(dual_tensor_hom R N Q) (g ⊗ₜ[R] q)) = ⇑(dual_tensor_hom R (M × N) (P × Q)) (linear_map.comp g (linear_map.snd R M N) ⊗ₜ[R] ⇑(linear_map.inr R P Q) q)
theorem
map_dual_tensor_hom
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid 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) :
tensor_product.map (⇑(dual_tensor_hom R M P) (f ⊗ₜ[R] p)) (⇑(dual_tensor_hom R N Q) (g ⊗ₜ[R] q)) = ⇑(dual_tensor_hom R (tensor_product R M N) (tensor_product R P Q)) (⇑(tensor_product.dual_distrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))
@[simp]
theorem
comp_dual_tensor_hom
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : module.dual R M)
(n : N)
(g : module.dual R N)
(p : P) :
theorem
to_matrix_dual_tensor_hom
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
{m : Type u_1}
{n : Type u_5}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
(bM : basis m R M)
(bN : basis n R N)
(j : m)
(i : n) :
⇑(linear_map.to_matrix bM bN) (⇑(dual_tensor_hom R M N) (bM.coord j ⊗ₜ[R] ⇑bN i)) = matrix.std_basis_matrix i j 1
As a matrix, dual_tensor_hom evaluated on a basis element of M* ⊗ N is a matrix with a
single one and zeros elsewhere
noncomputable
def
dual_tensor_hom_equiv_of_basis
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[decidable_eq ι]
[fintype ι]
(b : basis ι R M) :
tensor_product 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
- dual_tensor_hom_equiv_of_basis b = linear_equiv.of_linear (dual_tensor_hom R M N) (finset.univ.sum (λ (i : ι), (⇑(tensor_product.mk R (module.dual R M) N) (⇑(b.dual_basis) i)).comp (⇑linear_map.applyₗ (⇑b i)))) _ _
@[simp]
theorem
dual_tensor_hom_equiv_of_basis_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(ᾰ : tensor_product R (module.dual R M) N) :
⇑(dual_tensor_hom_equiv_of_basis b) ᾰ = ⇑(dual_tensor_hom R M N) ᾰ
@[simp]
theorem
dual_tensor_hom_equiv_of_basis_to_linear_map
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[decidable_eq ι]
[fintype ι]
(b : basis ι R M) :
@[simp]
theorem
dual_tensor_hom_equiv_of_basis_symm_cancel_left
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(x : tensor_product R (module.dual R M) N) :
⇑((dual_tensor_hom_equiv_of_basis b).symm) (⇑(dual_tensor_hom R M N) x) = x
@[simp]
theorem
dual_tensor_hom_equiv_of_basis_symm_cancel_right
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(x : M →ₗ[R] N) :
⇑(dual_tensor_hom R M N) (⇑((dual_tensor_hom_equiv_of_basis b).symm) x) = x
@[simp]
noncomputable
def
dual_tensor_hom_equiv
(R : Type u_2)
(M : Type u_3)
(N : Type u_4)
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[module.free R M]
[module.finite R M]
[nontrivial R] :
tensor_product 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
noncomputable
def
ltensor_hom_equiv_hom_ltensor
(R : Type u_2)
(M : Type u_3)
(P : Type u_5)
(Q : Type u_6)
[comm_ring R]
[add_comm_group M]
[add_comm_group P]
[add_comm_group Q]
[module R M]
[module R P]
[module R Q]
[module.free R M]
[module.finite R M]
[nontrivial R] :
tensor_product R P (M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] tensor_product R P Q
When M is a finite free module, the map ltensor_hom_to_hom_ltensor is an equivalence. Note
that ltensor_hom_equiv_hom_ltensor is not defined directly in terms of
ltensor_hom_to_hom_ltensor, but the equivalence between the two is given by
ltensor_hom_equiv_hom_ltensor_to_linear_map and ltensor_hom_equiv_hom_ltensor_apply.
Equations
- ltensor_hom_equiv_hom_ltensor R M P Q = ((tensor_product.congr (linear_equiv.refl R P) (dual_tensor_hom_equiv R M Q).symm).trans (tensor_product.left_comm R P (module.dual R M) Q)).trans (dual_tensor_hom_equiv R M (tensor_product R P Q))
noncomputable
def
rtensor_hom_equiv_hom_rtensor
(R : Type u_2)
(M : Type u_3)
(P : Type u_5)
(Q : Type u_6)
[comm_ring R]
[add_comm_group M]
[add_comm_group P]
[add_comm_group Q]
[module R M]
[module R P]
[module R Q]
[module.free R M]
[module.finite R M]
[nontrivial R] :
tensor_product R (M →ₗ[R] P) Q ≃ₗ[R] M →ₗ[R] tensor_product R P Q
When M is a finite free module, the map rtensor_hom_to_hom_rtensor is an equivalence. Note
that rtensor_hom_equiv_hom_rtensor is not defined directly in terms of
rtensor_hom_to_hom_rtensor, but the equivalence between the two is given by
rtensor_hom_equiv_hom_rtensor_to_linear_map and rtensor_hom_equiv_hom_rtensor_apply.
Equations
- rtensor_hom_equiv_hom_rtensor R M P Q = ((tensor_product.congr (dual_tensor_hom_equiv R M P).symm (linear_equiv.refl R Q)).trans (tensor_product.assoc R (module.dual R M) P Q)).trans (dual_tensor_hom_equiv R M (tensor_product R P Q))
@[simp]
theorem
ltensor_hom_equiv_hom_ltensor_to_linear_map
(R : Type u_2)
(M : Type u_3)
(P : Type u_5)
(Q : Type u_6)
[comm_ring R]
[add_comm_group M]
[add_comm_group P]
[add_comm_group Q]
[module R M]
[module R P]
[module R Q]
[module.free R M]
[module.finite R M]
[nontrivial R] :
(ltensor_hom_equiv_hom_ltensor R M P Q).to_linear_map = tensor_product.ltensor_hom_to_hom_ltensor R M P Q
@[simp]
theorem
rtensor_hom_equiv_hom_rtensor_to_linear_map
(R : Type u_2)
(M : Type u_3)
(P : Type u_5)
(Q : Type u_6)
[comm_ring R]
[add_comm_group M]
[add_comm_group P]
[add_comm_group Q]
[module R M]
[module R P]
[module R Q]
[module.free R M]
[module.finite R M]
[nontrivial R] :
(rtensor_hom_equiv_hom_rtensor R M P Q).to_linear_map = tensor_product.rtensor_hom_to_hom_rtensor R M P Q
@[simp]
theorem
ltensor_hom_equiv_hom_ltensor_apply
{R : Type u_2}
{M : Type u_3}
{P : Type u_5}
{Q : Type u_6}
[comm_ring R]
[add_comm_group M]
[add_comm_group P]
[add_comm_group Q]
[module R M]
[module R P]
[module R Q]
[module.free R M]
[module.finite R M]
[nontrivial R]
(x : tensor_product R P (M →ₗ[R] Q)) :
⇑(ltensor_hom_equiv_hom_ltensor R M P Q) x = ⇑(tensor_product.ltensor_hom_to_hom_ltensor R M P Q) x
@[simp]
theorem
rtensor_hom_equiv_hom_rtensor_apply
{R : Type u_2}
{M : Type u_3}
{P : Type u_5}
{Q : Type u_6}
[comm_ring R]
[add_comm_group M]
[add_comm_group P]
[add_comm_group Q]
[module R M]
[module R P]
[module R Q]
[module.free R M]
[module.finite R M]
[nontrivial R]
(x : tensor_product R (M →ₗ[R] P) Q) :
⇑(rtensor_hom_equiv_hom_rtensor R M P Q) x = ⇑(tensor_product.rtensor_hom_to_hom_rtensor R M P Q) x
noncomputable
def
hom_tensor_hom_equiv
(R : Type u_2)
(M : Type u_3)
(N : Type u_4)
(P : Type u_5)
(Q : Type u_6)
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[add_comm_group 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]
[nontrivial R] :
tensor_product R (M →ₗ[R] P) (N →ₗ[R] Q) ≃ₗ[R] tensor_product R M N →ₗ[R] tensor_product R P Q
When M and N are free R modules, the map hom_tensor_hom_map is an equivalence. Note that
hom_tensor_hom_equiv is not defined directly in terms of hom_tensor_hom_map, but the equivalence
between the two is given by hom_tensor_hom_equiv_to_linear_map and hom_tensor_hom_equiv_apply.
Equations
- hom_tensor_hom_equiv R M N P Q = ((rtensor_hom_equiv_hom_rtensor R M P (N →ₗ[R] Q)).trans ((linear_equiv.refl R M).arrow_congr (ltensor_hom_equiv_hom_ltensor R N P Q))).trans (tensor_product.lift.equiv R M N (tensor_product R P Q))
@[simp]
theorem
hom_tensor_hom_equiv_to_linear_map
(R : Type u_2)
(M : Type u_3)
(N : Type u_4)
(P : Type u_5)
(Q : Type u_6)
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[add_comm_group 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]
[nontrivial R] :
(hom_tensor_hom_equiv R M N P Q).to_linear_map = tensor_product.hom_tensor_hom_map R M N P Q
@[simp]
theorem
hom_tensor_hom_equiv_apply
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
{Q : Type u_6}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[add_comm_group P]
[add_comm_group 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]
[nontrivial R]
(x : tensor_product R (M →ₗ[R] P) (N →ₗ[R] Q)) :
⇑(hom_tensor_hom_equiv R M N P Q) x = ⇑(tensor_product.hom_tensor_hom_map R M N P Q) x