The bilinear form on a tensor product #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
bilin_form.tensor_distrib (B₁ ⊗ₜ B₂): the bilinear form onM₁ ⊗ M₂constructed by applyingB₁onM₁andB₂onM₂.bilin_form.tensor_distrib_equiv:bilin_form.tensor_distribas an equivalence on finite free modules.
def
bilin_form.tensor_distrib
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂] :
tensor_product R (bilin_form R M₁) (bilin_form R M₂) →ₗ[R] bilin_form R (tensor_product R M₁ M₂)
The tensor product of two bilinear forms injects into bilinear forms on tensor products.
Equations
- bilin_form.tensor_distrib = (((tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂).dual_map.trans (tensor_product.lift.equiv R (tensor_product R M₁ M₂) (tensor_product R M₁ M₂) R).symm).trans linear_map.to_bilin).to_linear_map.comp ((tensor_product.dual_distrib R (tensor_product R M₁ M₁) (tensor_product R M₂ M₂)).comp (tensor_product.congr (bilin_form.to_lin.trans (tensor_product.lift.equiv R M₁ M₁ R)) (bilin_form.to_lin.trans (tensor_product.lift.equiv R M₂ M₂ R))).to_linear_map)
@[simp]
theorem
bilin_form.tensor_distrib_tmul
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(B₁ : bilin_form R M₁)
(B₂ : bilin_form R M₂)
(m₁ : M₁)
(m₂ : M₂)
(m₁' : M₁)
(m₂' : M₂) :
@[protected, reducible]
def
bilin_form.tmul
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(B₁ : bilin_form R M₁)
(B₂ : bilin_form R M₂) :
bilin_form R (tensor_product R M₁ M₂)
The tensor product of two bilinear forms, a shorthand for dot notation.
noncomputable
def
bilin_form.tensor_distrib_equiv
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[comm_ring R]
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
[module.free R M₁]
[module.finite R M₁]
[module.free R M₂]
[module.finite R M₂]
[nontrivial R] :
tensor_product R (bilin_form R M₁) (bilin_form R M₂) ≃ₗ[R] bilin_form R (tensor_product R M₁ M₂)
tensor_distrib as an equivalence.
Equations
- bilin_form.tensor_distrib_equiv = ((((tensor_product.congr (bilin_form.to_lin.trans (tensor_product.lift.equiv R M₁ M₁ R)) (bilin_form.to_lin.trans (tensor_product.lift.equiv R M₂ M₂ R))).trans (tensor_product.dual_distrib_equiv R (tensor_product R M₁ M₁) (tensor_product R M₂ M₂))).trans (tensor_product.tensor_tensor_tensor_comm R M₁ M₂ M₁ M₂).dual_map).trans (tensor_product.lift.equiv R (tensor_product R M₁ M₂) (tensor_product R M₁ M₂) R).symm).trans linear_map.to_bilin
@[simp]
theorem
bilin_form.tensor_distrib_equiv_apply
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[comm_ring R]
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
[module.free R M₁]
[module.finite R M₁]
[module.free R M₂]
[module.finite R M₂]
[nontrivial R]
(B : tensor_product R (bilin_form R M₁) (bilin_form R M₂)) :