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.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair (R : Type u_2) [CommRing R] : Type u_2

Affine representatives of forms linear in the second pair of variables.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair R = (Polynomial R × Polynomial R)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal {R : Type u_1} [CommRing R] : FormPair R →ₗ[R] Polynomial R

Substitute the first variable pair into the second variable pair.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant {R : Type u_1} [CommRing R] : Polynomial R →ₗ[R] FormPair R

Multiplication by D = uw - vs after putting u = 1.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant = { toFun := fun (p : Polynomial R) => (-Polynomial.X * p, p), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_apply {R : Type u_1} [CommRing R] (p : FormPair R) : diagonal p = p.1 + Polynomial.X * p.2

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant_apply {R : Type u_1} [CommRing R] (p : Polynomial R) : determinant p = (-Polynomial.X * p, p)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_determinant {R : Type u_1} [CommRing R] (p : Polynomial R) : diagonal (determinant p) = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.determinant_injective {R : Type u_1} [CommRing R] : Function.Injective ⇑determinant

The determinant factor can be recovered from the second component.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_eq_zero_iff {R : Type u_1} [CommRing R] (p : FormPair R) : diagonal p = 0 ↔ p = determinant p.2

Vanishing after diagonal substitution is exactly divisibility by uw - vs.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.mem_kernel_iff {R : Type u_1} [CommRing R] (p : FormPair R) : p ∈ diagonal.ker ↔ ∃ (q : Polynomial R), determinant q = p

The kernel parametrization does not require any field or domain hypothesis.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernel_eq_range {R : Type u_1} [CommRing R] : diagonal.ker = determinant.range

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split {R : Type u_1} [CommRing R] : (Polynomial R × Polynomial R) ≃ₗ[R] FormPair R

A fixed linear complement to the determinant kernel on unrestricted polynomials.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_apply {R : Type u_1} [CommRing R] (p : Polynomial R × Polynomial R) : split p = (p.1 - Polynomial.X * p.2, p.2)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_symm_apply {R : Type u_1} [CommRing R] (p : FormPair R) : split.symm p = (diagonal p, p.2)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_split {R : Type u_1} [CommRing R] (p : Polynomial R × Polynomial R) : diagonal (split p) = p.1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_zero_left {R : Type u_1} [CommRing R] (q : Polynomial R) : split (0, q) = determinant q

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_surjective {R : Type u_1} [CommRing R] : Function.Surjective ⇑diagonal

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelEquiv {R : Type u_1} [CommRing R] : Polynomial R ≃ₗ[R] ↥diagonal.ker

The kernel is canonically isomorphic to one polynomial copy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply {R : Type u_1} [CommRing R] (f : Polynomial R) : FormPair R →ₗ[R] FormPair R

Multiply both coefficients by a first-input polynomial.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_apply {R : Type u_1} [CommRing R] (f : Polynomial R) (p : FormPair R) : (multiply f) p = (f * p.1, f * p.2)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_multiply {R : Type u_1} [CommRing R] (f : Polynomial R) (p : FormPair R) : diagonal ((multiply f) p) = f * diagonal p

The quotient action is ordinary polynomial multiplication.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_determinant {R : Type u_1} [CommRing R] (f p : Polynomial R) : (multiply f) (determinant p) = determinant (f * p)

The kernel action is ordinary polynomial multiplication with the same first input.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_mem_kernel {R : Type u_1} [CommRing R] (f : Polynomial R) {p : FormPair R} (hp : p ∈ diagonal.ker) : (multiply f) p ∈ diagonal.ker

Every first-input slice preserves the determinant kernel.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.split_multiply {R : Type u_1} [CommRing R] (f : Polynomial R) (p : Polynomial R × Polynomial R) : (multiply f) (split p) = split (f * p.1, f * p.2)

Quotient and kernel coordinates transform simultaneously, with an unchanged first input.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientMonomial {R : Type u_1} [CommRing R] (j : ℕ) : FormPair R

The ordinary quotient monomial u^(e-j) v^j s, with j ≤ e.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientMonomial j = (Polynomial.X ^ j, 0)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientTop {R : Type u_1} [CommRing R] (e : ℕ) : FormPair R

The last quotient monomial v^e w.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientTop e = (0, Polynomial.X ^ e)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelMonomial {R : Type u_1} [CommRing R] (j : ℕ) : FormPair R

The kernel monomial (uw-vs) u^(e-1-j) v^j, with j < e.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_quotientMonomial {R : Type u_1} [CommRing R] (j : ℕ) : diagonal (quotientMonomial j) = Polynomial.X ^ j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_quotientTop {R : Type u_1} [CommRing R] (e : ℕ) : diagonal (quotientTop e) = Polynomial.X ^ (e + 1)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_kernelMonomial {R : Type u_1} [CommRing R] (j : ℕ) : diagonal (kernelMonomial j) = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientMonomial {R : Type u_1} [CommRing R] (i j : ℕ) : (multiply (Polynomial.X ^ i)) (quotientMonomial j) = quotientMonomial (i + j)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_kernelMonomial {R : Type u_1} [CommRing R] (i j : ℕ) : (multiply (Polynomial.X ^ i)) (kernelMonomial j) = kernelMonomial (i + j)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientTop_cross {R : Type u_1} [CommRing R] (i e : ℕ) : (multiply (Polynomial.X ^ i)) (quotientTop e) = quotientMonomial (i + e + 1) + kernelMonomial (i + e)

The sole cross term in a nonfinal first-input slice has coefficient one.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientTop_last {R : Type u_1} [CommRing R] (d e : ℕ) : (multiply (Polynomial.X ^ d)) (quotientTop e) = quotientTop (d + e)

For the final first-input monomial the last quotient vector remains the last vector.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.quotientVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin (e + 2)) : FormPair R

The actual quotient vectors used at degree e: there are e + 2 of them.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.kernelVector {R : Type u_1} [CommRing R] (_e : ℕ) (j : Fin _e) : FormPair R

The actual kernel vectors used at degree e: there are e of them.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_quotientVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin (e + 2)) : diagonal (quotientVector e j) = Polynomial.X ^ ↑j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.diagonal_kernelVector {R : Type u_1} [CommRing R] (e : ℕ) (j : Fin e) : diagonal (kernelVector e j) = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientVector_ordinary {R : Type u_1} [CommRing R] (d e i j : ℕ) (hi : i ≤ d) (hj : j ≤ e) : (multiply (Polynomial.X ^ i)) (quotientVector e ⟨j, ⋯⟩) = quotientVector (d + e) ⟨i + j, ⋯⟩

Ordinary quotient columns have no kernel correction in the adapted output basis.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientVector_top_cross {R : Type u_1} [CommRing R] (d e i : ℕ) (hi : i < d) : (multiply (Polynomial.X ^ i)) (quotientVector e ⟨e + 1, ⋯⟩) = quotientVector (d + e) ⟨e + 1 + i, ⋯⟩ + kernelVector (d + e) ⟨e + i, ⋯⟩

Nonfinal slices have exactly the quotient-top cross term described in Section 5.1.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_quotientVector_top_last {R : Type u_1} [CommRing R] (d e : ℕ) : (multiply (Polynomial.X ^ d)) (quotientVector e ⟨e + 1, ⋯⟩) = quotientVector (d + e) ⟨d + e + 1, ⋯⟩

The final slice has no cross term.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply_kernelVector {R : Type u_1} [CommRing R] (d e i j : ℕ) (hi : i ≤ d) (hj : j < e) : (multiply (Polynomial.X ^ i)) (kernelVector e ⟨j, hj⟩) = kernelVector (d + e) ⟨i + j, ⋯⟩

All kernel columns have the convolution indices of the smaller branch.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.monomials_linearIndependent {R : Type u_1} [CommRing R] (n : ℕ) : LinearIndependent R fun (i : Fin n) => Polynomial.X ^ ↑i

Distinct bounded powers of X are independent even when the coefficient ring has zero divisors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.adaptedVectors_linearIndependent {R : Type u_1} [CommRing R] (e : ℕ) : LinearIndependent R (Sum.elim (quotientVector e) (kernelVector e))

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.