Grace/Cumulus/Algebra/Ring/SumExtension.g17

Open in Workbench Download source

Imports

FiniteSetSum

Declarations

Source

1-- Inserting fresh indices into canonical finite sums (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.Ring.SumExtension8import FiniteSetSum910theorem finiteRingSum.empty (A add zero neg mul one w : Set)11  requires ring : IsCommRing(A, add, zero, neg, mul, one)12  requires weights : w : ∅ → A13  shows finiteRingSum(∅, A, add, zero, neg, mul, one, w) = zero14proof15  have finite := Finite.empty16  have values : ∀ x ∈ ∅, w(x) = zero17    intros x impossible18    exfalso19    exact set.empty with impossible20  exact finiteRingSum.zero with ring, finite, weights, values2122theorem finiteRingSum.insert (V A add zero neg mul one w a : Set)23  requires ring : IsCommRing(A, add, zero, neg, mul, one)24  requires finite : Finite(V)25  requires weights : w : insert(a, V) → A26  requires fresh : ¬(a ∈ V)27  shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one, w) =28    call2(add, finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V)), w(a))29proof30  have subset : V ⊆ insert(a, V)31    intros x hx32    exact insert.contains with hx33  have closed : ∀ x ∈ V, w(x) ∈ A34    intros x hx35    have member := insert.contains at x, a, V with hx36    exact FunctionBetween.apply_closed at w, insert(a, V), A, x with *37  have restricted := restrict.function at w, insert(a, V), A, V, A with *38  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, restrict(w, V) with *39  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right40  have injective := Bijective.injective with enumeration41  have function := Injective.function with injective42  have nFresh := membership.irreflexive at n43  have extended := adjoinMap.bijective with enumeration, nFresh, fresh44  have successor := natural.successor_as_insert with natural45  rw ← successor at extended46  have extendedInjective := Bijective.injective with extended47  have extendedFunction := Injective.function with extendedInjective48  have extendedSum := finiteRingSum.enumeration at insert(a, V), A, add, zero, neg, mul, one, w, adjoinMap(f, n, a), succ(n) with *49  have oldValues : ∀ i ∈ n, w(adjoinMap(f, n, a)(i)) = restrict(w, V)(f(i))50    intros i hi51    have oldMember := FunctionBetween.apply_closed at f, n, V, i with *52    have oldEdge := FunctionBetween.relates_apply at f, n, V, i with *53    have edge := adjoinMap.relates_old at f, n, a, i, f(i) with oldEdge54    have next := membership.into_successor at i, n with *55    have value := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), i, f(i) with *56    have restrictedValue := restrict.apply at w, insert(a, V), A, V, A, f(i) with *57    cc58  have congr := indexedRingSum.congr at w, restrict(w, V), adjoinMap(f, n, a), f, add, zero, n with natural59  have prefix := congr with oldValues60  have newIndex := membership.self_successor with natural61  have newEdge := adjoinMap.relates_new at f, n, a62  have newValue := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), n, a with *63  rw [extendedSum, indexedRingSum, prefix, newValue, equation]64  rfl6566theorem finiteRingSum.insert_zero (V A add zero neg mul one w a : Set)67  requires ring : IsCommRing(A, add, zero, neg, mul, one)68  requires finite : Finite(V)69  requires weights : w : insert(a, V) → A70  requires fresh : ¬(a ∈ V)71  requires vanishes : w(a) = zero72  shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one, w) =73    finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V))74proof75  have inserted := finiteRingSum.insert with *76  have subset : V ⊆ insert(a, V)77    intros x hx78    exact insert.contains with hx79  have closed : ∀ x ∈ V, w(x) ∈ A80    intros x hx81    have member := insert.contains at x, a, V with hx82    exact FunctionBetween.apply_closed with *83  have restricted := restrict.function with *84  have sumIn := finiteRingSum.closed with *85  rw [inserted, vanishes]86  ring87