Documentation

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

The quadratic form on a tensor product #

Main definitions #

noncomputable def QuadraticForm.tensorDistrib (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] :

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

Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right.

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

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

    Equations
    Instances For
      theorem QuadraticForm.associated_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] [Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
      QuadraticMap.associated (Q₁.tmul Q₂) = (QuadraticMap.associated Q₁).tmul (QuadraticMap.associated Q₂)
      theorem QuadraticForm.polarBilin_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] [Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
      noncomputable def QuadraticForm.baseChange {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] (Q : QuadraticForm R M₂) :

      The base change of a quadratic form.

      Equations
      Instances For
        @[simp]
        theorem QuadraticForm.baseChange_tmul {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) :
        (QuadraticForm.baseChange A Q) (a ⊗ₜ[R] m₂) = Q m₂ (a * a)
        theorem QuadraticForm.associated_baseChange {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] [Invertible 2] (Q : QuadraticForm R M₂) :
        QuadraticMap.associated (QuadraticForm.baseChange A Q) = LinearMap.BilinMap.baseChange A (QuadraticMap.associated Q)
        theorem QuadraticForm.baseChange_ext {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] ⦃Q₁ : QuadraticForm A (TensorProduct R A M₂) ⦃Q₂ : QuadraticForm A (TensorProduct R A M₂) (h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)) :
        Q₁ = Q₂

        If two quadratic forms from A ⊗[R] M₂ agree on elements of the form 1 ⊗ m, they are equal.

        In other words, if a base change exists for a quadratic form, it is unique.

        Note that unlike QuadraticForm.baseChange, this does not need Invertible (2 : R).