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₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₁] [AddCommMonoid M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] : TensorProduct R (LinearMap.BilinForm A M₁) (LinearMap.BilinForm R M₂) →ₗ[A] LinearMap.BilinForm A (TensorProduct R M₁ 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.

@[simp]

theorem LinearMap.BilinForm.tensorDistrib_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₁] [AddCommMonoid M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] (B₁ : LinearMap.BilinForm A M₁) (B₂ : LinearMap.BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : (((LinearMap.BilinForm.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' • (B₁ m₁) m₁'

@[reducible]

noncomputable def LinearMap.BilinForm.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₁] [AddCommMonoid M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] (B₁ : LinearMap.BilinForm A M₁) (B₂ : LinearMap.BilinForm R M₂) : LinearMap.BilinForm A (TensorProduct R M₁ M₂)

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

Equations

• LinearMap.BilinForm.tmul B₁ B₂ = (LinearMap.BilinForm.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)

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

A tensor product of symmetric bilinear forms is symmetric.

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

The base change of a bilinear form.

Equations

• LinearMap.BilinForm.baseChange A B = LinearMap.BilinForm.tmul (LinearMap.mul A A) B

@[simp]

theorem LinearMap.BilinForm.baseChange_tmul {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₂] [Algebra R A] [Module R M₂] (B₂ : LinearMap.BilinForm R M₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : ((LinearMap.BilinForm.baseChange A B₂) (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₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₂] [Algebra R A] [Module R M₂] {B₂ : LinearMap.BilinForm R M₂} (hB₂ : LinearMap.IsSymm B₂) : LinearMap.IsSymm (LinearMap.BilinForm.baseChange A B₂)

The base change of a symmetric bilinear form is symmetric.

noncomputable def LinearMap.BilinForm.tensorDistribEquiv (R : Type uR) {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] : TensorProduct R (LinearMap.BilinForm R M₁) (LinearMap.BilinForm R M₂) ≃ₗ[R] LinearMap.BilinForm R (TensorProduct R M₁ M₂)

tensorDistrib as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.BilinForm.tensorDistribEquiv_tmul {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] (B₁ : LinearMap.BilinForm R M₁) (B₂ : LinearMap.BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : (((LinearMap.BilinForm.tensorDistribEquiv R) (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₂) [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] : ↑(LinearMap.BilinForm.tensorDistribEquiv R) = LinearMap.BilinForm.tensorDistrib R R

@[simp]

theorem LinearMap.BilinForm.tensorDistribEquiv_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] (B : TensorProduct R (LinearMap.BilinForm R M₁) (LinearMap.BilinForm R M₂)) : (LinearMap.BilinForm.tensorDistribEquiv R) B = (LinearMap.BilinForm.tensorDistrib R R) B