-- Characteristic polynomials and evaluation into coefficient extensions (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.Characteristic
import Ring.CharacteristicMatrix
import EvaluationOver

def characteristicPolynomial (n I A add zero neg mul one M j : Set) : Set :=
  determinant(n, polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one), characteristicMatrix(n, polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one), matrixMap(n, A, polynomials(I, A, zero), polynomialCoefficients(I, A, zero), M), polynomialVariable(I, A, zero, one, j)))

notation scoped characteristicPolynomial(n, I, R, M, j) => characteristicPolynomial(n, I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, j)

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

theorem characteristicPolynomial.member (n : Nat) (M j : Set)
  requires matrix : RingMatrix(n, R, M)
  requires index : j ∈ I
  shows characteristicPolynomial(n, I, R, M, j) ∈ P
proof
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have constants := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *
  have function := IsRingHom.function with constants
  have embedded := matrixMap.matrix with *
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have variableIn := polynomialVariable.member at I, A, zero, one, j with *
  have characteristic : RingMatrix(n, P, characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j)))
    exact characteristicMatrix.matrix with *
  unfold characteristicPolynomial
  exact determinant.closed with *

end Polynomials

section Evaluation
variable (I A add zero neg mul one B plus z minus times unit f v : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring P := R[I]
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis assignment : v : I → S

theorem characteristicPolynomial.evaluate_over (n : Nat) (M N j : Set)
  requires matrixM : RingMatrix(n, R, M)
  requires matrixN : RingMatrix(n, S, N)
  requires index : j ∈ I
  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])
  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) =
    determinant(n, S, characteristicMatrix(n, S, N, v(j)))
proof
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have constants := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *
  have function := IsRingHom.function with constants
  have embedded := matrixMap.matrix with function
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have variableIn := polynomialVariable.member at I, A, zero, one, j with *
  have evaluation := polynomialAtOver.hom at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v with *
  have variableValue := polynomialAtOver.variable at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v, j with *
  have mapped : ∀ a ∈ n, ∀ b ∈ n,
    N[a, b] = polynomialAtOver(I, R, S, f, v)(matrixMap(n, R, P, polynomialCoefficients(I, R), M)[a, b])
    intros a ha b hb
    have coefficient := RingMatrix.entry at n, A, M, a, b with *
    have embeddedEntry := matrixMap.entry at n, A, P, polynomialCoefficients(I, R), M, a, b with *
    have constantValue := polynomialCoefficients.value at I, A, zero, M[a, b] with *
    have evaluated := polynomialAtOver.constant at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v, M[a, b] with *
    have entry := entries with a, ha, b, hb
    cc
  have transported : polynomialAtOver(I, R, S, f, v)(determinant(n, P, characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j)))) =
    determinant(n, S, characteristicMatrix(n, S, N, polynomialAtOver(I, R, S, f, v)(polynomialVariable(I, R, j))))
    exact determinant.characteristic_map with *
  unfold characteristicPolynomial
  cc

theorem characteristicPolynomial.annihilates (n : Nat) (M N j w k : Set)
  requires matrixM : RingMatrix(n, R, M)
  requires matrixN : RingMatrix(n, S, N)
  requires index : j ∈ I
  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])
  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)
  requires coordinate : k ∈ n
  shows S[polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) * w(k)] = S[0]
proof
  have scalar := FunctionBetween.apply_closed with *
  have evaluated := characteristicPolynomial.evaluate_over with *
  have annihilated := characteristicMatrix.annihilates with *
  cc


-- The mapped-matrix form constructs the coefficient extension automatically.
theorem characteristicPolynomial.evaluate_mapped (n : Nat) (M j : Set)
  requires matrix : RingMatrix(n, R, M)
  requires index : j ∈ I
  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) =
    determinant(n, S, characteristicMatrix(n, S, matrixMap(n, R, S, f, M), v(j)))
proof
  have function := IsRingHom.function with hom
  have mapped := matrixMap.matrix with *
  have entries : ∀ a ∈ n, ∀ b ∈ n, matrixMap(n, R, S, f, M)[a, b] = f(M[a, b])
    intros a ha b hb
    exact matrixMap.entry with *
  exact characteristicPolynomial.evaluate_over with *

-- Nonzero eigenvectors yield roots only when zero divisors are excluded.
theorem characteristicPolynomial.root (n : Nat) (M N j w k : Set)
  requires domain : IsIntegralDomain(S)
  requires matrixM : RingMatrix(n, R, M)
  requires matrixN : RingMatrix(n, S, N)
  requires index : j ∈ I
  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])
  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)
  requires coordinate : k ∈ n
  requires nonzero : w(k) ≠ S[0]
  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) = S[0]
proof
  have scalar := FunctionBetween.apply_closed with *
  have characteristic := characteristicMatrix.matrix at n, B, plus, z, minus, times, unit, N, v(j) with *
  have kernel := characteristicMatrix.left_kernel with *
  have vanishes := determinant.zero_of_nonzero_left_kernel with *
  have evaluated := characteristicPolynomial.evaluate_over with *
  cc

end Evaluation