Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Determinant.Basis

The finite adapted basis for the determinant filtration #

The quotient vectors and determinant-kernel vectors of Section 5.1 form a basis of the actual space of bidegree (e,1) forms. The proof works over every field, including in the boundary case e = 0 where the kernel has dimension zero.

source
@[reducible, inline]
abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair (R : Type u_2) [CommRing R] (e : ℕ) :
Type u_2

Affine coefficient pairs of forms of bidegree (e,1).

Equations
Instances For
    source
    def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget {R : Type u_1} [CommRing R] (e : ℕ) :
    BoundedPair R e →ₗ[R] DeterminantKernel.FormPair R

    Forget the degree bounds in the affine representation of binary forms.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_injective {R : Type u_1} [CommRing R] (e : ℕ) :
      Function.Injective ⇑(forget e)
      source
      noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.quotientVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin (e + 2)) :
      BoundedPair R e

      A quotient vector with both coefficient polynomials of degree at most e.

      Equations
      Instances For
        source
        noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.kernelVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin e) :
        BoundedPair R e

        A bounded kernel vector, obtained by multiplication by uw-vs.

        Equations
        Instances For
          source
          noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.vector {R : Type u_1} [CommRing R] (e : ℕ) :
          Fin (e + 2) ⊕ Fin e → BoundedPair R e

          The quotient vectors first, followed by the determinant-kernel vectors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_quotientVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin (e + 2)) :
            (forget e) (quotientVector e j) = DeterminantKernel.quotientVector e j
            source
            @[simp]
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_kernelVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin e) :
            (forget e) (kernelVector e j) = DeterminantKernel.kernelVector e j
            source
            @[simp]
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_vector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin (e + 2) ⊕ Fin e) :
            (forget e) (vector e j) = Sum.elim (DeterminantKernel.quotientVector e) (DeterminantKernel.kernelVector e) j
            source
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.vector_linearIndependent {R : Type u_1} [CommRing R] (e : ℕ) :
            LinearIndependent R (vector e)

            Linear independence holds over a general commutative coefficient ring.

            source
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.finrank_boundedPair (K : Type u_2) [Field K] (e : ℕ) :
            Module.finrank K (BoundedPair K e) = 2 * (e + 1)

            The dimension of the original space of forms is twice e+1.

            source
            noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.basis (K : Type u_2) [Field K] (e : ℕ) :
            Module.Basis (Fin (e + 2) ⊕ Fin e) K (BoundedPair K e)

            The fixed simultaneous change of basis used in the determinant degeneration.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.basis_apply (K : Type u_2) [Field K] (e : ℕ) (j : Fin (e + 2) ⊕ Fin e) :
              (basis K e) j = vector e j
              source
              theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_basis (K : Type u_2) [Field K] (e : ℕ) (j : Fin (e + 2) ⊕ Fin e) :
              (forget e) ((basis K e) j) = Sum.elim (DeterminantKernel.quotientVector e) (DeterminantKernel.kernelVector e) j

              Forgetting degree bounds identifies the finite basis with the explicit polynomial-pair formulas.