CharacteristicMonic

Characteristic monicity and a common monic eigenvector annihilator in ZF

Open in Workbench View on GitHub

1-- Characteristic monicity and a common monic eigenvector annihilator in ZF.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module CharacteristicMonicExample7import Grace.Cumulus.Algebra.Polynomial.CharacteristicMonic89section Polynomials10variable (I A add zero neg mul one j : Set)11notation ring R := (A, add, zero, neg, mul, one)12notation ring P := R[I]13hypothesis ring : IsCommRing(R)14hypothesis index : j ∈ I1516theorem affine_determinant (n : Nat) (M B D : Set)17  requires matrixM : RingMatrix(n, P, M)18  requires matrixB : RingMatrix(n, R, B)19  requires matrixD : RingMatrix(n, R, D)20  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)]21  shows HornerForm(I, R, j, determinant(n, P, M), n, determinant(n, R, D))22proof23  exact determinant.affine_horner with *2425theorem monic (n : Nat) (M : Set)26  requires matrix : RingMatrix(n, R, M)27  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ characteristicPolynomial(n, I, R, M, j) = polynomialFromHorner(I, R, j, R[1], cs)28proof29  exact characteristicPolynomial.monic with *3031theorem add_forms (p q n a b : Set)32  requires first : HornerForm(I, R, j, p, n, a)33  requires second : HornerForm(I, R, j, q, n, b)34  shows HornerForm(I, R, j, P[p + q], n, R[a + b])35proof36  exact HornerForm.add with *3738end Polynomials3940section Extensions41variable (A add zero neg mul one B plus z minus times unit f : Set)42notation ring R := (A, add, zero, neg, mul, one)43notation ring S := (B, plus, z, minus, times, unit)44hypothesis source : IsCommRing(R)45hypothesis target : IsCommRing(S)46hypothesis hom : IsRingHom(f, R, S)4748theorem common_annihilator (n : Nat) (M N x w : Set)49  requires matrixM : RingMatrix(n, R, M)50  requires matrixN : RingMatrix(n, S, N)51  requires entries : ∀ r ∈ n, ∀ c ∈ n, N[r, c] = f(M[r, c])52  requires element : x ∈ S53  requires eigenvector : LeftEigenvector(n, S, N, x, w)54  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ (∀ k ∈ n, S[monicValue(R, f, S, x, cs) * w(k)] = S[0])55proof56  exact LeftEigenvector.monic_annihilator with *5758end Extensions59