# The bilinear form on a tensor product #

## Main definitions #

• LinearMap.BilinForm.tensorDistrib (B₁ ⊗ₜ B₂): the bilinear form on M₁ ⊗ M₂ constructed by applying B₁ on M₁ and B₂ on M₂.
• LinearMap.BilinForm.tensorDistribEquiv: BilinForm.tensorDistrib as an equivalence on finite free modules.
noncomputable def LinearMap.BilinForm.tensorDistrib (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] :

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

Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra over the ring in which the right bilinear form is valued.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.BilinForm.tensorDistrib_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] (B₁ : ) (B₂ : ) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) :
(( (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' (B₁ m₁) m₁'
@[reducible, inline]
noncomputable abbrev LinearMap.BilinForm.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] (B₁ : ) (B₂ : ) :

The tensor product of two bilinear forms, a shorthand for dot notation.

Equations
Instances For
theorem LinearMap.IsSymm.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] {B₁ : } {B₂ : } (hB₁ : ) (hB₂ : ) :
LinearMap.IsSymm (B₁.tmul B₂)

A tensor product of symmetric bilinear forms is symmetric.

noncomputable def LinearMap.BilinForm.baseChange {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [] [] [] [Algebra R A] [Module R M₂] (B : ) :

The base change of a bilinear form.

Equations
Instances For
@[simp]
theorem LinearMap.BilinForm.baseChange_tmul {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [] [] [] [Algebra R A] [Module R M₂] (B₂ : ) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) :
( (a ⊗ₜ[R] m₂)) (a' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' (a * a')
theorem LinearMap.BilinForm.IsSymm.baseChange {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [] [] [] [Algebra R A] [Module R M₂] {B₂ : } (hB₂ : ) :

The base change of a symmetric bilinear form is symmetric.

noncomputable def LinearMap.BilinForm.tensorDistribEquiv (R : Type uR) {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [Module R M₁] [Module R M₂] [Module.Free R M₁] [] [Module.Free R M₂] [] :

tensorDistrib as an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.BilinForm.tensorDistribEquiv_tmul {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [Module R M₁] [Module R M₂] [Module.Free R M₁] [] [Module.Free R M₂] [] (B₁ : ) (B₂ : ) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) :
(( (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₁ m₁) m₁' * (B₂ m₂) m₂'
@[simp]
theorem LinearMap.BilinForm.tensorDistribEquiv_toLinearMap (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) [] [] [] [Module R M₁] [Module R M₂] [Module.Free R M₁] [] [Module.Free R M₂] [] :
@[simp]
theorem LinearMap.BilinForm.tensorDistribEquiv_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [Module R M₁] [Module R M₂] [Module.Free R M₁] [] [Module.Free R M₂] [] (B : TensorProduct R () ()) :