Grace/Cumulus/Algebra/Ring/FiniteSum.g17

Open in Workbench Download source

Imports

GeneratedIdeal · Core.List

Declarations

• ringSum def
• ringImageSum def
• ringScale def
• ringScale.closed theorem derivation
• ringSum.nil theorem derivation
• ringSum.cons theorem derivation
• IsIdeal.sum_mem theorem derivation
• ringSum.closed theorem derivation
• ringSum.append theorem derivation
• ringSum.scale theorem derivation
• IsRingHom.sum theorem derivation

Source

1-- Finite sums over arbitrary set-sized rings and their ideals (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.FiniteSum8import GeneratedIdeal9import Core.List1011def ringSum {C : Set} (add z0 : Set) (xs : List(C)) → Set12  | add, z0, List.nil => z013  | add, z0, List.cons(x, tail) => call2(add, x, ringSum(add, z0, tail))14  descends xs1516def ringImageSum {C : Set} (f plus z : Set) (xs : List(C)) → Set17  | f, plus, z, List.nil => z18  | f, plus, z, List.cons(x, tail) => plus(f(x), ringImageSum(f, plus, z, tail))19  descends xs2021def ringScale {C : Set} (mul a : Set) (xs : List(C)) → Set22  | mul, a, List.nil => []23  | mul, a, List.cons(x, tail) => call2(mul, a, x) :: ringScale(mul, a, tail)24  descends xs2526theorem ringScale.closed (C mul a : Set) (xs : List(C))27  requires closed : ∀ x ∈ C, call2(mul, a, x) ∈ C28  shows List(C, ringScale{C}(mul, a, xs))29proof30  induction xs31  | List.nil =>32    rw ringScale33    typecheck34  | List.cons(x, tail) using ih =>35    have member := closed with x36    rw ringScale37    typecheck3839theorem ringSum.nil (C add zero : Set)40  shows ringSum{C}(add, zero, []) = zero41proof42  unfold ringSum43  rfl4445theorem ringSum.cons (C add zero x : Set) (xs : List(C))46  requires member : x ∈ C47  shows ringSum{C}(add, zero, x :: xs) = call2(add, x, ringSum{C}(add, zero, xs))48proof49  unfold ringSum50  rfl5152theorem IsIdeal.sum_mem (A add zero neg mul I C : Set) (xs : List(C))53  requires ideal : IsIdeal(A, add, zero, neg, mul, I)54  requires included : C ⊆ I55  shows ringSum{C}(add, zero, xs) ∈ I56proof57  induction xs58  | List.nil =>59    rw ringSum60    exact IsIdeal.zero_closed with ideal61  | List.cons(x, tail) using ih =>62    have member := included with x, assumption63    have sum := IsIdeal.add_closed with ideal, member, ih64    rwa ringSum6566section Rings67variable (A add zero neg mul one C : Set)68hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)69hypothesis bounded : C ⊆ A70notation ring R := (A, add, zero, neg, mul, one)7172theorem ringSum.closed (xs : List(C))73  shows ringSum{C}(add, zero, xs) ∈ A74proof75  induction xs76  | List.nil =>77    have ordinary := IsCommRing.ring with ring78    rw ringSum79    exact IsRing.zero_in_carrier with ordinary80  | List.cons(x, tail) using ih =>81    have ordinary := IsCommRing.ring with ring82    have member := bounded with x, assumption83    have sum := IsRing.add_closed with ordinary, member, ih84    rwa ringSum8586theorem ringSum.append (ys xs : List(C))87  shows ringSum{C}(add, zero, ListOps.append{C}(ys, xs)) =88    ringSum{C}(add, zero, xs) + ringSum{C}(add, zero, ys)89proof90  induction xs91  | List.nil =>92    have sumY := ringSum.closed at A, add, zero, neg, mul, one, C, ys with *93    simp [ListOps.append, ringSum]94    ring95  | List.cons(x, tail) using ih =>96    have sumY := ringSum.closed at A, add, zero, neg, mul, one, C, ys with *97    have sumTail := ringSum.closed at A, add, zero, neg, mul, one, C, tail with *98    have member := bounded with x, assumption99    simp [ListOps.append, ringSum, ih]100    ring101102theorem ringSum.scale (a : Set) (xs : List(C))103  requires ha : a ∈ A104  requires closed : ∀ x ∈ C, a * x ∈ C105  shows ringSum{C}(add, zero, ringScale{C}(mul, a, xs)) = a * ringSum{C}(add, zero, xs)106proof107  induction xs108  | List.nil =>109    rw [ringScale, ringSum]110    ring111  | List.cons(x, tail) using ih =>112    have sumTail := ringSum.closed at A, add, zero, neg, mul, one, C, tail with *113    have scaledHead := closed with x114    have member := bounded with x, assumption115    rw [ringScale, ringSum, ringSum, ih]116    ring117118section Maps119variable (f B plus z minus times unit : Set)120hypothesis target : IsCommRing(B, plus, z, minus, times, unit)121hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)122notation ring S := (B, plus, z, minus, times, unit)123124theorem IsRingHom.sum (xs : List(C))125  shows f(ringSum{C}(add, zero, xs)) = ringImageSum{C}(f, plus, z, xs)126proof127  induction xs128  | List.nil =>129    rw [ringSum, ringImageSum]130    exact IsRingHom.zero with hom131  | List.cons(x, tail) using ih =>132    have sumTail := ringSum.closed at A, add, zero, neg, mul, one, C, tail with *133    have member := bounded with x, assumption134    have mapped := IsRingHom.add with hom, member, sumTail135    rw [ringSum, ringImageSum, mapped, ih]136    rfl137138end Maps139end Rings140