Grace/Cumulus/Algebra/Polynomial/Determinant.g17

Open in Workbench Download source

Imports

Assignment · Ring.DeterminantHom

Declarations

• determinant.evaluate theorem derivation
• determinant.evaluate_matrix theorem derivation

Source

1-- Evaluating a polynomial matrix commutes with its determinant (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.Determinant8import Assignment9import Ring.DeterminantHom1011section Evaluation12variable (I A add zero neg mul one v : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring P := R[I]15hypothesis ring : IsCommRing(R)16hypothesis assignment : v : I → R1718-- N may be any matrix whose entries are the evaluated entries of M.19theorem determinant.evaluate (n : Nat) (M N : Set)20  requires matrixM : RingMatrix(n, P, M)21  requires matrixN : RingMatrix(n, R, N)22  requires entries : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = polynomialAt(I, R, v)(M[i, j])23  shows polynomialAt(I, R, v)(determinant(n, P, M)) = determinant(n, R, N)24proof25  have polynomials := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *26  have evaluation := polynomialAt.hom with *27  exact determinant.map with *2829-- When no evaluated matrix is already in hand, the graph is supplied for free.30theorem determinant.evaluate_matrix (n : Nat) (M : Set)31  requires matrix : RingMatrix(n, P, M)32  shows polynomialAt(I, R, v)(determinant(n, P, M)) =33    determinant(n, R, matrixMap(n, P, R, polynomialAt(I, R, v), M))34proof35  have polynomials := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *36  have evaluation := polynomialAt.hom with *37  exact determinant.map_matrix with *3839end Evaluation40