mathlib3 documentation

linear_algebra.bilinear_form.tensor_product

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 #

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₂] :

The tensor product of two bilinear forms injects into bilinear forms on tensor products.

Equations
@[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₂) :
(bilin_form.tensor_distrib (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂) (m₁' ⊗ₜ[R] m₂') = B₁ m₁ m₁' * B₂ 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.

Equations
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_distrib as an equivalence.

Equations
@[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₂)) :