Kernel.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

The determinant kernel of diagonal substitution

A form A(u,v)s + B(u,v)w of bidegree (e,1) is represented on the affine chart u = 1 by the polynomial pair (A(1,X), B(1,X)). Diagonal substitution becomes (A,B) ↦ A + X * B, and multiplication by uw - vs becomes p ↦ (-X * p, p).

The identities here hold over every commutative ring. They include the fixed quotient/kernel coordinates and the monomial identities underlying the simultaneous triangularization in Section 5.1 of Matrix Multiplication via Auxiliary Separation and Polynomial Multiplication.

abbrev OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair line 29
Source documentation
Affine representatives of forms linear in the second pair of variables.
```
abbrev FormPair (R : Type*) [CommRing R] := R[X] × R[X]
```
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal line 32
Source documentation
Substitute the first variable pair into the second variable pair.
```
def diagonal : FormPair R →ₗ[R] R[X] where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant line 38
Source documentation
Multiplication by D = uw - vs after putting u = 1.
```
def determinant : R[X] →ₗ[R] FormPair R where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_apply line 45
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant_apply line 47
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_determinant line 49
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant_injective line 53
Source documentation
The determinant factor can be recovered from the second component.
```
theorem determinant_injective : Function.Injective (determinant (R := R)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_eq_zero_iff line 58
Source documentation
Vanishing after diagonal substitution is exactly divisibility by uw - vs.
```
theorem diagonal_eq_zero_iff (p : FormPair R) :
    diagonal p = 0 ↔ p = determinant p.2 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.mem_kernel_iff line 72
Source documentation
The kernel parametrization does not require any field or domain hypothesis.
```
theorem mem_kernel_iff (p : FormPair R) :
    p ∈ LinearMap.ker diagonal ↔ ∃ q, determinant q = p := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernel_eq_range line 81
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split line 86
Source documentation
A fixed linear complement to the determinant kernel on unrestricted polynomials.
```
def split : (R[X] × R[X]) ≃ₗ[R] FormPair R where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_apply line 98
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_symm_apply line 100
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_split line 102
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_zero_left line 105
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_surjective line 108
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelEquiv line 113
Source documentation
The kernel is canonically isomorphic to one polynomial copy.
```
def kernelEquiv : R[X] ≃ₗ[R] LinearMap.ker (diagonal (R := R)) where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply line 124
Source documentation
Multiply both coefficients by a first-input polynomial.
```
def multiply (f : R[X]) : FormPair R →ₗ[R] FormPair R where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_apply line 129
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_multiply line 133
Source documentation
The quotient action is ordinary polynomial multiplication.
```
theorem diagonal_multiply (f : R[X]) (p : FormPair R) :
    diagonal (multiply f p) = f * diagonal p := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_determinant line 139
Source documentation
The kernel action is ordinary polynomial multiplication with the same first input.
```
theorem multiply_determinant (f p : R[X]) :
    multiply f (determinant p) = determinant (f * p) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_mem_kernel line 145
Source documentation
Every first-input slice preserves the determinant kernel.
```
theorem multiply_mem_kernel (f : R[X]) {p : FormPair R}
    (hp : p ∈ LinearMap.ker diagonal) : multiply f p ∈ LinearMap.ker diagonal := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_multiply line 150
Source documentation
Quotient and kernel coordinates transform simultaneously, with an unchanged first input.
```
theorem split_multiply (f : R[X]) (p : R[X] × R[X]) :
    multiply f (split p) = split (f * p.1, f * p.2) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientMonomial line 156
Source documentation
The ordinary quotient monomial u^(e-j) v^j s, with j ≤ e.
```
def quotientMonomial (j : ℕ) : FormPair R := (X ^ j, 0)
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientTop line 159
Source documentation
The last quotient monomial v^e w.
```
def quotientTop (e : ℕ) : FormPair R := (0, X ^ e)
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelMonomial line 162
Source documentation
The kernel monomial (uw-vs) u^(e-1-j) v^j, with j < e.
```
def kernelMonomial (j : ℕ) : FormPair R := determinant (X ^ j)
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_quotientMonomial line 164
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_quotientTop line 168
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_kernelMonomial line 172
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientMonomial line 176
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_kernelMonomial line 180
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientTop_cross line 185
Source documentation
The sole cross term in a nonfinal first-input slice has coefficient one.
```
theorem multiply_quotientTop_cross (i e : ℕ) :
    multiply (X ^ i) (quotientTop (R := R) e) =
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientTop
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientTop_last line 193
Source documentation
For the final first-input monomial the last quotient vector remains the last vector.
```
theorem multiply_quotientTop_last (d e : ℕ) :
    multiply (X ^ d) (quotientTop (R := R) e) = quotientTop (d + e) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientTop
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector line 198
Source documentation
The actual quotient vectors used at degree e: there are e + 2 of them.
```
def quotientVector (e : ℕ) (j : Fin (e + 2)) : FormPair R :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelVector line 202
Source documentation
The actual kernel vectors used at degree e: there are e of them.
```
def kernelVector (_e : ℕ) (j : Fin _e) : FormPair R := kernelMonomial j
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelMonomial
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_quotientVector line 204
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_kernelVector line 212
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientVector_ordinary line 217
Source documentation
Ordinary quotient columns have no kernel correction in the adapted output basis.
```
theorem multiply_quotientVector_ordinary (d e i j : ℕ)
    (hi : i ≤ d) (hj : j ≤ e) :
    multiply (X ^ i) (quotientVector (R := R) e ⟨j, by omega⟩) =
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector, OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientVector_top_cross line 226
Source documentation
Nonfinal slices have exactly the quotient-top cross term described in Section 5.1.
```
theorem multiply_quotientVector_top_cross (d e i : ℕ) (hi : i < d) :
    multiply (X ^ i) (quotientVector (R := R) e ⟨e + 1, by omega⟩) =
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector, OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientVector_top_last line 236
Source documentation
The final slice has no cross term.
```
theorem multiply_quotientVector_top_last (d e : ℕ) :
    multiply (X ^ d) (quotientVector (R := R) e ⟨e + 1, by omega⟩) =
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector, OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_kernelVector line 243
Source documentation
All kernel columns have the convolution indices of the smaller branch.
```
theorem multiply_kernelVector (d e i j : ℕ) (hi : i ≤ d) (hj : j < e) :
    multiply (X ^ i) (kernelVector (R := R) e ⟨j, hj⟩) =
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelVector
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.monomials_linearIndependent line 251
Source documentation
Distinct bounded powers of X are independent even when the coefficient ring has zero divisors.
```
theorem monomials_linearIndependent (n : ℕ) :
    LinearIndependent R (fun i : Fin n => (X : R[X]) ^ (i : ℕ)) := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.adaptedVectors_linearIndependent line 261
Source documentation
The quotient vectors followed by the kernel vectors are linearly independent. This establishes nonsingularity of the simultaneous change of coordinates, without any genericity assumption on the first input.
```
theorem adaptedVectors_linearIndependent (e : ℕ) :
    LinearIndependent R (Sum.elim (quotientVector (R := R) e) (kernelVector e)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelVector