Basis.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

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.

abbrev OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair line 23
Source documentation
Affine coefficient pairs of forms of bidegree (e,1).
```
abbrev BoundedPair (R : Type*) [CommRing R] (e : ℕ) :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget line 27
Source documentation
Forget the degree bounds in the affine representation of binary forms.
```
def forget (e : ℕ) : BoundedPair R e →ₗ[R] DeterminantKernel.FormPair R where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_injective line 32
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.quotientVector line 39
Source documentation
A quotient vector with both coefficient polynomials of degree at most e.
```
def quotientVector (e : ℕ) (j : Fin (e + 2)) : BoundedPair R e :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.kernelVector line 46
Source documentation
A bounded kernel vector, obtained by multiplication by uw-vs.
```
def kernelVector (e : ℕ) (j : Fin e) : BoundedPair R e :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.vector line 54
Source documentation
The quotient vectors first, followed by the determinant-kernel vectors.
```
def vector (e : ℕ) : (Fin (e + 2) ⊕ Fin e) → BoundedPair R e :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_quotientVector line 57
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_kernelVector line 62
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_vector line 69
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.vector_linearIndependent line 75
Source documentation
Linear independence holds over a general commutative coefficient ring.
```
theorem vector_linearIndependent (e : ℕ) : LinearIndependent R (vector (R := R) e) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.vector
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.finrank_boundedPair line 81
Source documentation
The dimension of the original space of forms is twice e+1.
```
theorem finrank_boundedPair (K : Type*) [Field K] (e : ℕ) :
    Module.finrank K (BoundedPair K e) = 2 * (e + 1) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.basis line 89
Source documentation
The fixed simultaneous change of basis used in the determinant degeneration.
```
def basis (K : Type*) [Field K] (e : ℕ) :
    Module.Basis (Fin (e + 2) ⊕ Fin e) K (BoundedPair K e) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.basis_apply line 95
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget_basis line 101
Source documentation
Forgetting degree bounds identifies the finite basis with the explicit polynomial-pair formulas.
```
@[simp] theorem forget_basis (K : Type*) [Field K] (e : ℕ)
    (j : Fin (e + 2) ⊕ Fin e) :
    forget e (basis K e j) =
      Sum.elim (DeterminantKernel.quotientVector e) (DeterminantKernel.kernelVector e) j := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.forget, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.basis, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelVector