CharacteristicPolynomial

Characteristic polynomials over coefficient extensions, without Choice

Open in Workbench View on GitHub

1-- Characteristic polynomials over coefficient extensions, without Choice.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module CharacteristicPolynomialExample7import Grace.Cumulus.Algebra.Polynomial.Characteristic89section Extensions10variable (I A add zero neg mul one B plus z minus times unit f v : Set)11notation ring R := (A, add, zero, neg, mul, one)12notation ring S := (B, plus, z, minus, times, unit)13notation ring P := R[I]14hypothesis source : IsCommRing(R)15hypothesis target : IsCommRing(S)16hypothesis hom : IsRingHom(f, R, S)17hypothesis assignment : v : I → S1819theorem polynomial (n : Nat) (M j : Set)20  requires matrix : RingMatrix(n, R, M)21  requires index : j ∈ I22  shows characteristicPolynomial(n, I, R, M, j) ∈ P23proof24  exact characteristicPolynomial.member with *2526theorem evaluate (n : Nat) (M j : Set)27  requires matrix : RingMatrix(n, R, M)28  requires index : j ∈ I29  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) =30    determinant(n, S, characteristicMatrix(n, S, matrixMap(n, R, S, f, M), v(j)))31proof32  exact characteristicPolynomial.evaluate_mapped with *3334theorem annihilate (n : Nat) (M N j w k : Set)35  requires matrixM : RingMatrix(n, R, M)36  requires matrixN : RingMatrix(n, S, N)37  requires index : j ∈ I38  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])39  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)40  requires coordinate : k ∈ n41  shows S[polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) * w(k)] = S[0]42proof43  exact characteristicPolynomial.annihilates with *4445theorem root (n : Nat) (M N j w k : Set)46  requires domain : IsIntegralDomain(S)47  requires matrixM : RingMatrix(n, R, M)48  requires matrixN : RingMatrix(n, S, N)49  requires index : j ∈ I50  requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])51  requires eigenvector : LeftEigenvector(n, S, N, v(j), w)52  requires coordinate : k ∈ n53  requires nonzero : w(k) ≠ S[0]54  shows polynomialAtOver(I, R, S, f, v)(characteristicPolynomial(n, I, R, M, j)) = S[0]55proof56  exact characteristicPolynomial.root with *5758end Extensions59