Grace/Cumulus/Algebra/Coefficients.g17

Open in Workbench Download source

Imports

Ring · Cardinal.ListSupport

Declarations

Source

1-- Finitely supported coefficient maps over a set-sized commutative ring (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.Coefficients8import Ring9import Cardinal.ListSupport1011def functionSupport (f I z : Set) : Set := {i ∈ I | f(i) ≠ z}12predicate CoefficientMap (f I A z : Set) := FunctionBetween(f, I, A) ∧ Finite(functionSupport(f, I, z))13def coefficientMaps (I A z : Set) : Set := {f ∈ 𝒫(I × A) | CoefficientMap(f, I, A, z)}1415theorem functionSupport.subset (f I z : Set)16  shows functionSupport(f, I, z) ⊆ I17proof18  simp1920theorem functionSupport.outside (f I z i : Set)21  requires hi : i ∈ I22  requires absent : ¬(i ∈ functionSupport(f, I, z))23  shows f(i) = z24proof25  ext y26  simp2728theorem CoefficientMap.function (f I A z : Set)29  requires map : CoefficientMap(f, I, A, z)30  shows f : I → A31proof32  exact map.left3334theorem CoefficientMap.finite_support (f I A z : Set)35  requires map : CoefficientMap(f, I, A, z)36  shows Finite(functionSupport(f, I, z))37proof38  exact map.right3940theorem coefficientMaps.contains (I A z f : Set)41  requires map : CoefficientMap(f, I, A, z)42  shows f ∈ coefficientMaps(I, A, z)43proof44  have function := CoefficientMap.function with map45  have relation := FunctionBetween.relation with function46  unfold RelationBetween at relation47  unfold Subset at relation48  have bound := set.powerset.backward with relation49  exact coefficientMaps.membership.backward with ⟨bound, map⟩5051theorem CoefficientMap.ext (f g I A z : Set)52  requires left : CoefficientMap(f, I, A, z)53  requires right : CoefficientMap(g, I, A, z)54  requires values : ∀ i ∈ I, f(i) = g(i)55  shows f = g56proof57  have functionF := CoefficientMap.function with left58  have functionG := CoefficientMap.function with right59  exact FunctionBetween.ext with functionF, functionG, values6061defgraph coefficientAdd (I A add zero neg mul one f g : Set) (i ∈ I) : A := call2(add, f(i), g(i))62requires ring : IsCommRing(A, add, zero, neg, mul, one)63requires left : f : I → A64requires right : g : I → A65proof66  have ordinary := IsCommRing.ring with ring67  have fi := FunctionBetween.apply_closed with left, member68  have gi := FunctionBetween.apply_closed with right, member69  exact IsRing.add_closed with ordinary, fi, gi7071notation scoped coefficientAdd(I, R, f, g) => coefficientAdd(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, f, g)7273defgraph coefficientNeg (I A add zero neg mul one f : Set) (i ∈ I) : A := neg(f(i))74requires ring : IsCommRing(A, add, zero, neg, mul, one)75requires function : f : I → A76proof77  have ordinary := IsCommRing.ring with ring78  have fi := FunctionBetween.apply_closed with function, member79  exact IsRing.neg_closed with ordinary, fi8081defgraph coefficientScale (I A add zero neg mul one a f : Set) (i ∈ I) : A := call2(mul, a, f(i))82requires ring : IsCommRing(A, add, zero, neg, mul, one)83requires scalar : a ∈ A84requires function : f : I → A85proof86  have ordinary := IsCommRing.ring with ring87  have fi := FunctionBetween.apply_closed with function, member88  exact IsRing.mul_closed with ordinary, scalar, fi8990notation scoped coefficientScale(I, R, a, f) => coefficientScale(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, a, f)9192section Rings93variable (I A add zero neg mul one : Set)94hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)95notation ring R := (A, add, zero, neg, mul, one)9697theorem CoefficientMap.zero98  shows CoefficientMap(constantFunction(I, A, zero), I, A, zero)99proof100  have ordinary := IsCommRing.ring with ring101  have zeroIn := IsRing.zero_in_carrier with ordinary102  have function := constantFunction.function at I, A, zero with zeroIn103  have support : functionSupport(constantFunction(I, A, zero), I, zero) = ∅104    ext i105    constructor106    . intro member107      have data := functionSupport.membership.forward with member108      have value := constantFunction.apply with data.left, zeroIn109      have contradiction := data.right with value110      tauto111    . intro member112      simp113  unfold CoefficientMap114  refine ⟨function, ?_⟩115  rw support116  exact Finite.empty117118theorem coefficientAdd.support (f g : Set)119  requires left : f : I → A120  requires right : g : I → A121  shows functionSupport(coefficientAdd(I, A, add, zero, neg, mul, one, f, g), I, zero) ⊆ functionSupport(f, I, zero) ∪ functionSupport(g, I, zero)122proof123  have ordinary := IsCommRing.ring with ring124  have zeroIn := IsRing.zero_in_carrier with ordinary125  have zeroSum : 0 + 0 = 0 by ring126  intros i hi127  have data := functionSupport.membership.forward with hi128  have value := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, g, i with *129  have casesF : f(i) = zero ∨ f(i) ≠ zero by tauto130  have casesG : g(i) = zero ∨ g(i) ≠ zero by tauto131  cases casesF with fZero | fNonzero132  . cases casesG with gZero | gNonzero133    . have equal : coefficientAdd(I, A, add, zero, neg, mul, one, f, g)(i) = zero134        cc135      have contradiction := data.right with equal136      tauto137    . have member : i ∈ functionSupport(g, I, zero)138        exact functionSupport.membership.backward with ⟨data.left, gNonzero⟩139      apply union2.membership.backward140      right141      exact member142  . have member : i ∈ functionSupport(f, I, zero)143      exact functionSupport.membership.backward with ⟨data.left, fNonzero⟩144    apply union2.membership.backward145    left146    exact member147148theorem CoefficientMap.add (f g : Set)149  requires left : CoefficientMap(f, I, A, zero)150  requires right : CoefficientMap(g, I, A, zero)151  shows CoefficientMap(coefficientAdd(I, A, add, zero, neg, mul, one, f, g), I, A, zero)152proof153  have functionF := CoefficientMap.function with left154  have functionG := CoefficientMap.function with right155  have finiteF := CoefficientMap.finite_support with left156  have finiteG := CoefficientMap.finite_support with right157  have finiteUnion := Finite.union with finiteF, finiteG158  have support := coefficientAdd.support with ring, functionF, functionG159  have finite := Finite.subset with finiteUnion, support160  have function := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, g with *161  unfold CoefficientMap162  refine ⟨function, finite⟩163164theorem coefficientNeg.support (f : Set)165  requires function : f : I → A166  shows functionSupport(coefficientNeg(I, A, add, zero, neg, mul, one, f), I, zero) ⊆ functionSupport(f, I, zero)167proof168  have zeroValue : -0 = 0 by ring169  intros i hi170  have data := functionSupport.membership.forward with hi171  have value := coefficientNeg.value at I, A, add, zero, neg, mul, one, f, i with *172  have casesF : f(i) = zero ∨ f(i) ≠ zero by tauto173  cases casesF with fZero | fNonzero174  . have equal : coefficientNeg(I, A, add, zero, neg, mul, one, f)(i) = zero175      cc176    have contradiction := data.right with equal177    tauto178  . apply functionSupport.membership.backward at f, I, zero, i179    refine ⟨data.left, fNonzero⟩180181theorem CoefficientMap.neg (f : Set)182  requires map : CoefficientMap(f, I, A, zero)183  shows CoefficientMap(coefficientNeg(I, A, add, zero, neg, mul, one, f), I, A, zero)184proof185  have functionF := CoefficientMap.function with map186  have finiteF := CoefficientMap.finite_support with map187  have support := coefficientNeg.support with *188  have finite := Finite.subset with finiteF, support189  have function := coefficientNeg.function at I, A, add, zero, neg, mul, one, f with *190  unfold CoefficientMap191  refine ⟨function, finite⟩192193theorem coefficientScale.support (a f : Set)194  requires scalar : a ∈ A195  requires function : f : I → A196  shows functionSupport(coefficientScale(I, A, add, zero, neg, mul, one, a, f), I, zero) ⊆ functionSupport(f, I, zero)197proof198  have zeroValue : a * 0 = 0 by ring199  intros i hi200  have data := functionSupport.membership.forward with hi201  have value := coefficientScale.value at I, A, add, zero, neg, mul, one, a, f, i with *202  have casesF : f(i) = zero ∨ f(i) ≠ zero by tauto203  cases casesF with fZero | fNonzero204  . have equal : coefficientScale(I, A, add, zero, neg, mul, one, a, f)(i) = zero205      cc206    have contradiction := data.right with equal207    tauto208  . apply functionSupport.membership.backward at f, I, zero, i209    refine ⟨data.left, fNonzero⟩210211theorem CoefficientMap.scale (a f : Set)212  requires scalar : a ∈ A213  requires map : CoefficientMap(f, I, A, zero)214  shows CoefficientMap(coefficientScale(I, A, add, zero, neg, mul, one, a, f), I, A, zero)215proof216  have functionF := CoefficientMap.function with map217  have finiteF := CoefficientMap.finite_support with map218  have support := coefficientScale.support with *219  have finite := Finite.subset with finiteF, support220  have function := coefficientScale.function at I, A, add, zero, neg, mul, one, a, f with *221  unfold CoefficientMap222  refine ⟨function, finite⟩223224theorem CoefficientMap.support_list (f : Set)225  requires map : CoefficientMap(f, I, A, zero)226  shows ∃ xs, List(I, xs) ∧ functionSupport(f, I, zero) ⊆ listSupport{I}(xs)227proof228  have finite := CoefficientMap.finite_support with map229  have subset := functionSupport.subset at f, I, zero230  exact Finite.cover_in with finite, subset231232theorem coefficientAdd.commutative (f g : Set)233  requires functionF : f : I → A234  requires functionG : g : I → A235  shows coefficientAdd(I, A, add, zero, neg, mul, one, f, g) = coefficientAdd(I, A, add, zero, neg, mul, one, g, f)236proof237  have ordinary := IsCommRing.ring with ring238  have zeroIn := IsRing.zero_in_carrier with ordinary239  have function0 := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, g with *240  have function1 := coefficientAdd.function at I, A, add, zero, neg, mul, one, g, f with *241  apply FunctionBetween.ext with function0, function1242  intros i hi243  have fIn := FunctionBetween.apply_closed at f, I, A, i with *244  have gIn := FunctionBetween.apply_closed at g, I, A, i with *245  have value0 := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, g, i with *246  have value1 := coefficientAdd.value at I, A, add, zero, neg, mul, one, g, f, i with *247  rw [value1, value0]248  ring249250theorem coefficientAdd.associative (f g h : Set)251  requires functionF : f : I → A252  requires functionG : g : I → A253  requires functionH : h : I → A254  shows coefficientAdd(I, A, add, zero, neg, mul, one, coefficientAdd(I, A, add, zero, neg, mul, one, f, g), h) = coefficientAdd(I, A, add, zero, neg, mul, one, f, coefficientAdd(I, A, add, zero, neg, mul, one, g, h))255proof256  have ordinary := IsCommRing.ring with ring257  have zeroIn := IsRing.zero_in_carrier with ordinary258  have function0 := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, g with *259  have function1 := coefficientAdd.function at I, A, add, zero, neg, mul, one, coefficientAdd(I, A, add, zero, neg, mul, one, f, g), h with *260  have function2 := coefficientAdd.function at I, A, add, zero, neg, mul, one, g, h with *261  have function3 := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, coefficientAdd(I, A, add, zero, neg, mul, one, g, h) with *262  apply FunctionBetween.ext with function1, function3263  intros i hi264  have fIn := FunctionBetween.apply_closed at f, I, A, i with *265  have gIn := FunctionBetween.apply_closed at g, I, A, i with *266  have hIn := FunctionBetween.apply_closed at h, I, A, i with *267  have value0 := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, g, i with *268  have value1 := coefficientAdd.value at I, A, add, zero, neg, mul, one, coefficientAdd(I, A, add, zero, neg, mul, one, f, g), h, i with *269  have value2 := coefficientAdd.value at I, A, add, zero, neg, mul, one, g, h, i with *270  have value3 := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, coefficientAdd(I, A, add, zero, neg, mul, one, g, h), i with *271  rw [value3, value2, value1, value0]272  ring273274theorem coefficientAdd.zero (f : Set)275  requires functionF : f : I → A276  shows coefficientAdd(I, A, add, zero, neg, mul, one, f, constantFunction(I, A, zero)) = f277proof278  have ordinary := IsCommRing.ring with ring279  have zeroIn := IsRing.zero_in_carrier with ordinary280  have functionZero := constantFunction.function at I, A, zero with zeroIn281  have function0 := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, constantFunction(I, A, zero) with *282  apply FunctionBetween.ext with function0, functionF283  intros i hi284  have fIn := FunctionBetween.apply_closed at f, I, A, i with *285  have zeroValue := constantFunction.apply at I, A, i, zero with *286  have value0 := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, constantFunction(I, A, zero), i with *287  rw [value0, zeroValue]288  ring289290theorem coefficientAdd.inverse (f : Set)291  requires functionF : f : I → A292  shows coefficientAdd(I, A, add, zero, neg, mul, one, f, coefficientNeg(I, A, add, zero, neg, mul, one, f)) = constantFunction(I, A, zero)293proof294  have ordinary := IsCommRing.ring with ring295  have zeroIn := IsRing.zero_in_carrier with ordinary296  have functionZero := constantFunction.function at I, A, zero with zeroIn297  have function0 := coefficientNeg.function at I, A, add, zero, neg, mul, one, f with *298  have function1 := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, coefficientNeg(I, A, add, zero, neg, mul, one, f) with *299  apply FunctionBetween.ext with function1, functionZero300  intros i hi301  have fIn := FunctionBetween.apply_closed at f, I, A, i with *302  have zeroValue := constantFunction.apply at I, A, i, zero with *303  have value0 := coefficientNeg.value at I, A, add, zero, neg, mul, one, f, i with *304  have value1 := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, coefficientNeg(I, A, add, zero, neg, mul, one, f), i with *305  rw [value1, value0, zeroValue]306  ring307308theorem coefficientScale.one (f : Set)309  requires functionF : f : I → A310  shows coefficientScale(I, A, add, zero, neg, mul, one, one, f) = f311proof312  have ordinary := IsCommRing.ring with ring313  have zeroIn := IsRing.zero_in_carrier with ordinary314  have multiplicative := IsRing.multiplicative with ordinary315  have oneIn := IsMonoid.unit_in_carrier with multiplicative316  have function0 := coefficientScale.function at I, A, add, zero, neg, mul, one, one, f with *317  apply FunctionBetween.ext with function0, functionF318  intros i hi319  have fIn := FunctionBetween.apply_closed at f, I, A, i with *320  have value0 := coefficientScale.value at I, A, add, zero, neg, mul, one, one, f, i with *321  rw value0322  ring323324theorem coefficientScale.associative (a b f : Set)325  requires aIn : a ∈ A326  requires bIn : b ∈ A327  requires functionF : f : I → A328  shows coefficientScale(I, A, add, zero, neg, mul, one, a, coefficientScale(I, A, add, zero, neg, mul, one, b, f)) = coefficientScale(I, A, add, zero, neg, mul, one, call2(mul, a, b), f)329proof330  have ordinary := IsCommRing.ring with ring331  have zeroIn := IsRing.zero_in_carrier with ordinary332  have productIn := IsRing.mul_closed at A, add, zero, neg, mul, one, a,333    b with *334  have function0 := coefficientScale.function at I, A, add, zero, neg, mul, one, b, f with *335  have function1 := coefficientScale.function at I, A, add, zero, neg, mul, one, a, coefficientScale(I, A, add, zero, neg, mul, one, b, f) with *336  have function2 := coefficientScale.function at I, A, add, zero, neg, mul, one, call2(mul, a, b), f with *337  apply FunctionBetween.ext with function1, function2338  intros i hi339  have fIn := FunctionBetween.apply_closed at f, I, A, i with *340  have value0 := coefficientScale.value at I, A, add, zero, neg, mul, one, b, f, i with *341  have value1 := coefficientScale.value at I, A, add, zero, neg, mul, one, a, coefficientScale(I, A, add, zero, neg, mul, one, b, f), i with *342  have value2 := coefficientScale.value at I, A, add, zero, neg, mul, one, call2(mul, a, b), f, i with *343  rw [value2, value1, value0]344  ring345346theorem coefficientScale.add (a f g : Set)347  requires aIn : a ∈ A348  requires functionF : f : I → A349  requires functionG : g : I → A350  shows coefficientScale(I, A, add, zero, neg, mul, one, a, coefficientAdd(I, A, add, zero, neg, mul, one, f, g)) = coefficientAdd(I, A, add, zero, neg, mul, one, coefficientScale(I, A, add, zero, neg, mul, one, a, f), coefficientScale(I, A, add, zero, neg, mul, one, a, g))351proof352  have ordinary := IsCommRing.ring with ring353  have zeroIn := IsRing.zero_in_carrier with ordinary354  have function0 := coefficientAdd.function at I, A, add, zero, neg, mul, one, f, g with *355  have function1 := coefficientScale.function at I, A, add, zero, neg, mul, one, a, coefficientAdd(I, A, add, zero, neg, mul, one, f, g) with *356  have function2 := coefficientScale.function at I, A, add, zero, neg, mul, one, a, f with *357  have function3 := coefficientScale.function at I, A, add, zero, neg, mul, one, a, g with *358  have function4 := coefficientAdd.function at I, A, add, zero, neg, mul, one, coefficientScale(I, A, add, zero, neg, mul, one, a, f), coefficientScale(I, A, add, zero, neg, mul, one, a, g) with *359  apply FunctionBetween.ext with function1, function4360  intros i hi361  have fIn := FunctionBetween.apply_closed at f, I, A, i with *362  have gIn := FunctionBetween.apply_closed at g, I, A, i with *363  have value0 := coefficientAdd.value at I, A, add, zero, neg, mul, one, f, g, i with *364  have value1 := coefficientScale.value at I, A, add, zero, neg, mul, one, a, coefficientAdd(I, A, add, zero, neg, mul, one, f, g), i with *365  have value2 := coefficientScale.value at I, A, add, zero, neg, mul, one, a, f, i with *366  have value3 := coefficientScale.value at I, A, add, zero, neg, mul, one, a, g, i with *367  have value4 := coefficientAdd.value at I, A, add, zero, neg, mul, one, coefficientScale(I, A, add, zero, neg, mul, one, a, f), coefficientScale(I, A, add, zero, neg, mul, one, a, g), i with *368  rw [value4, value3, value2, value1, value0]369  ring370371end Rings372