Grace/Cumulus/Algebra/IndexedCombinations.g17

Open in Workbench Download source

Imports

SpanCoefficients · IndexedLists · Ring.FiniteSetSum

Declarations

Source

1-- List linear combinations as sums over their finite ordinal of positions (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.IndexedCombinations8import SpanCoefficients9import IndexedLists10import Ring.FiniteSetSum1112section Sums13variable (A add zero neg mul one w v f g : Set)14notation ring R := (A, add, zero, neg, mul, one)15hypothesis ring : IsCommRing(R)16hypothesis first : w(f(∅)) ∈ R1718theorem indexedRingSum.head_tail (n : Nat)19  shows WeightedValues(w, f, A, succ(n)) → WeightedValues(v, g, A, n) →20    (∀ i ∈ n, w(f(succ(i))) = v(g(i))) →21    indexedRingSum(w, f, add, zero, succ(n)) = R[w(f(∅)) + indexedRingSum(v, g, add, zero, n)]22proof23  induction n24  | zero =>25    intros valuesW valuesV entries26    have headIn : w(f(∅)) ∈ A by exact first27    rw [indexedRingSum, indexedRingSum, indexedRingSum, nat.zero]28    ring29  | succ(k) using ih =>30    intros valuesW valuesV entries31    have prefixW := WeightedValues.prefix at w, f, A, succ(k) with *32    have prefixV := WeightedValues.prefix at v, g, A, k with *33    have lastW := WeightedValues.last at w, f, A, succ(k) with *34    have lastV := WeightedValues.last at v, g, A, k with *35    have prefix : ∀ i ∈ k, w(f(succ(i))) = v(g(i))36      intros i hi37      have included := membership.into_successor at i, k with *38      exact entries with i, included39    have previous := ih with prefixW, prefixV, prefix40    have last := entries with k, membership.self_successor at k with *41    have closed := indexedRingSum.closed at A, add, zero, neg, mul, one, v, g, k with *42    have sumIn := closed with prefixV43    rw [indexedRingSum, previous, indexedRingSum, last]44    ring4546end Sums474849defgraph combinationWeights (A a0 B b0 times f xs cs : Set) (i ∈ length{B}(xs)) : B := times(f(listCoefficient{A}(a0, cs, i)), listCoefficient{B}(b0, xs, i))50requires listX : List(B, xs)51requires listC : List(A, cs)52requires zeroA : a0 ∈ A53requires zeroB : b0 ∈ B54requires function : f : A → B55requires closed : ClosedBinary(B, times)56proof57  have size : Nat(length{B}(xs))58    typecheck59  have positions := natural.member at length{B}(xs) with size60  have index := positions with i, assumption61  have coefficient := listCoefficient.closed at A, a0, cs, i with *62  have generator := listCoefficient.closed at B, b0, xs, i with *63  have image := FunctionBetween.apply_closed with function, coefficient64  exact ClosedBinary.mem with closed, image, generator6566section Algebras67variable (A add zero neg mul one B plus z minus times unit f : Set)68notation ring R := (A, add, zero, neg, mul, one)69notation ring S := (B, plus, z, minus, times, unit)70hypothesis source : IsCommRing(R)71hypothesis target : IsCommRing(S)72hypothesis hom : IsRingHom(f, R, S)7374theorem linearCombination.indexed_sum (xs : List(B)) (cs : List(A))75  shows linearCombination(R, S, f, xs, cs) = indexedRingSum(combinationWeights(A, zero, B, z, times, f, xs, cs), identity(length{B}(xs)), plus, z, length{B}(xs))76proof77  induction xs generalizing cs78  | List.nil =>79    intros cs coefficients80    rw [linearCombination, length.nil, indexedRingSum]81    rfl82  | List.cons(a, tail) using ih =>83    intros cs coefficients84    have element : a ∈ B by assumption85    have ordinaryR := IsCommRing.ring with source86    have ordinaryS := IsCommRing.ring with target87    have zeroR := IsRing.zero_in_carrier with ordinaryR88    have zeroS := IsRing.zero_in_carrier with ordinaryS89    have function := IsRingHom.function with hom90    have closed : ClosedBinary(B, times)91      intros u hu v hv92      exact IsRing.mul_closed with ordinaryS, hu, hv93    have restList := listTail.closed at A, cs with *94    have nNat : Nat(length{B}(tail)) by typecheck95    have size : length{B}(a :: tail) = succ(length{B}(tail))96      rw length.cons97      rfl98    have weights := combinationWeights.function at A, zero, B, z, times, f, a :: tail, cs with *99    have tails := combinationWeights.function at A, zero, B, z, times, f, tail, listTail{A}(cs) with *100    have enum := identity.function at length{B}(a :: tail)101    have tailEnum := identity.function at length{B}(tail)102    have values := WeightedValues.of_functions with weights, enum103    have restValues := WeightedValues.of_functions with tails, tailEnum104    have firstIndex : ∅ ∈ length{B}(a :: tail)105      rw size106      have positive : 0 < succ(length{B}(tail)) by arith107      have included := membership.of_Less with Naturals.constructor.zero, positive108      rwa nat.zero at included109    have firstEnum := identity.apply with firstIndex110    have firstValue := combinationWeights.value at A, zero, B, z, times, f, a :: tail, cs, ∅ with *111    have firstIn : combinationWeights(A, zero, B, z, times, f, a :: tail, cs)(identity(length{B}(a :: tail))(∅)) ∈ B112      rw firstEnum113      exact FunctionBetween.apply_closed with weights, firstIndex114    have entries : ∀ i ∈ length{B}(tail), combinationWeights(A, zero, B, z, times, f, a :: tail, cs)(identity(length{B}(a :: tail))(succ(i))) = combinationWeights(A, zero, B, z, times, f, tail, listTail{A}(cs))(identity(length{B}(tail))(i))115      intros i hi116      have positions := natural.member with nNat117      have index := positions with i, hi118      have boundRule := Less.of_membership at i, length{B}(tail) with *119      have bound := boundRule with hi120      have nextBound : succ(i) < succ(length{B}(tail)) by arith121      have included : succ(i) ∈ length{B}(a :: tail)122        rw size123        exact membership.of_Less with nextBound124      have leftEnum := identity.apply with included125      have rightEnum := identity.apply with hi126      have left := combinationWeights.value at A, zero, B, z, times, f, a :: tail, cs, succ(i) with *127      have right := combinationWeights.value at A, zero, B, z, times, f, tail, listTail{A}(cs), i with *128      rw [leftEnum, rightEnum, left, right, listCoefficient.succ, listCoefficient]129      rfl130    have valuesNext : WeightedValues(combinationWeights(A, zero, B, z, times, f, a :: tail, cs), identity(length{B}(a :: tail)), B, succ(length{B}(tail)))131      rwa ← size132    have shiftRule := indexedRingSum.head_tail at B, plus, z, minus, times, unit, combinationWeights(A, zero, B, z, times, f, a :: tail, cs), combinationWeights(A, zero, B, z, times, f, tail, listTail{A}(cs)), identity(length{B}(a :: tail)), identity(length{B}(tail)), length{B}(tail) with *133    have shift := shiftRule with valuesNext, restValues, entries134    have previous := ih with listTail{A}(cs)135    rw [firstEnum, firstValue, ← nat.zero, listCoefficient.zero, listCoefficient, ← size] at shift136    rw [shift, ← previous, linearCombination]137    rfl138139theorem linearCombination.finite_sum (xs : List(B)) (cs : List(A)) (w : Set)140  requires weights : w : length{B}(xs) → B141  requires entries : ∀ i ∈ length{B}(xs), w(i) = S[f(listCoefficient{A}(zero, cs, i)) * listCoefficient{B}(z, xs, i)]142  shows linearCombination(R, S, f, xs, cs) = finiteRingSum(length{B}(xs), S, w)143proof144  have ordinaryR := IsCommRing.ring with source145  have ordinaryS := IsCommRing.ring with target146  have zeroR := IsRing.zero_in_carrier with ordinaryR147  have zeroS := IsRing.zero_in_carrier with ordinaryS148  have function := IsRingHom.function with hom149  have closed : ClosedBinary(B, times)150    intros u hu v hv151    exact IsRing.mul_closed with ordinaryS, hu, hv152  have canonical := combinationWeights.function at A, zero, B, z, times, f, xs, cs with *153  have enumeration := identity.bijective at length{B}(xs)154  have same : ∀ i ∈ length{B}(xs), combinationWeights(A, zero, B, z, times, f, xs, cs)(i) = w(i)155    intros i hi156    have value := combinationWeights.value at A, zero, B, z, times, f, xs, cs, i with *157    have specified := entries with i, hi158    cc159  have sums := finiteRingSum.congr with *160  have enumerated := finiteRingSum.enumeration at length{B}(xs), B, plus, z, minus, times, unit, combinationWeights(A, zero, B, z, times, f, xs, cs), identity(length{B}(xs)), length{B}(xs) with *161  have indexed := linearCombination.indexed_sum with *162  cc163164end Algebras165