The bilinear form on a tensor product

Main definitions

• BilinForm.tensorDistrib (B₁ ⊗ₜ B₂): the bilinear form on M₁ ⊗ M₂ constructed by applying B₁ on M₁ and B₂ on M₂.
• BilinForm.tensorDistribEquiv: BilinForm.tensorDistrib as an equivalence on finite free modules.

noncomputable def 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 (BilinForm A M₁) (BilinForm R M₂) →ₗ[A] 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 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₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : ((BilinForm.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)).bilin (m₁ ⊗ₜ[R] m₂) (m₁' ⊗ₜ[R] m₂') = B₂.bilin m₂ m₂' • B₁.bilin m₁ m₁'

@[reducible]

noncomputable def 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₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (TensorProduct R M₁ M₂)

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

Equations

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

theorem BilinForm.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₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} (hB₁ : BilinForm.IsSymm B₁) (hB₂ : BilinForm.IsSymm B₂) : BilinForm.IsSymm (BilinForm.tmul B₁ B₂)

A tensor product of symmetric bilinear forms is symmetric.

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

The base change of a bilinear form.

Equations

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

@[simp]

theorem 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₂ : BilinForm R M₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : (BilinForm.baseChange A B₂).bilin (a ⊗ₜ[R] m₂) (a' ⊗ₜ[R] m₂') = B₂.bilin m₂ m₂' • (a * a')

theorem 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₂ : BilinForm R M₂} (hB₂ : BilinForm.IsSymm B₂) : BilinForm.IsSymm (BilinForm.baseChange A B₂)

The base change of a symmetric bilinear form is symmetric.

noncomputable def 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 (BilinForm R M₁) (BilinForm R M₂) ≃ₗ[R] 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 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₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : ((BilinForm.tensorDistribEquiv R) (B₁ ⊗ₜ[R] B₂)).bilin (m₁ ⊗ₜ[R] m₂) (m₁' ⊗ₜ[R] m₂') = B₁.bilin m₁ m₁' * B₂.bilin m₂ m₂'

@[simp]

theorem 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₂] : ↑(BilinForm.tensorDistribEquiv R) = BilinForm.tensorDistrib R R

@[simp]

theorem 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 (BilinForm R M₁) (BilinForm R M₂)) : (BilinForm.tensorDistribEquiv R) B = (BilinForm.tensorDistrib R R) B