Grace/Cumulus/Algebra/Ring/CharacteristicMatrix.g17

Open in Workbench Download source

Imports

DeterminantKernel · DeterminantHom

Declarations

Source

1-- The characteristic matrix xI-M and its eigenvector annihilation law (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.Ring.CharacteristicMatrix8import DeterminantKernel9import DeterminantHom1011defunique characteristicEntry (I A add zero neg mul one M x p : Set) (a ∈ A) :=12  ∃ i ∈ I, ∃ j ∈ I, p = (i, j) ∧ a = call2(add, singleValue(A, zero, x, j, i), neg(M[i, j]))13requires ring : IsCommRing(A, add, zero, neg, mul, one)14requires matrix : RingMatrix(I, A, M)15requires scalar : x ∈ A16requires pair : p ∈ I × I17proof18  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at19    I, I, p with *20  have ordinary := IsCommRing.ring with ring21  have zeroIn := IsRing.zero_in_carrier with ordinary22  have diagonal := singleValue.closed at A, zero, x, j, i with *23  have entry := RingMatrix.entry at I, A, M, i, j with *24  have negative := IsRing.neg_closed with ordinary, entry25  have value := IsRing.add_closed with ordinary, diagonal, negative26  refine ⟨call2(add, singleValue(A, zero, x, j, i), neg(M[i, j])), value, i, hi, j, hj, shape, rfl⟩27uniqueness28  intros u hu first v hv second29  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first30  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second31  have equal : (i, j) = (k, l)32    cc33  have coordinates := orderedPair.injective at i, j, k, l with equal34  cc3536defgraph characteristicMatrix (I A add zero neg mul one M x : Set) (p ∈ I × I) : A :=37  characteristicEntry(I, A, add, zero, neg, mul, one, M, x, p)38requires ring : IsCommRing(A, add, zero, neg, mul, one)39requires matrix : RingMatrix(I, A, M)40requires scalar : x ∈ A41proof42  have selected := characteristicEntry.selected at I, A, add, zero, neg, mul, one, M, x, p with *43  exact selected.left4445notation scoped characteristicMatrix(I, R, M, x) => characteristicMatrix(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, x)4647section Matrices48variable (I A add zero neg mul one M x : Set)49notation ring R := (A, add, zero, neg, mul, one)50hypothesis ring : IsCommRing(R)51hypothesis matrix : RingMatrix(I, R, M)52hypothesis scalar : x ∈ R5354theorem characteristicMatrix.matrix55  shows RingMatrix(I, R, characteristicMatrix(I, R, M, x))56proof57  unfold RingMatrix58  exact characteristicMatrix.function with *5960theorem characteristicMatrix.entry (i j : Set)61  requires row : i ∈ I62  requires column : j ∈ I63  shows characteristicMatrix(I, R, M, x)[i, j] = R[singleValue(A, zero, x, j, i) - M[i, j]]64proof65  have pair := product.pair at i, j, I, I with *66  have selected := characteristicEntry.selected at I, A, add, zero, neg, mul, one, M, x, (i, j) with *67  obtain ⟨k, hk, l, hl, shape, result⟩ := selected.right68  have coordinates := orderedPair.injective with shape69  have value := characteristicMatrix.value at I, A, add, zero, neg, mul, one, M, x, (i, j) with *70  cc7172theorem characteristicMatrix.diagonal (i : Set)73  requires row : i ∈ I74  shows characteristicMatrix(I, R, M, x)[i, i] = R[x - M[i, i]]75proof76  have ordinary := IsCommRing.ring with ring77  have zeroIn := IsRing.zero_in_carrier with ordinary78  have same : i = i by rfl79  have diagonal := singleValue.same at A, zero, x, i, i with *80  have entry := characteristicMatrix.entry at I, A, add, zero, neg, mul, one, M, x, i, i with *81  cc8283theorem characteristicMatrix.off_diagonal (i j : Set)84  requires row : i ∈ I85  requires column : j ∈ I86  requires distinct : i ≠ j87  shows characteristicMatrix(I, R, M, x)[i, j] = R[-M[i, j]]88proof89  have ordinary := IsCommRing.ring with ring90  have zeroIn := IsRing.zero_in_carrier with ordinary91  have diagonal := singleValue.other at A, zero, x, j, i with *92  have entry := characteristicMatrix.entry at I, A, add, zero, neg, mul, one, M, x, i, j with *93  have closed := RingMatrix.entry at I, A, M, i, j with *94  rw [entry, diagonal]95  ring9697end Matrices9899-- The eigenvector equation includes the zero vector; nonzero coordinates are100-- required separately only when a root, rather than annihilation, is needed.101predicate LeftEigenvector (I A add zero neg mul one M x v : Set) :=102  FunctionBetween(v, I, A) ∧ ∀ j ∈ I, rowVectorEntry(I, A, add, zero, neg, mul, one, v, M, j) = call2(mul, x, v(j))103104notation scoped LeftEigenvector(I, R, M, x, v) => LeftEigenvector(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, x, v)105106section Eigenvectors107variable (I A add zero neg mul one M x v : Set)108notation ring R := (A, add, zero, neg, mul, one)109hypothesis ring : IsCommRing(R)110hypothesis finite : Finite(I)111hypothesis matrix : RingMatrix(I, R, M)112hypothesis scalar : x ∈ R113hypothesis eigenvector : LeftEigenvector(I, R, M, x, v)114115theorem characteristicMatrix.left_kernel116  shows LeftKernelVector(I, R, characteristicMatrix(I, R, M, x), v)117proof118  have vector := eigenvector.left119  have eigen := eigenvector.right120  have characteristic := characteristicMatrix.matrix at I, A, add, zero, neg, mul, one, M, x with *121  have ordinary := IsCommRing.ring with ring122  have zeroIn := IsRing.zero_in_carrier with ordinary123  have multiplicative := IsRing.multiplicative with ordinary124  have unit := IsMonoid.unit_in_carrier with multiplicative125  have negativeUnit := IsRing.neg_closed with ordinary, unit126  constructor127  . exact vector128  . intros j hj129    have valueIn := FunctionBetween.apply_closed at v, I, A, j with *130    have diagonalIn := RingMatrix.entry at I, A, M, j, j with *131    have productIn := IsRing.mul_closed with ordinary, scalar, valueIn132    have original := rowVectorWeights.function at I, A, add, zero, neg, mul, one, v, M, j with *133    have changed := rowVectorWeights.function at I, A, add, zero, neg, mul, one, v, characteristicMatrix(I, R, M, x), j with *134    have single := coefficientSingle.function at I, A, zero, R[x * v(j)], j with *135    have entries : ∀ i ∈ I, rowVectorWeights(I, R, v, characteristicMatrix(I, R, M, x), j)(i) = R[1 * coefficientSingle(I, A, zero, x * v(j), j)(i) + (-1) * rowVectorWeights(I, R, v, M, j)(i)]136      intros i hi137      have coefficient := FunctionBetween.apply_closed at v, I, A, i with *138      have matrixEntry := RingMatrix.entry at I, A, M, i, j with *139      have left := rowVectorWeights.value at I, A, add, zero, neg, mul, one, v, characteristicMatrix(I, R, M, x), j, i with *140      have right := rowVectorWeights.value at I, A, add, zero, neg, mul, one, v, M, j, i with *141      have entry := characteristicMatrix.entry at I, A, add, zero, neg, mul, one, M, x, i, j with *142      have alternatives : i = j ∨ i ≠ j by tauto143      cases alternatives with same | different144      . have delta := singleValue.same at A, zero, x, j, i with *145        have selected := coefficientSingle.same at I, A, zero, R[x * v(j)], j with *146        rw [left, right, entry, delta, same, selected]147        ring148      . have delta := singleValue.other at A, zero, x, j, i with *149        have selected := coefficientSingle.other at I, A, zero, R[x * v(j)], j, i with *150        rw [left, right, entry, delta, selected]151        ring152    have linear := finiteRingSum.linear at I, A, add, zero, neg, mul, one, coefficientSingle(I, A, zero, R[x * v(j)], j), rowVectorWeights(I, R, v, M, j), rowVectorWeights(I, R, v, characteristicMatrix(I, R, M, x), j), one, R[-1] with *153    have singleSum := finiteRingSum.single at I, A, add, zero, neg, mul, one, R[x * v(j)], j with *154    have eigenEquation := eigen with j, hj155    unfold rowVectorEntry at eigenEquation156    simp [rowVectorEntry]157    ring158159end Eigenvectors160161section Annihilation162variable (A add zero neg mul one : Set)163notation ring R := (A, add, zero, neg, mul, one)164hypothesis ring : IsCommRing(R)165166theorem characteristicMatrix.annihilates (n : Nat) (M x v j : Set)167  requires matrix : RingMatrix(n, R, M)168  requires scalar : x ∈ R169  requires eigenvector : LeftEigenvector(n, R, M, x, v)170  requires index : j ∈ n171  shows determinant(n, R, characteristicMatrix(n, R, M, x)) * v(j) = R[0]172proof173  have characteristic := characteristicMatrix.matrix with *174  have kernel := characteristicMatrix.left_kernel with *175  exact determinant.annihilates_left_kernel with *176177end Annihilation178section Homomorphisms179variable (A add zero neg mul one B plus z minus times unit h : Set)180notation ring R := (A, add, zero, neg, mul, one)181notation ring S := (B, plus, z, minus, times, unit)182hypothesis source : IsCommRing(R)183hypothesis target : IsCommRing(S)184hypothesis hom : IsRingHom(h, R, S)185186theorem characteristicMatrix.map_entries (I M N x : Set)187  requires matrixM : RingMatrix(I, R, M)188  requires matrixN : RingMatrix(I, S, N)189  requires scalar : x ∈ R190  requires entries : ∀ i ∈ I, ∀ j ∈ I, N[i, j] = h(M[i, j])191  shows ∀ i ∈ I, ∀ j ∈ I,192    characteristicMatrix(I, S, N, h(x))[i, j] = h(characteristicMatrix(I, R, M, x)[i, j])193proof194  have ordinaryR := IsCommRing.ring with source195  have ordinaryS := IsCommRing.ring with target196  have zeroR := IsRing.zero_in_carrier with ordinaryR197  have zeroS := IsRing.zero_in_carrier with ordinaryS198  have image := IsRingHom.closed with hom, scalar199  have mapsZero := IsRingHom.zero with hom200  intros i hi j hj201  have matrixEntry := RingMatrix.entry at I, A, M, i, j with *202  have deltaMap : singleValue(B, z, h(x), j, i) = h(singleValue(A, zero, x, j, i))203    have alternatives : i = j ∨ i ≠ j by tauto204    cases alternatives with same | different205    . have left := singleValue.same at B, z, h(x), j, i with *206      have right := singleValue.same at A, zero, x, j, i with *207      cc208    . have left := singleValue.other at B, z, h(x), j, i with *209      have right := singleValue.other at A, zero, x, j, i with *210      cc211  have left := characteristicMatrix.entry at I, B, plus, z, minus, times, unit, N, h(x), i, j with *212  have right := characteristicMatrix.entry at I, A, add, zero, neg, mul, one, M, x, i, j with *213  have preserved := IsRingHom.sub at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, singleValue(A, zero, x, j, i), M[i, j] with *214  have mapped := entries with i, hi, j, hj215  cc216217theorem determinant.characteristic_map (n : Nat) (M N x : Set)218  requires matrixM : RingMatrix(n, R, M)219  requires matrixN : RingMatrix(n, S, N)220  requires scalar : x ∈ R221  requires entries : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = h(M[i, j])222  shows h(determinant(n, R, characteristicMatrix(n, R, M, x))) =223    determinant(n, S, characteristicMatrix(n, S, N, h(x)))224proof225  have image := IsRingHom.closed with hom, scalar226  have first := characteristicMatrix.matrix at n, A, add, zero, neg, mul, one, M, x with *227  have second := characteristicMatrix.matrix at n, B, plus, z, minus, times, unit, N, h(x) with *228  have mapped := characteristicMatrix.map_entries with *229  exact determinant.map with *230231end Homomorphisms232