FiniteSupportCoefficients

Finite support survives linear combinations of coefficient maps

Open in Workbench View on GitHub

1-- Finite support survives linear combinations of coefficient maps.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module FiniteSupportCoefficients8import Grace.Cumulus.Algebra.Coefficients910section Coefficients11variable (I A add zero neg mul one : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)1314theorem zero_in_carrier15  shows constantFunction(I, A, zero) ∈ coefficientMaps(I, A, zero)16proof17  have map := CoefficientMap.zero at I, A, add, zero, neg, mul, one with *18  exact coefficientMaps.contains with map1920theorem linear_combination (a f g : Set)21  requires scalar : a ∈ A22  requires left : CoefficientMap(f, I, A, zero)23  requires right : CoefficientMap(g, I, A, zero)24  shows coefficientAdd(I, A, add, zero, neg, mul, one, coefficientScale(I, A, add, zero, neg, mul, one, a, f), g) ∈ coefficientMaps(I, A, zero)25proof26  have scaled := CoefficientMap.scale at I, A, add, zero, neg, mul, one, a, f with *27  have combined := CoefficientMap.add with ring, scaled, right28  exact coefficientMaps.contains with combined2930theorem finite_enumeration (f : Set)31  requires map : CoefficientMap(f, I, A, zero)32  shows ∃ xs, List(I, xs) ∧ functionSupport(f, I, zero) ⊆ listSupport{I}(xs)33proof34  exact CoefficientMap.support_list at I, A, add, zero, neg, mul, one, f with *3536theorem cancellation (f : Set)37  requires map : CoefficientMap(f, I, A, zero)38  shows coefficientAdd(I, A, add, zero, neg, mul, one, f, coefficientNeg(I, A, add, zero, neg, mul, one, f)) = constantFunction(I, A, zero)39proof40  have function := CoefficientMap.function with map41  exact coefficientAdd.inverse with ring, function4243end Coefficients44