Grace/Cumulus/Algebra/Polynomial/AffineDeterminant.g17

Imports

Declarations

determinant.affine_horner theorem derivation
Source

1-- The determinant of an affine polynomial matrix has a tracked Horner form (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.AffineDeterminant8import HornerForms910section Rings11variable (I A add zero neg mul one j : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring P := R[I]14hypothesis ring : IsCommRing(R)1516-- det(B+XD) has a length-n Horner representation with terminal coefficient det(D).17theorem determinant.affine_horner (n : Nat) (M B D : Set)18  requires matrixM : RingMatrix(n, P, M)19  requires matrixB : RingMatrix(n, R, B)20  requires matrixD : RingMatrix(n, R, D)21  requires entries : ∀ r ∈ n, ∀ c ∈ n, M[r, c] = P[polynomialCoefficients(I, R)(B[r, c]) + polynomialCoefficients(I, R)(D[r, c]) * polynomialVariable(I, R, j)]22  shows HornerForm(I, R, j, determinant(n, P, M), n, determinant(n, R, D))23proof24  have finite := Finite.natural at n with *25  have permutationsFinite := permutations.finite with finite26  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *27  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *28  have size := cardinality.natural at n with *29  have polynomialTerms := determinantTerms.function at n, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], M with *30  have coefficientTerms := determinantTerms.function at n, A, add, zero, neg, mul, one, D with *31  have forms : ∀ p ∈ permutations(n), HornerForm(I, R, j, determinantTerms(n, P, M)(p), n, determinantTerms(n, R, D)(p))32    intros p hp33    have permutation := permutations.mem_iff.forward with hp34    have injective := Bijective.injective with permutation35    have function := Injective.function with injective36    have polynomialEntries := permutationEntries.function at n, P, M, p with *37    have constantEntries := permutationEntries.function at n, A, B, p with *38    have slopeEntries := permutationEntries.function at n, A, D, p with *39    have affine : ∀ r ∈ n, permutationEntries(n, P, M, p)(r) = P[polynomialCoefficients(I, R)(permutationEntries(n, R, B, p)(r)) + polynomialCoefficients(I, R)(permutationEntries(n, R, D, p)(r)) * polynomialVariable(I, R, j)]40      intros r hr41      have column := FunctionBetween.apply_closed at p, n, n, r with *42      have left := permutationEntries.value at n, P, M, p, r with *43      have constant := permutationEntries.value at n, A, B, p, r with *44      have slope := permutationEntries.value at n, A, D, p, r with *45      have equation := entries with r, hr, p(r), column46      cc47    have product := HornerForm.finite_affine_product at I, A, add, zero, neg, mul, one, j, n, permutationEntries(n, P, M, p), permutationEntries(n, R, B, p), permutationEntries(n, R, D, p) with *48    rw size at product49    have mappedSign := permutationSign.map at A, add, zero, neg, mul, one, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], polynomialCoefficients(I, R), n, p with *50    have scaled := HornerForm.scale at I, A, add, zero, neg, mul, one, j, finiteRingProduct(n, P, permutationEntries(n, P, M, p)), n, permutationSign(n, R, p), finiteRingProduct(n, R, permutationEntries(n, R, D, p)) with *51    have polynomialTerm := determinantTerms.value at n, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], M, p with *52    have coefficientTerm := determinantTerms.value at n, A, add, zero, neg, mul, one, D, p with *53    rwa [polynomialTerm, coefficientTerm, ← mappedSign]54  have result := HornerForm.finite_sum at I, A, add, zero, neg, mul, one, j, n, permutations(n), determinantTerms(n, P, M), determinantTerms(n, R, D) with *55  unfold determinant56  exact result5758end Rings59