Documentation

Mathlib.LinearAlgebra.BilinearForm.TensorProduct

The bilinear form on a tensor product #

Main definitions #

noncomputable def LinearMap.BilinMap.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₂] :

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.BilinMap.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.BilinMap.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' (B₁ m₁) m₁'
    @[reducible, inline]
    noncomputable abbrev LinearMap.BilinMap.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.BilinMap A M₁ A) (B₂ : LinearMap.BilinMap R M₂ R) :

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

      A tensor product of symmetric bilinear forms is symmetric.

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

      The base change of a bilinear form.

      Equations
      Instances For
        @[simp]
        theorem LinearMap.BilinMap.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.BilinMap R M₂ R) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) :
        ((LinearMap.BilinMap.baseChange A B₂) (a ⊗ₜ[R] m₂)) (a' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' (a * a')
        theorem LinearMap.BilinMap.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₂) :

        The base change of a symmetric bilinear form is symmetric.

        noncomputable def LinearMap.BilinMap.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₂] :

        tensorDistrib as an equivalence.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem LinearMap.BilinMap.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.BilinMap.tensorDistribEquiv R) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₁ m₁) m₁' * (B₂ m₂) m₂'
          @[simp]
          @[simp]