FiniteModuleCoefficients

Coefficients and faithful annihilator certificates for finite algebra-modules

Open in Workbench View on GitHub

1-- Coefficients and faithful annihilator certificates for finite algebra-modules.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module FiniteModuleCoefficients8import Grace.Cumulus.Algebra.SpanAnnihilator910section Algebras11variable (A add zero neg mul one B plus z minus times unit f : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis source : IsCommRing(R)15hypothesis target : IsCommRing(S)16hypothesis hom : IsRingHom(f, R, S)1718theorem extract_coefficients19  requires finiteModule : FiniteAlgebraModule(f, R, S)20  shows ∃ xs, List(B, xs) ∧ (∀ y ∈ S, ∃ cs, List(A, cs) ∧21    ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs))22proof23  exact FiniteAlgebraModule.coefficients with *2425theorem certify_finite_module (xs : List(B))26  requires representations : ∀ y ∈ S, ∃ cs, List(A, cs) ∧ y = linearCombination(R, S, f, xs, cs)27  shows FiniteAlgebraModule(f, R, S)28proof29  exact FiniteAlgebraModule.of_coefficients with *3031theorem expose_one_coefficient (G x y : Set)32  requires bounded : G ⊆ S33  requires element : x ∈ S34  shows y ∈ linearSpan(f, R, S, insert(x, G)) ↔35    y ∈ S ∧ (∃ a ∈ R, ∃ u ∈ linearSpan(f, R, S, G), y = S[f(a) * x + u])36proof37  exact linearSpan.insert_membership with *3839theorem span_membership (xs : List(B)) (y : Set)40  shows y ∈ linearSpan(f, R, S, listSupport{B}(xs)) ↔41    (∃ cs, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs) ∧ y = linearCombination(R, S, f, xs, cs))42proof43  exact linearSpan.list_membership with *4445theorem faithful_generators (G p : Set)46  requires bounded : G ⊆ S47  requires element : p ∈ S48  requires annihilates : ∀ g ∈ G, S[p * g] = S[0]49  requires unitIn : S[1] ∈ linearSpan(f, R, S, G)50  shows p = S[0]51proof52  exact linearSpan.annihilator_zero with *5354theorem monic_annihilator_is_integral (G x : Set) (cs : List(A))55  requires bounded : G ⊆ S56  requires element : x ∈ S57  requires unitIn : S[1] ∈ linearSpan(f, R, S, G)58  requires annihilates : ∀ g ∈ G, S[monicValue(R, f, S, x, cs) * g] = S[0]59  shows IntegralOver(f, R, S, x)60proof61  exact IntegralOver.of_annihilates_generators with *6263-- Duplicate generators are allowed; this is not a basis representation.64theorem repeated_generator (x a b : Set)65  requires element : x ∈ S66  requires first : a ∈ R67  requires second : b ∈ R68  shows linearCombination(R, S, f, [x, x], [a, b]) = S[f(R[a + b]) * x]69proof70  have imageA := IsRingHom.closed with hom, first71  have imageB := IsRingHom.closed with hom, second72  have mapped := IsRingHom.add with hom, first, second73  simp [linearCombination, listHeadOr, listTail]74  ring7576theorem no_generators (cs : List(A))77  shows linearCombination(R, S, f, [], cs) = S[0]78proof79  rw linearCombination80  rfl8182end Algebras83