-- Constructive monicity of characteristic polynomials over commutative rings (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.CharacteristicMonic
import AffineDeterminant
import Ring.DeterminantIdentity

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

theorem characteristicPolynomial.horner_form (n : Nat) (M : Set)
  requires matrix : RingMatrix(n, R, M)
  shows HornerForm(I, R, j, characteristicPolynomial(n, I, R, M, j), n, R[1])
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have oneIn : R[1] ∈ R by typecheck
  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have targetRing := IsCommRing.ring with target
  have zeroPoly := IsRing.zero_in_carrier with targetRing
  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *
  have function := IsRingHom.function with hom
  have mapsZero := IsRingHom.zero with hom
  have mapsOne := IsRingHom.one with hom
  have variableIn := polynomialVariable.member at I, A, zero, one, j with *
  have embedded := matrixMap.matrix at n, A, P, polynomialCoefficients(I, R), M 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 *
  have constants := characteristicMatrix.matrix at n, A, add, zero, neg, mul, one, M, zero with *
  have slopes := identityMatrix.matrix at A, add, zero, neg, mul, one, n with *
  have affine : ∀ r ∈ n, ∀ c ∈ n, characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j))[r, c] =
    P[polynomialCoefficients(I, R)(characteristicMatrix(n, R, M, zero)[r, c]) + polynomialCoefficients(I, R)(identityMatrix(n, R)[r, c]) * polynomialVariable(I, R, j)]
    intros r hr c hc
    have entryIn := RingMatrix.entry at n, A, M, r, c with *
    have image := IsRingHom.closed with hom, entryIn
    have embeddedEntry := matrixMap.entry at n, A, P, polynomialCoefficients(I, R), M, r, c with *
    have characteristicEntry : characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j))[r, c] =
      P[singleValue(P, P[0], polynomialVariable(I, R, j), c, r) - matrixMap(n, R, P, polynomialCoefficients(I, R), M)[r, c]]
      exact characteristicMatrix.entry with *
    have constantEntry := characteristicMatrix.entry at n, A, add, zero, neg, mul, one, M, zero, r, c with *
    have zeroDelta := singleValue.zero at A, zero, c, r with *
    have constant : characteristicMatrix(n, R, M, zero)[r, c] = R[-M[r, c]]
      rw [constantEntry, zeroDelta]
      ring
    have slopeEntry := identityMatrix.entry at A, add, zero, neg, mul, one, n, r, c with *
    have negative := IsRingHom.neg with hom, entryIn
    have deltaIn := singleValue.closed at P, P[0], polynomialVariable(I, R, j), c, r with *
    have deltaMap : P[polynomialCoefficients(I, R)(singleValue(A, zero, one, c, r)) * polynomialVariable(I, R, j)] = singleValue(P, P[0], polynomialVariable(I, R, j), c, r)
      have alternatives : r = c ∨ r ≠ c by tauto
      cases alternatives with same | different
      . have scalarDelta := singleValue.same at A, zero, one, c, r with *
        have variableDelta := singleValue.same at P, P[0], polynomialVariable(I, R, j), c, r with *
        rw [scalarDelta, variableDelta, mapsOne]
        ring
      . have scalarDelta := singleValue.other at A, zero, one, c, r with *
        have variableDelta := singleValue.other at P, P[0], polynomialVariable(I, R, j), c, r with *
        rw [scalarDelta, variableDelta, mapsZero]
        ring
    rw [characteristicEntry, embeddedEntry, constant, slopeEntry, negative, deltaMap]
    ring
  have form : HornerForm(I, R, j, determinant(n, P, characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j))), n, determinant(n, R, identityMatrix(n, R)))
    exact determinant.affine_horner with *
  have leading := determinant.identity at A, add, zero, neg, mul, one, n with *
  rw leading at form
  unfold characteristicPolynomial
  exact form

theorem characteristicPolynomial.monic (n : Nat) (M : Set)
  requires matrix : RingMatrix(n, R, M)
  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ characteristicPolynomial(n, I, R, M, j) = polynomialFromHorner(I, R, j, R[1], cs)
proof
  have form := characteristicPolynomial.horner_form with *
  exact form.right

end Rings
section Extensions
variable (A add zero neg mul one B plus z minus times unit f : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)

-- The same monic coefficient list annihilates every coordinate of the vector.
theorem LeftEigenvector.monic_annihilator (n : Nat) (M N x w : Set)
  requires matrixM : RingMatrix(n, R, M)
  requires matrixN : RingMatrix(n, S, N)
  requires entries : ∀ r ∈ n, ∀ c ∈ n, N[r, c] = f(M[r, c])
  requires element : x ∈ S
  requires eigenvector : LeftEigenvector(n, S, N, x, w)
  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ (∀ k ∈ n, S[monicValue(R, f, S, x, cs) * w(k)] = S[0])
proof
  have index : ∅ ∈ {∅} by simp [singleton.membership]
  have assignment := constantFunction.function at {∅}, B, x with *
  have point := constantFunction.apply at {∅}, B, ∅, x with *
  obtain ⟨cs, coefficients, size, representation⟩ := characteristicPolynomial.monic at {∅}, A, add, zero, neg, mul, one, ∅, n, M with *
  have evaluatedEigenvector : LeftEigenvector(n, S, N, constantFunction({∅}, B, x)(∅), w) by rwa point
  refine ⟨cs, coefficients, size, ?_⟩
  intros k hk
  have annihilates := characteristicPolynomial.horner_annihilates with *
  rwa point at annihilates

end Extensions