The finite determinant filtration of polynomial multiplication

The first leg is kept fixed throughout. The second and third legs use the explicit quotient/kernel vectors of DeterminantKernel. The coefficient identity adaptedTensor_reconstruct verifies the actual multiplication on every basis input; it does not assume a simultaneous triangularization.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index (e : ℕ) : Type

Indices for the quotient and kernel parts of a determinant filtration.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index e = (Fin (e + 2) ⊕ Fin e)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.vector (K : Type) [Field K] (e : ℕ) : Index e → DeterminantKernel.FormPair K

The ordered quotient/kernel vectors in the actual polynomial pair space.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor (K : Type) [Field K] (d e : ℕ) : Foundation.Tensor K (Fin (d + 1)) (Index e) (Index (d + e))

All multiplication coefficients in the explicit adapted bases. Here a=d+1, b=e+1, and no first-leg change of coordinates occurs.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor K d e x✝ (Sum.inl j) (Sum.inl k) = if ↑x✝ + ↑j = ↑k then 1 else 0
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor K d e x✝ (Sum.inr val) (Sum.inl val_1) = 0
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor K d e x✝ (Sum.inr j) (Sum.inr k) = if ↑x✝ + ↑j = ↑k then 1 else 0

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor (K : Type) [Field K] (d e : ℕ) : Foundation.Tensor K (Fin (d + 1)) (Index e) (Index (d + e))

The associated graded tensor, whose two branches still share the first leg.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor K d e x✝ (Sum.inl j) (Sum.inl k) = if ↑x✝ + ↑j = ↑k then 1 else 0
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor K d e x✝ (Sum.inl j) (Sum.inr k) = 0
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor K d e x✝ (Sum.inr val) (Sum.inl val_1) = 0
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor K d e x✝ (Sum.inr j) (Sum.inr k) = if ↑x✝ + ↑j = ↑k then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor_reconstruct {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Index e) : ∑ k : Index (d + e), adaptedTensor K d e i j k • vector K (d + e) k = (DeterminantKernel.multiply (Polynomial.X ^ ↑i)) (vector K e j)

Exact coordinate reconstruction of every first-leg slice, in common bases.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor_unique {K : Type} [Field K] (d e : ℕ) (T : Foundation.Tensor K (Fin (d + 1)) (Index e) (Index (d + e))) (hT : ∀ (i : Fin (d + 1)) (j : Index e), ∑ k : Index (d + e), T i j k • vector K (d + e) k = (DeterminantKernel.multiply (Polynomial.X ^ ↑i)) (vector K e j)) : T = adaptedTensor K d e

The reconstruction uniquely determines every tensor coefficient.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor_quotient {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin (e + 2)) (k : Fin (d + e + 2)) : gradedTensor K d e i (Sum.inl j) (Sum.inl k) = convolution K (d + 1) (e + 2) i j (Fin.cast ⋯ k)

The quotient branch is exactly C(a,b+1).

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor_kernel {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin e) (k : Fin (d + e)) : gradedTensor K d e i (Sum.inr j) (Sum.inr k) = convolution K (d + 1) e i j (Fin.cast ⋯ k)

The kernel branch is exactly C(a,b-1).

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor_kernel_to_quotient {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin e) (k : Fin (d + e + 2)) : adaptedTensor K d e i (Sum.inr j) (Sum.inl k) = 0

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputScale (K : Type) [Field K] (e : ℕ) : Index e → Polynomial K

Polynomial diagonal maps; scaling the quotient input by X clears the negative input-kernel weight without changing the leading tensor.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputScale K e (Sum.inl val) = Polynomial.X
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputScale K e (Sum.inr val) = 1

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputScale (K : Type) [Field K] (e : ℕ) : Index e → Polynomial K

Scale quotient coordinates by one and kernel coordinates by the polynomial variable.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputScale K e (Sum.inl val) = 1
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputScale K e (Sum.inr val) = Polynomial.X

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.diagonalMap {K : Type} [Field K] {I : Type u_1} [DecidableEq I] (s : I → Polynomial K) : I → I → Polynomial K

The diagonal coordinate map with prescribed polynomial scaling factors.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.diagonalMap s i j = if i = j then s i else 0

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.degeneration (K : Type) [Field K] (d e : ℕ) : (adaptedTensor K d e).PolynomialRestrictionDegeneration (gradedTensor K d e) 1 0 1 1

A checked polynomial degeneration to the two matched convolution branches.

Equations

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

The actual coordinate change from the original two-copy convolution.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex (e : ℕ) : Type

Indices for the two original monomial bases before the filtration change of basis.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex e = (Fin (e + 1) ⊕ Fin (e + 1))

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalBasis (K : Type) [Field K] (e : ℕ) : Module.Basis (OriginalIndex e) K (DeterminantBasis.BoundedPair K e)

The original monomial bases in the s and w components.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalBasis K e = (Polynomial.degreeLT.basis K (e + 1)).prod (Polynomial.degreeLT.basis K (e + 1))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.degree_shift_lt {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (p : ↥(Polynomial.degreeLT K (e + 1))) : (Polynomial.X ^ ↑i * ↑p).degree < ↑(d + e + 1)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.boundedShift (K : Type) [Field K] (d e : ℕ) (i : Fin (d + 1)) : ↥(Polynomial.degreeLT K (e + 1)) →ₗ[K] ↥(Polynomial.degreeLT K (d + e + 1))

Multiplication by a fixed first-input monomial between the bounded spaces.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.boundedMultiply (K : Type) [Field K] (d e : ℕ) (i : Fin (d + 1)) : DeterminantBasis.BoundedPair K e →ₗ[K] DeterminantBasis.BoundedPair K (d + e)

The same first monomial multiplies both components.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.forget_boundedMultiply {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (p : DeterminantBasis.BoundedPair K e) : (DeterminantBasis.forget (d + e)) ((boundedMultiply K d e i) p) = (DeterminantKernel.multiply (Polynomial.X ^ ↑i)) ((DeterminantBasis.forget e) p)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor (K : Type) [Field K] (d e : ℕ) : Foundation.Tensor K (Fin (d + 1)) (OriginalIndex e) (OriginalIndex (d + e))

Polynomial multiplication in its original monomial coordinates.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inl_inl {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin (e + 1)) (k : Fin (d + e + 1)) : sourceTensor K d e i (Sum.inl j) (Sum.inl k) = convolution K (d + 1) (e + 1) i j (Fin.cast ⋯ k)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inr_inr {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin (e + 1)) (k : Fin (d + e + 1)) : sourceTensor K d e i (Sum.inr j) (Sum.inr k) = convolution K (d + 1) (e + 1) i j (Fin.cast ⋯ k)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inl_inr {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin (e + 1)) (k : Fin (d + e + 1)) : sourceTensor K d e i (Sum.inl j) (Sum.inr k) = 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inr_inl {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Fin (e + 1)) (k : Fin (d + e + 1)) : sourceTensor K d e i (Sum.inr j) (Sum.inl k) = 0

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalCoordinate (e : ℕ) : OriginalIndex e → Fin (e + 1) × Bool

Record the polynomial coordinate and the choice of s or w separately.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalCoordinate e (Sum.inl j) = (j, false)
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalCoordinate e (Sum.inr j) = (j, true)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_product {K : Type} [Field K] (d e : ℕ) : sourceTensor K d e = Foundation.Tensor.pullback (fun (i : Fin (d + 1)) => (i, ())) (originalCoordinate e) (fun (k : OriginalIndex (d + e)) => (Fin.cast ⋯ (originalCoordinate (d + e) k).1, (originalCoordinate (d + e) k).2)) ((convolution K (d + 1) (e + 1)).product (Foundation.Tensor.dotPairing Bool).cyclic.cyclic)

The source is exactly polynomial convolution tensored with a two-coordinate dot product whose singleton is on the unchanged first leg.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputChange (K : Type) [Field K] (e : ℕ) (j : Index e) (old : OriginalIndex e) : K

The input matrix has adapted vectors as columns in the original basis.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputDualChange (K : Type) [Field K] (e : ℕ) (k : Index e) (old : OriginalIndex e) : K

The output-dual matrix uses the inverse basis change, as required for tensors.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.fixedFirst (K : Type) [Field K] (d : ℕ) (i j : Fin (d + 1)) : K

The first input is unchanged, including throughout the basis change.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.fixedFirst K d i j = if i = j then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.boundedMultiply_adapted_coordinates {K : Type} [Field K] (d e : ℕ) (i : Fin (d + 1)) (j : Index e) (k : Index (d + e)) : ((DeterminantBasis.basis K (d + e)).repr ((boundedMultiply K d e i) ((DeterminantBasis.basis K e) j))) k = adaptedTensor K d e i j k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_coordinate_change {K : Type} [Field K] (d e : ℕ) : Foundation.Tensor.restrict (fixedFirst K d) (inputChange K e) (outputDualChange K (d + e)) (sourceTensor K d e) = adaptedTensor K d e

A concrete restriction, with the identity first map, changes the original two-copy convolution into the simultaneously triangular coefficient tensor.