-- Evaluating a polynomial matrix commutes with its determinant (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Polynomial.Determinant
import Assignment
import Ring.DeterminantHom

section Evaluation
variable (I A add zero neg mul one v : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
hypothesis ring : IsCommRing(R)
hypothesis assignment : v : I → R

-- N may be any matrix whose entries are the evaluated entries of M.
theorem determinant.evaluate (n : Nat) (M N : Set)
  requires matrixM : RingMatrix(n, P, M)
  requires matrixN : RingMatrix(n, R, N)
  requires entries : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = polynomialAt(I, R, v)(M[i, j])
  shows polynomialAt(I, R, v)(determinant(n, P, M)) = determinant(n, R, N)
proof
  have polynomials := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have evaluation := polynomialAt.hom with *
  exact determinant.map with *

-- When no evaluated matrix is already in hand, the graph is supplied for free.
theorem determinant.evaluate_matrix (n : Nat) (M : Set)
  requires matrix : RingMatrix(n, P, M)
  shows polynomialAt(I, R, v)(determinant(n, P, M)) =
    determinant(n, R, matrixMap(n, P, R, polynomialAt(I, R, v), M))
proof
  have polynomials := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have evaluation := polynomialAt.hom with *
  exact determinant.map_matrix with *

end Evaluation