Grace/Cumulus/Algebra/Ring/FiniteSetSum.g17

Open in Workbench Download source

Imports

IndexedSum

Declarations

Source

1-- Canonical finite-set sums from enumeration independence, without Choice.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.FiniteSetSum8import IndexedSum910theorem WeightedValues.of_functions (w f V A n : Set)11  requires weights : w : V → A12  requires enumeration : f : n → V13  shows WeightedValues(w, f, A, n)14proof15  intros i hi16  have member := FunctionBetween.apply_closed at f, n, V, i with *17  exact FunctionBetween.apply_closed at w, V, A, f(i) with *1819defunique finiteRingSum (V A add zero neg mul one w : Set) (sum ∈ A) :=20  ∃ n, Nat(n) ∧ ∃ f, BijectiveBetween(f, n, V) ∧ sum = indexedRingSum(w, f, add, zero, n)21requires ring : IsCommRing(A, add, zero, neg, mul, one)22requires finite : Finite(V)23requires weights : w : V → A24proof25  obtain ⟨n, natural, equivalent⟩ := finite26  obtain ⟨f, bijective⟩ := equivalent27  have enumeration := converse.bijective with bijective28  have function := converse.function_of_bijective with bijective29  have values := WeightedValues.of_functions with weights, function30  have closure := indexedRingSum.closed at A, add, zero, neg, mul, one, w, converse(f, V, n), n with *31  have sumIn := closure with values32  witness indexedRingSum(w, converse(f, V, n), add, zero, n)33  refine ⟨sumIn, n, natural, converse(f, V, n), enumeration, rfl⟩34uniqueness35  intros u uIn first v vIn second36  obtain ⟨n, naturalN, f, enumerationF, valueF⟩ := first37  obtain ⟨m, naturalM, g, enumerationG, valueG⟩ := second38  have same := indexedRingSum.reindex at A, add, zero, neg, mul, one, w, V, f, g, n, m with *39  cc4041notation scoped finiteRingSum(V, R, w) => finiteRingSum(V, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, w)4243theorem finiteRingSum.closed (V A add zero neg mul one w : Set)44  requires ring : IsCommRing(A, add, zero, neg, mul, one)45  requires finite : Finite(V)46  requires weights : w : V → A47  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) ∈ A48proof49  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *50  exact selected.left5152theorem finiteRingSum.enumeration (V A add zero neg mul one w f : Set, n : Nat)53  requires ring : IsCommRing(A, add, zero, neg, mul, one)54  requires weights : w : V → A55  requires enumeration : BijectiveBetween(f, n, V)56  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) = indexedRingSum(w, f, add, zero, n)57proof58  have reverse := converse.bijective with enumeration59  have cardinality : HasCardinality(V, n)60    unfold HasCardinality61    refine ⟨assumption, ?_⟩62    unfold Equipotent63    refine ⟨converse(f, n, V), reverse⟩64  have finite := Finite.from_cardinality with cardinality65  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *66  obtain ⟨m, naturalM, g, enumerationG, value⟩ := selected.right67  have same := indexedRingSum.reindex at A, add, zero, neg, mul, one, w, V, g, f, m, n with *68  cc6970theorem indexedRingSum.congr (w v f g add zero : Set, n : Nat)71  shows (∀ i ∈ n, w(f(i)) = v(g(i))) → indexedRingSum(w, f, add, zero, n) = indexedRingSum(v, g, add, zero, n)72proof73  induction n74  | zero =>75    intro values76    simp [indexedRingSum]77  | succ(k) using ih =>78    intro values79    have prefix : ∀ i ∈ k, w(f(i)) = v(g(i))80      intros i before81      have included := membership.into_successor with *82      exact values with i, included83    have last := values with k, membership.self_successor at k with *84    have previous := ih with prefix85    rw [indexedRingSum, indexedRingSum, previous, last]86    rfl8788theorem finiteRingSum.congr (V A add zero neg mul one w v : Set)89  requires ring : IsCommRing(A, add, zero, neg, mul, one)90  requires finite : Finite(V)91  requires weightsW : w : V → A92  requires weightsV : v : V → A93  requires values : ∀ x ∈ V, w(x) = v(x)94  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) = finiteRingSum(V, A, add, zero, neg, mul, one, v)95proof96  have equal := FunctionBetween.ext with weightsW, weightsV, values97  rw equal98  rfl99100theorem indexedRingSum.zero (A add zero neg mul one w f : Set, n : Nat)101  requires ring : IsCommRing(A, add, zero, neg, mul, one)102  shows (∀ i ∈ n, w(f(i)) = zero) → indexedRingSum(w, f, add, zero, n) = zero103proof104  induction n105  | zero =>106    intro values107    rw indexedRingSum108    rfl109  | succ(k) using ih =>110    intro values111    have prefix : ∀ i ∈ k, w(f(i)) = zero112      intros i before113      have included := membership.into_successor with *114      exact values with i, included115    have last := values with k, membership.self_successor at k with *116    have previous := ih with prefix117    rw [indexedRingSum, previous, last]118    ring119120theorem finiteRingSum.zero (V A add zero neg mul one w : Set)121  requires ring : IsCommRing(A, add, zero, neg, mul, one)122  requires finite : Finite(V)123  requires weights : w : V → A124  requires values : ∀ x ∈ V, w(x) = zero125  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) = zero126proof127  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *128  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right129  have injective := Bijective.injective with enumeration130  have function := Injective.function with injective131  have vanishing : ∀ i ∈ n, w(f(i)) = zero132    intros i hi133    have member := FunctionBetween.apply_closed with *134    exact values with f(i), member135  have zeroSum := indexedRingSum.zero at A, add, zero, neg, mul, one, w, f, n with *136  rw equation137  exact zeroSum with vanishing138139section Linearity140variable (V A add zero neg mul one w : Set)141hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)142hypothesis finite : Finite(V)143hypothesis weights : w : V → A144notation ring R := (A, add, zero, neg, mul, one)145146theorem finiteRingSum.add (v : Set)147  requires weightsV : v : V → A148  shows finiteRingSum(V, A, add, zero, neg, mul, one, coefficientAdd(V, A, add, zero, neg, mul, one, w, v)) =149    finiteRingSum(V, A, add, zero, neg, mul, one, w) + finiteRingSum(V, A, add, zero, neg, mul, one, v)150proof151  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *152  obtain ⟨n, natural, f, enumeration, equationW⟩ := selected.right153  have inj := Bijective.injective with enumeration154  have function := Injective.function with inj155  have valuesW := WeightedValues.of_functions with weights, function156  have valuesV := WeightedValues.of_functions with weightsV, function157  have combined := coefficientAdd.function at V, A, add, zero, neg, mul, one, w, v with *158  have equationV := finiteRingSum.enumeration at V, A, add, zero, neg, mul, one, v, f, n with *159  have equationSum := finiteRingSum.enumeration at V, A, add, zero, neg, mul, one, coefficientAdd(V, A, add, zero, neg, mul, one, w, v), f, n with *160  have equations : ∀ i ∈ n, coefficientAdd(V, A, add, zero, neg, mul, one, w, v)(f(i)) = w(f(i)) + v(f(i))161    intros i hi162    have member := FunctionBetween.apply_closed with *163    exact coefficientAdd.value at V, A, add, zero, neg, mul, one, w, v, f(i) with *164  have distribute := indexedRingSum.add at A, add, zero, neg, mul, one, w, v, coefficientAdd(V, A, add, zero, neg, mul, one, w, v), f, n with *165  rw [equationSum, equationW, equationV]166  exact distribute with valuesW, valuesV, equations167168theorem finiteRingSum.scale (a : Set)169  requires scalar : a ∈ A170  shows finiteRingSum(V, A, add, zero, neg, mul, one, coefficientScale(V, A, add, zero, neg, mul, one, a, w)) =171    a * finiteRingSum(V, A, add, zero, neg, mul, one, w)172proof173  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *174  obtain ⟨n, natural, f, enumeration, equationW⟩ := selected.right175  have inj := Bijective.injective with enumeration176  have function := Injective.function with inj177  have valuesW := WeightedValues.of_functions with weights, function178  have scaled := coefficientScale.function at V, A, add, zero, neg, mul, one, a, w with *179  have equationScale := finiteRingSum.enumeration at V, A, add, zero, neg, mul, one, coefficientScale(V, A, add, zero, neg, mul, one, a, w), f, n with *180  have equations : ∀ i ∈ n, coefficientScale(V, A, add, zero, neg, mul, one, a, w)(f(i)) = a * w(f(i))181    intros i hi182    have member := FunctionBetween.apply_closed at f, n, V, i with *183    exact coefficientScale.value at V, A, add, zero, neg, mul, one, a, w, f(i) with *184  have distribute := indexedRingSum.scale at A, add, zero, neg, mul, one, w, a, coefficientScale(V, A, add, zero, neg, mul, one, a, w), f, n with *185  rw [equationScale, equationW]186  exact distribute with valuesW, equations187188end Linearity189