Grace/Cumulus/Algebra/Polynomial/CharacteristicMonic.g17

Open in Workbench Download source

Imports

AffineDeterminant · Ring.DeterminantIdentity

Declarations

Source

1-- Constructive monicity of characteristic polynomials over commutative rings (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.CharacteristicMonic8import AffineDeterminant9import Ring.DeterminantIdentity1011section Rings12variable (I A add zero neg mul one j : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring P := R[I]15hypothesis ring : IsCommRing(R)16hypothesis index : j ∈ I1718theorem characteristicPolynomial.horner_form (n : Nat) (M : Set)19  requires matrix : RingMatrix(n, R, M)20  shows HornerForm(I, R, j, characteristicPolynomial(n, I, R, M, j), n, R[1])21proof22  have ordinary := IsCommRing.ring with ring23  have zeroIn := IsRing.zero_in_carrier with ordinary24  have oneIn : R[1] ∈ R by typecheck25  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *26  have targetRing := IsCommRing.ring with target27  have zeroPoly := IsRing.zero_in_carrier with targetRing28  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *29  have function := IsRingHom.function with hom30  have mapsZero := IsRingHom.zero with hom31  have mapsOne := IsRingHom.one with hom32  have variableIn := polynomialVariable.member at I, A, zero, one, j with *33  have embedded := matrixMap.matrix at n, A, P, polynomialCoefficients(I, R), M with *34  have characteristic : RingMatrix(n, P, characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j)))35    exact characteristicMatrix.matrix with *36  have constants := characteristicMatrix.matrix at n, A, add, zero, neg, mul, one, M, zero with *37  have slopes := identityMatrix.matrix at A, add, zero, neg, mul, one, n with *38  have affine : ∀ r ∈ n, ∀ c ∈ n, characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j))[r, c] =39    P[polynomialCoefficients(I, R)(characteristicMatrix(n, R, M, zero)[r, c]) + polynomialCoefficients(I, R)(identityMatrix(n, R)[r, c]) * polynomialVariable(I, R, j)]40    intros r hr c hc41    have entryIn := RingMatrix.entry at n, A, M, r, c with *42    have image := IsRingHom.closed with hom, entryIn43    have embeddedEntry := matrixMap.entry at n, A, P, polynomialCoefficients(I, R), M, r, c with *44    have characteristicEntry : characteristicMatrix(n, P, matrixMap(n, R, P, polynomialCoefficients(I, R), M), polynomialVariable(I, R, j))[r, c] =45      P[singleValue(P, P[0], polynomialVariable(I, R, j), c, r) - matrixMap(n, R, P, polynomialCoefficients(I, R), M)[r, c]]46      exact characteristicMatrix.entry with *47    have constantEntry := characteristicMatrix.entry at n, A, add, zero, neg, mul, one, M, zero, r, c with *48    have zeroDelta := singleValue.zero at A, zero, c, r with *49    have constant : characteristicMatrix(n, R, M, zero)[r, c] = R[-M[r, c]]50      rw [constantEntry, zeroDelta]51      ring52    have slopeEntry := identityMatrix.entry at A, add, zero, neg, mul, one, n, r, c with *53    have negative := IsRingHom.neg with hom, entryIn54    have deltaIn := singleValue.closed at P, P[0], polynomialVariable(I, R, j), c, r with *55    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)56      have alternatives : r = c ∨ r ≠ c by tauto57      cases alternatives with same | different58      . have scalarDelta := singleValue.same at A, zero, one, c, r with *59        have variableDelta := singleValue.same at P, P[0], polynomialVariable(I, R, j), c, r with *60        rw [scalarDelta, variableDelta, mapsOne]61        ring62      . have scalarDelta := singleValue.other at A, zero, one, c, r with *63        have variableDelta := singleValue.other at P, P[0], polynomialVariable(I, R, j), c, r with *64        rw [scalarDelta, variableDelta, mapsZero]65        ring66    rw [characteristicEntry, embeddedEntry, constant, slopeEntry, negative, deltaMap]67    ring68  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)))69    exact determinant.affine_horner with *70  have leading := determinant.identity at A, add, zero, neg, mul, one, n with *71  rw leading at form72  unfold characteristicPolynomial73  exact form7475theorem characteristicPolynomial.monic (n : Nat) (M : Set)76  requires matrix : RingMatrix(n, R, M)77  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ characteristicPolynomial(n, I, R, M, j) = polynomialFromHorner(I, R, j, R[1], cs)78proof79  have form := characteristicPolynomial.horner_form with *80  exact form.right8182end Rings83section Extensions84variable (A add zero neg mul one B plus z minus times unit f : Set)85notation ring R := (A, add, zero, neg, mul, one)86notation ring S := (B, plus, z, minus, times, unit)87hypothesis source : IsCommRing(R)88hypothesis target : IsCommRing(S)89hypothesis hom : IsRingHom(f, R, S)9091-- The same monic coefficient list annihilates every coordinate of the vector.92theorem LeftEigenvector.monic_annihilator (n : Nat) (M N x w : Set)93  requires matrixM : RingMatrix(n, R, M)94  requires matrixN : RingMatrix(n, S, N)95  requires entries : ∀ r ∈ n, ∀ c ∈ n, N[r, c] = f(M[r, c])96  requires element : x ∈ S97  requires eigenvector : LeftEigenvector(n, S, N, x, w)98  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ (∀ k ∈ n, S[monicValue(R, f, S, x, cs) * w(k)] = S[0])99proof100  have index : ∅ ∈ {∅} by simp [singleton.membership]101  have assignment := constantFunction.function at {∅}, B, x with *102  have point := constantFunction.apply at {∅}, B, ∅, x with *103  obtain ⟨cs, coefficients, size, representation⟩ := characteristicPolynomial.monic at {∅}, A, add, zero, neg, mul, one, ∅, n, M with *104  have evaluatedEigenvector : LeftEigenvector(n, S, N, constantFunction({∅}, B, x)(∅), w) by rwa point105  refine ⟨cs, coefficients, size, ?_⟩106  intros k hk107  have annihilates := characteristicPolynomial.horner_annihilates with *108  rwa point at annihilates109110end Extensions111