Grace/Cumulus/Algebra/Ring/Cancellation.g17

Open in Workbench Download source

Imports

SumSupport · Set.Involution

Declarations

Source

1-- Pairwise cancellation of finite sums, valid in every characteristic (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.Cancellation8import SumSupport9import Set.Involution1011section Sums12variable (D A add zero neg mul one w : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)15hypothesis weights : w : D → A1617theorem finiteRingSum.remove (V a : Set)18  requires finite : Finite(V)19  requires subset : V ⊆ D20  requires member : a ∈ V21  shows finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V)) =22    R[finiteRingSum(V ∖ {a}, A, add, zero, neg, mul, one, restrict(w, V ∖ {a})) + w(a)]23proof24  have restSubset : V ∖ {a} ⊆ V by simp [Subset, difference.membership]25  have smaller := Finite.subset with finite, restSubset26  have fresh : ¬(a ∈ V ∖ {a}) by simp [difference.membership, singleton.membership]27  have restore := insert.restore with member28  have restricted := restrict.domain_function with weights, subset29  have expanded : restrict(w, V) : insert(a, V ∖ {a}) → A by rwa restore30  have equation := finiteRingSum.insert with *31  have nested := restrict.nested at w, V ∖ {a}, V with restSubset32  have value := restrict.domain_apply with *33  rwa [restore, nested, value] at equation3435-- Remove one complete orbit. Fixed points must vanish separately: in36-- characteristic two, a value being its own negative does not imply zero.37theorem finiteRingSum.remove_orbit (V a b : Set)38  requires finite : Finite(V)39  requires subset : V ⊆ D40  requires first : a ∈ V41  requires second : b ∈ V42  requires opposite : w(b) = R[-w(a)]43  requires fixed : b = a → w(a) = R[0]44  shows finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V)) =45    finiteRingSum((V ∖ {a}) ∖ {b}, A, add, zero, neg, mul, one, restrict(w, (V ∖ {a}) ∖ {b}))46proof47  have restSubset : V ∖ {a} ⊆ V by simp [Subset, difference.membership]48  have restDomain := Subset.transitive with restSubset, subset49  have finiteRest := Finite.subset with finite, restSubset50  have pairedSubset : (V ∖ {a}) ∖ {b} ⊆ V ∖ {a} by simp [Subset, difference.membership]51  have pairedDomain := Subset.transitive with pairedSubset, restDomain52  have finitePair := Finite.subset with finiteRest, pairedSubset53  have pairWeights := restrict.domain_function with weights, pairedDomain54  have pairValue := finiteRingSum.closed with ring, finitePair, pairWeights55  have aIn : a ∈ D by simp [Subset]56  have value := FunctionBetween.apply_closed with weights, aIn57  have removed := finiteRingSum.remove at D, A, add, zero, neg, mul, one, w, V, a with *58  have alternatives : b = a ∨ b ≠ a by tauto59  cases alternatives with same | different60  . have vanishes := fixed with same61    have unchanged : (V ∖ {a}) ∖ {b} = V ∖ {a}62      rw same63      ext y64      simp [difference.membership]65    rw unchanged66    have restWeights := restrict.domain_function with weights, restDomain67    have restValue := finiteRingSum.closed with ring, finiteRest, restWeights68    rw [removed, vanishes]69    ring70  . have member : b ∈ V ∖ {a}71      simp [difference.membership, singleton.membership]72    have removedAgain := finiteRingSum.remove at D, A, add, zero, neg, mul, one, w, V ∖ {a}, b with *73    rw [removed, removedAgain, opposite]74    ring7576-- A list supplies finite induction only; it need not enumerate without repeats.77theorem finiteRingSum.involution_cover (t : Set) (xs : List(D))78  requires involution : InvolutionOn(t, D)79  requires opposite : ∀ a ∈ D, w(t(a)) = R[-w(a)]80  requires fixed : ∀ a ∈ D, t(a) = a → w(a) = R[0]81  shows ∀ V, V ⊆ D → V ⊆ listSupport{D}(xs) → (∀ a ∈ V, t(a) ∈ V) →82    finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V)) = R[0]83proof84  induction xs85  | List.nil =>86    intros V subset covered closed87    rw listSupport at covered88    have empty : V = ∅89      apply Subset.antisymmetric with covered90      exact empty.subset91    rw empty92    have bounded := empty.subset at D93    have restricted := restrict.domain_function with weights, bounded94    exact finiteRingSum.empty with ring, restricted95  | List.cons(a, tail) using ih =>96    intros V subset covered closed97    rw listSupport at covered98    have finiteSupport := listSupport.finite at D, List.cons{D}(a, tail) with *99    rw listSupport at finiteSupport100    have finite := Finite.subset with finiteSupport, covered101    have alternatives : a ∈ V ∨ ¬(a ∈ V) by tauto102    cases alternatives with present | absent103    . have partner := closed with a, present104      have pairedClosed := InvolutionOn.remove_pair with involution, subset, closed, present105      have pairedSubset : (V ∖ {a}) ∖ {t(a)} ⊆ D by simp [Subset, difference.membership]106      have pairedCovered : (V ∖ {a}) ∖ {t(a)} ⊆ listSupport{D}(tail)107        intros y member108        have outer := difference.membership.forward with member109        have inner := difference.membership.forward with outer.left110        have includes := covered111        have inserted := includes with y, inner.left112        have choices := insert.membership.forward with inserted113        cases choices with same | inTail114        . exfalso115          have singleton := singleton.membership.backward with same116          exact inner.right with singleton117        . exact inTail118      have previous := ih with (V ∖ {a}) ∖ {t(a)}, pairedSubset, pairedCovered, pairedClosed119      have aIn : a ∈ D by assumption120      have negative := opposite with a, aIn121      have fixedValue := fixed with a, aIn122      have removed := finiteRingSum.remove_orbit at D, A, add, zero, neg, mul, one, w, V, a, t(a) with *123      cc124    . have smaller : V ⊆ listSupport{D}(tail)125        intros y member126        have includes := covered127        have inserted := includes with y, member128        have choices := insert.membership.forward with inserted129        cases choices with same | inTail130        . exfalso131          rw same at member132          exact absent with member133        . exact inTail134      exact ih with V, subset, smaller, closed135136theorem finiteRingSum.involution (t : Set)137  requires finite : Finite(D)138  requires involution : InvolutionOn(t, D)139  requires opposite : ∀ a ∈ D, w(t(a)) = R[-w(a)]140  requires fixed : ∀ a ∈ D, t(a) = a → w(a) = R[0]141  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = R[0]142proof143  obtain ⟨xs, list, covered⟩ := Finite.list_cover with finite144  have reflexive : D ⊆ D by simp [Subset]145  have function := InvolutionOn.function with involution146  have closed : ∀ a ∈ D, t(a) ∈ D147    intros a member148    exact FunctionBetween.apply_closed with function, member149  have scan := finiteRingSum.involution_cover with *150  have sum := scan with D, reflexive, covered, closed151  have restricted := restrict.domain_function with weights, reflexive152  have same : restrict(w, D) = w153    apply FunctionBetween.ext with restricted, weights154    intros a member155    exact restrict.domain_apply with weights, reflexive, member156  rwa same at sum157158-- Common determinant/combinatorial case: the pairing has no fixed points.159theorem finiteRingSum.involution_free (t : Set)160  requires finite : Finite(D)161  requires involution : InvolutionOn(t, D)162  requires opposite : ∀ a ∈ D, w(t(a)) = R[-w(a)]163  requires free : ∀ a ∈ D, t(a) ≠ a164  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = R[0]165proof166  have fixed : ∀ a ∈ D, t(a) = a → w(a) = R[0]167    intros a member same168    exfalso169    exact free with a, member, same170  exact finiteRingSum.involution with *171172end Sums173