Grace/Cumulus/Algebra/Polynomial/Characteristic.g17

Open in Workbench Download source

Imports

Ring.CharacteristicMatrix · EvaluationOver

Declarations

Source

1-- Characteristic polynomials and evaluation into coefficient extensions (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.Characteristic8import Ring.CharacteristicMatrix9import EvaluationOver1011def characteristicPolynomial (n I A add zero neg mul one M j : Set) : Set :=12  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)))1314notation scoped characteristicPolynomial(n, I, R, M, j) => characteristicPolynomial(n, I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, j)1516section Polynomials17variable (I A add zero neg mul one : Set)18notation ring R := (A, add, zero, neg, mul, one)19notation ring P := R[I]20hypothesis ring : IsCommRing(R)2122theorem characteristicPolynomial.member (n : Nat) (M j : Set)23  requires matrix : RingMatrix(n, R, M)24  requires index : j ∈ I25  shows characteristicPolynomial(n, I, R, M, j) ∈ P26proof27  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *28  have constants := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *29  have function := IsRingHom.function with constants30  have embedded := matrixMap.matrix with *31  have zeroIn : R[0] ∈ R by typecheck32  have oneIn : R[1] ∈ R by typecheck33  have variableIn := polynomialVariable.member at I, A, zero, one, j 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  unfold characteristicPolynomial37  exact determinant.closed with *3839end Polynomials4041section Evaluation42variable (I A add zero neg mul one B plus z minus times unit f v : Set)43notation ring R := (A, add, zero, neg, mul, one)44notation ring S := (B, plus, z, minus, times, unit)45notation ring P := R[I]46hypothesis source : IsCommRing(R)47hypothesis target : IsCommRing(S)48hypothesis hom : IsRingHom(f, R, S)49hypothesis assignment : v : I → S5051theorem characteristicPolynomial.evaluate_over (n : Nat) (M N j : Set)52  requires matrixM : RingMatrix(n, R, M)53  requires matrixN : RingMatrix(n, S, N)54  requires index : j ∈ I55  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])56  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) =57    determinant(n, S, characteristicMatrix(n, S, N, v(j)))58proof59  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *60  have constants := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *61  have function := IsRingHom.function with constants62  have embedded := matrixMap.matrix with function63  have zeroIn : R[0] ∈ R by typecheck64  have oneIn : R[1] ∈ R by typecheck65  have variableIn := polynomialVariable.member at I, A, zero, one, j with *66  have evaluation := polynomialAtOver.hom at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v with *67  have variableValue := polynomialAtOver.variable at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v, j with *68  have mapped : ∀ a ∈ n, ∀ b ∈ n,69    N[a, b] = polynomialAtOver(I, R, S, f, v)(matrixMap(n, R, P, polynomialCoefficients(I, R), M)[a, b])70    intros a ha b hb71    have coefficient := RingMatrix.entry at n, A, M, a, b with *72    have embeddedEntry := matrixMap.entry at n, A, P, polynomialCoefficients(I, R), M, a, b with *73    have constantValue := polynomialCoefficients.value at I, A, zero, M[a, b] with *74    have evaluated := polynomialAtOver.constant at I, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v, M[a, b] with *75    have entry := entries with a, ha, b, hb76    cc77  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)))) =78    determinant(n, S, characteristicMatrix(n, S, N, polynomialAtOver(I, R, S, f, v)(polynomialVariable(I, R, j))))79    exact determinant.characteristic_map with *80  unfold characteristicPolynomial81  cc8283theorem characteristicPolynomial.annihilates (n : Nat) (M N j w k : Set)84  requires matrixM : RingMatrix(n, R, M)85  requires matrixN : RingMatrix(n, S, N)86  requires index : j ∈ I87  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])88  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)89  requires coordinate : k ∈ n90  shows S[polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) * w(k)] = S[0]91proof92  have scalar := FunctionBetween.apply_closed with *93  have evaluated := characteristicPolynomial.evaluate_over with *94  have annihilated := characteristicMatrix.annihilates with *95  cc969798-- The mapped-matrix form constructs the coefficient extension automatically.99theorem characteristicPolynomial.evaluate_mapped (n : Nat) (M j : Set)100  requires matrix : RingMatrix(n, R, M)101  requires index : j ∈ I102  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) =103    determinant(n, S, characteristicMatrix(n, S, matrixMap(n, R, S, f, M), v(j)))104proof105  have function := IsRingHom.function with hom106  have mapped := matrixMap.matrix with *107  have entries : ∀ a ∈ n, ∀ b ∈ n, matrixMap(n, R, S, f, M)[a, b] = f(M[a, b])108    intros a ha b hb109    exact matrixMap.entry with *110  exact characteristicPolynomial.evaluate_over with *111112-- Nonzero eigenvectors yield roots only when zero divisors are excluded.113theorem characteristicPolynomial.root (n : Nat) (M N j w k : Set)114  requires domain : IsIntegralDomain(S)115  requires matrixM : RingMatrix(n, R, M)116  requires matrixN : RingMatrix(n, S, N)117  requires index : j ∈ I118  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])119  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)120  requires coordinate : k ∈ n121  requires nonzero : w(k) ≠ S[0]122  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) = S[0]123proof124  have scalar := FunctionBetween.apply_closed with *125  have characteristic := characteristicMatrix.matrix at n, B, plus, z, minus, times, unit, N, v(j) with *126  have kernel := characteristicMatrix.left_kernel with *127  have vanishes := determinant.zero_of_nonzero_left_kernel with *128  have evaluated := characteristicPolynomial.evaluate_over with *129  cc130131end Evaluation132