The bilinear form on a tensor product

Main definitions

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

def LinearMap.BilinMap.tensorDistrib (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [SMulCommClass R A N₁] [IsScalarTower R A N₁] [Module R M₂] [Module R N₂] : TensorProduct R (LinearMap.BilinMap A M₁ N₁) (LinearMap.BilinMap R M₂ N₂) →ₗ[A] LinearMap.BilinMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)

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

Note this is heterobasic; the bilinear map on the left can take values in a module over a (commutative) algebra over the ring of the module in which the right bilinear map is valued.

@[simp]

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

@[reducible, inline]

abbrev LinearMap.BilinMap.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [SMulCommClass R A N₁] [IsScalarTower R A N₁] [Module R M₂] [Module R N₂] (B₁ : LinearMap.BilinMap A M₁ N₁) (B₂ : LinearMap.BilinMap R M₂ N₂) : LinearMap.BilinMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)

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

theorem LinearMap.BilinMap.tmul_isSymm {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [SMulCommClass R A N₁] [IsScalarTower R A N₁] [Module R M₂] [Module R N₂] {B₁ : LinearMap.BilinMap A M₁ N₁} {B₂ : LinearMap.BilinMap R M₂ N₂} (hB₁ : ∀ (x y : M₁), (B₁ x) y = (B₁ y) x) (hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x) (x y : TensorProduct R M₁ M₂) : ((B₁.tmul B₂) x) y = ((B₁.tmul B₂) y) x

A tensor product of symmetric bilinear maps is symmetric.

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

The base change of a bilinear map (also known as "extension of scalars").

@[simp]

theorem LinearMap.BilinMap.baseChange_tmul {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₂ : Type uN₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₂] [AddCommMonoid N₂] [Algebra R A] [Module R M₂] [Module R N₂] (B₂ : LinearMap.BilinMap R M₂ N₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : ((BilinMap.baseChange A B₂) (a ⊗ₜ[R] m₂)) (a' ⊗ₜ[R] m₂') = (a * a') ⊗ₜ[R] (B₂ m₂) m₂'

theorem LinearMap.BilinMap.baseChange_isSymm {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₂ : Type uN₂} [CommSemiring R] [CommSemiring A] [AddCommMonoid M₂] [AddCommMonoid N₂] [Algebra R A] [Module R M₂] [Module R N₂] {B₂ : LinearMap.BilinMap R M₂ N₂} (hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x) (x y : TensorProduct R A M₂) : ((BilinMap.baseChange A B₂) x) y = ((BilinMap.baseChange A B₂) y) x

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.

@[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₂) : (((tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' • (B₁ m₁) m₁'

@[reducible, inline]

abbrev 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.BilinMap R M₂ R) : LinearMap.BilinMap A (TensorProduct R M₁ M₂) A

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

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₁ : IsSymm B₁) (hB₂ : IsSymm B₂) : IsSymm (B₁.tmul B₂)

A tensor product of symmetric bilinear forms is symmetric.

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.

@[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₂) : ((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₂ : IsSymm B₂) : IsSymm (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.

@[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₂) : (((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₂] : ↑(tensorDistribEquiv R) = 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₂)) : (tensorDistribEquiv R) B = (tensorDistrib R R) B