Grace/Cumulus/Algebra/MatrixAnnihilator.g17

Open in Workbench Download source

Imports

SpanAnnihilator · MultiplicationMatrix · IndexedCombinations · Polynomial.CharacteristicMonic

Declarations

Source

1-- A common monic annihilator for finite-module multiplication equations (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.MatrixAnnihilator9import SpanAnnihilator10import MultiplicationMatrix11import IndexedCombinations12import Polynomial.CharacteristicMonic1314section Algebras15variable (A add zero neg mul one B plus z minus times unit f x : Set)16notation ring R := (A, add, zero, neg, mul, one)17notation ring S := (B, plus, z, minus, times, unit)18hypothesis source : IsCommRing(R)19hypothesis target : IsCommRing(S)20hypothesis hom : IsRingHom(f, R, S)21hypothesis element : x ∈ S2223theorem multiplicationMatrix.monic_annihilator (xs : List(B)) (M : Set)24  requires matrix : RingMatrix(length{B}(xs), R, M)25  requires rows : ∀ i ∈ length{B}(xs), ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧ S[x * listCoefficient{B}(z, xs, i)] = linearCombination(R, S, f, xs, cs) ∧ (∀ j ∈ length{B}(xs), M[i, j] = listCoefficient{A}(zero, cs, j))26  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧ (∀ g ∈ listSupport{B}(xs), S[monicValue(R, f, S, x, cs) * g] = S[0])27proof28  have size : Nat(length{B}(xs)) by typecheck29  have ordinaryR := IsCommRing.ring with source30  have ordinaryS := IsCommRing.ring with target31  have zeroR := IsRing.zero_in_carrier with ordinaryR32  have zeroS := IsRing.zero_in_carrier with ordinaryS33  have function := IsRingHom.function with hom34  have matrixFunction : M : length{B}(xs) × length{B}(xs) → A by exact matrix35  have transpose := transposedMatrix.function at length{B}(xs), length{B}(xs), A, M with *36  have transposeMatrix : RingMatrix(length{B}(xs), R, transposedMatrix(length{B}(xs), length{B}(xs), A, M))37    exact transpose38  have mapped := matrixMap.matrix with matrix, function39  have vectorSupport := listEntries.function at B, z, xs with *40  have vectorValues : ∀ i ∈ length{B}(xs), listEntries(B, z, xs)(i) ∈ B41    intros i hi42    have positions := natural.member with size43    have index := positions with i, hi44    have value := listEntries.value at B, z, xs, i with *45    rw value46    exact listCoefficient.closed with *47  have vector := FunctionBetween.codomain_of_values with *48  have entries : ∀ r ∈ length{B}(xs), ∀ c ∈ length{B}(xs), matrixMap(length{B}(xs), R, S, f, transposedMatrix(length{B}(xs), length{B}(xs), A, M))[r, c] = f(transposedMatrix(length{B}(xs), length{B}(xs), A, M)[r, c])49    intros r hr c hc50    exact matrixMap.entry with *51  have eigenvector : LeftEigenvector(length{B}(xs), S, matrixMap(length{B}(xs), R, S, f, transposedMatrix(length{B}(xs), length{B}(xs), A, M)), x, listEntries(B, z, xs))52    unfold LeftEigenvector53    refine ⟨vector, ?_⟩54    intros i hi55    obtain ⟨cs, coefficients, count, equation, row⟩ := rows with i, hi56    have weights := rowVectorWeights.function at length{B}(xs), B, plus, z, minus, times, unit, listEntries(B, z, xs), matrixMap(length{B}(xs), R, S, f, transposedMatrix(length{B}(xs), length{B}(xs), A, M)), i with *57    have products : ∀ j ∈ length{B}(xs), rowVectorWeights(length{B}(xs), S, listEntries(B, z, xs), matrixMap(length{B}(xs), R, S, f, transposedMatrix(length{B}(xs), length{B}(xs), A, M)), i)(j) = S[f(listCoefficient{A}(zero, cs, j)) * listCoefficient{B}(z, xs, j)]58      intros j hj59      have positions := natural.member with size60      have index := positions with j, hj61      have coefficient := listCoefficient.closed at A, zero, cs, j with *62      have generator := listCoefficient.closed at B, z, xs, j with *63      have image := IsRingHom.closed with hom, coefficient64      have weight := rowVectorWeights.value at length{B}(xs), B, plus, z, minus, times, unit, listEntries(B, z, xs), matrixMap(length{B}(xs), R, S, f, transposedMatrix(length{B}(xs), length{B}(xs), A, M)), i, j with *65      have vectorEntry := listEntries.value at B, z, xs, j with *66      have mappedEntry := entries with j, hj, i, hi67      have transposed := transposedMatrix.pair at length{B}(xs), length{B}(xs), A, M, i, j with *68      have rowEntry := row with j, hj69      rw [weight, vectorEntry, mappedEntry, transposed, rowEntry]70      ring71    have sum := linearCombination.finite_sum with *72    have vectorEntry := listEntries.value at B, z, xs, i with *73    unfold rowVectorEntry74    rw ← sum75    rw vectorEntry76    symm77    exact equation78  obtain ⟨cs, coefficients, count, annihilates⟩ := LeftEigenvector.monic_annihilator at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, length{B}(xs), transposedMatrix(length{B}(xs), length{B}(xs), A, M), matrixMap(length{B}(xs), R, S, f, transposedMatrix(length{B}(xs), length{B}(xs), A, M)), x, listEntries(B, z, xs) with *79  refine ⟨cs, coefficients, count, ?_⟩80  intros g hg81  have covers := listSupport.exists_index at B, z, xs with *82  obtain ⟨i, index, bound, value⟩ := covers with g, hg83  have position : i ∈ length{B}(xs) by exact membership.of_Less at i, length{B}(xs) with index, bound84  have kills := annihilates with i, position85  have entry := listEntries.value at B, z, xs, i with *86  rwa [entry, value] at kills8788-- Faithfulness comes from the generators spanning the unit, not from freeness.89theorem FiniteAlgebraModule.integral90  requires finiteModule : FiniteAlgebraModule(f, R, S)91  shows IntegralOver(f, R, S, x)92proof93  obtain ⟨xs, list, spans, M, matrix, rows⟩ := FiniteAlgebraModule.multiplication_matrix at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x with *94  obtain ⟨cs, coefficients, count, annihilates⟩ := multiplicationMatrix.monic_annihilator at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, xs, M with *95  have bounded := listSupport.subset at B, xs with *96  have unitIn : S[1] ∈ linearSpan(f, R, S, listSupport{B}(xs))97    rw spans98    typecheck99  exact IntegralOver.of_annihilates_generators with *100101end Algebras102