Grace/Cumulus/Algebra/Ring/ProductExpansion.g17

Open in Workbench Download source

Imports

ProductSetSum · FiniteLinearity · Combinatorics.Functions

Declarations

Source

1-- A product of sums expands as a sum of products over the function space:2-- by induction on the index set, the product over m of the row sums of w3-- is the sum over the functions f : m → E of the products of the picked4-- entries w(i, f(i))5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.ProductExpansion11import ProductSetSum12import FiniteLinearity13import Combinatorics.Functions1415-- The entries w(i, f(i)) picked by a function f, and their product.16defgraph pickedWeights (D E A w f : Set) (i ∈ D) : A := w((i, f(i)))17requires matrix : w : D × E → A18requires function : f : D → E19proof20  have image := FunctionBetween.apply_closed with function, assumption21  have pair := product.pair at i, f(i), D, E with assumption, image22  exact FunctionBetween.apply_closed with matrix, pair2324defgraph functionProducts (D E A add zero neg mul one w : Set) (f ∈ functionSpace(D, E)) : A :=25  finiteRingProduct(D, A, add, zero, neg, mul, one, pickedWeights(D, E, A, w, f))26requires ring : IsCommRing(A, add, zero, neg, mul, one)27requires finite : Finite(D)28requires matrix : w : D × E → A29proof30  have function := functionSpace.mem_iff.forward with assumption31  have weights := pickedWeights.function at D, E, A, w, f with matrix, function32  exact finiteRingProduct.closed at D, A, add, zero, neg, mul, one,33    pickedWeights(D, E, A, w, f) with ring, finite, weights3435-- The weights on functionSpace(D, E) × E pairing a product over D with36-- one more entry from the row a.37defgraph expansionWeights (D E A add zero neg mul one w a : Set)38    (q ∈ functionSpace(D, E) × E) : A :=39  call2(mul, functionProducts(D, E, A, add, zero, neg, mul, one, restrict(w, D × E))(fst(q)),40    w((a, snd(q))))41requires ring : IsCommRing(A, add, zero, neg, mul, one)42requires finite : Finite(D)43requires matrix : w : insert(a, D) × E → A44proof45  obtain ⟨bound, g, hg, y, hy, shape⟩ := product.membership.forward with assumption46  have subset : D × E ⊆ insert(a, D) × E47    intros p hp48    obtain ⟨boundP, i, hi, z, hz, shapeP⟩ := product.membership.forward with hp49    rw shapeP50    exact product.pair with (insert.contains with hi), hz51  have restricted := restrict.domain_function at w, insert(a, D) × E, A, D × E with matrix, subset52  have products := functionProducts.function at D, E, A, add, zero, neg, mul, one,53    restrict(w, D × E) with ring, finite, restricted54  have selfA := insert.self at a, D55  have pair := product.pair at a, y, insert(a, D), E with selfA, hy56  have entry := FunctionBetween.apply_closed with matrix, pair57  have first : fst(q) = g58    rw shape59    exact fst.pair at g, y60  have second : snd(q) = y61    rw shape62    exact snd.pair at g, y63  rw [first, second]64  have product := FunctionBetween.apply_closed with products, hg65  have ordinary := IsCommRing.ring with ring66  exact IsRing.mul_closed with ordinary, product, entry6768-- The product over m of the row sums of w is the sum over the functions69-- m → E of the products of the picked entries w(i, f(i)).70theorem finiteRingProduct.row_sums (E A add zero neg mul one : Set) (m : Nat)71  requires ring : IsCommRing(A, add, zero, neg, mul, one)72  requires finiteE : Finite(E)73  shows ∀ w, (w : m × E → A) →74    finiteRingProduct(m, A, add, zero, neg, mul, one,75      finiteRowSums(m, E, A, add, zero, neg, mul, one, w)) =76    finiteRingSum(functionSpace(m, E), A, add, zero, neg, mul, one,77      functionProducts(m, E, A, add, zero, neg, mul, one, w))78proof79  induction m80  | zero =>81    intros w matrix82    rw nat.zero at matrix83    rw nat.zero84    have rows := finiteRowSums.function at ∅, E, A, add, zero, neg, mul, one, w85      with ring, finiteE, matrix86    have productEmpty := finiteRingProduct.empty at A, add, zero, neg, mul, one,87      finiteRowSums(∅, E, A, add, zero, neg, mul, one, w) with ring, rows88    have spaceEmpty := functionSpace.empty_domain at E89    have finiteEmpty := Finite.empty90    have products := functionProducts.function at ∅, E, A, add, zero, neg, mul, one, w91      with ring, finiteEmpty, matrix92    have emptyIn : ∅ ∈ functionSpace(∅, E)93      rw spaceEmpty94      exact singleton.self at ∅95    have value := functionProducts.value at ∅, E, A, add, zero, neg, mul, one, w, ∅96      with ring, finiteEmpty, matrix, emptyIn97    have emptyFunction := functionSpace.mem_iff.forward with emptyIn98    have pairedEmpty := pickedWeights.function at ∅, E, A, w, ∅ with matrix, emptyFunction99    have productPaired := finiteRingProduct.empty at A, add, zero, neg, mul, one,100      pickedWeights(∅, E, A, w, ∅) with ring, pairedEmpty101    rw spaceEmpty at products102    have single := finiteRingSum.singleton at A, add, zero, neg, mul, one,103      functionProducts(∅, E, A, add, zero, neg, mul, one, w), ∅ with ring, products104    rw [productEmpty, spaceEmpty, single, value, productPaired]105    rfl106  | succ(k) using ih =>107    intros w matrix108    have step : succ(k) = insert(k, k) := natural.successor_as_insert at k109    have fresh := membership.irreflexive at k110    have finiteK := Finite.natural at k111    have selfK := insert.self at k, k112    rw step at matrix113    rw step114    have subset : k × E ⊆ insert(k, k) × E115      intros p hp116      obtain ⟨bound, i, hi, z, hz, shape⟩ := product.membership.forward with hp117      rw shape118      exact product.pair with (insert.contains with hi), hz119    have subsetK : k ⊆ insert(k, k)120      intros x hx121      exact insert.contains with hx122    have restricted := restrict.domain_function at w, insert(k, k) × E, A, k × E123      with matrix, subset124    have inner := ih with restrict(w, k × E), restricted125    have rows := finiteRowSums.function at insert(k, k), E, A, add, zero, neg, mul, one, w126      with ring, finiteE, matrix127    have rowsK := finiteRowSums.function at k, E, A, add, zero, neg, mul, one,128      restrict(w, k × E) with ring, finiteE, restricted129    have splitProduct := finiteRingProduct.insert at k, A, add, zero, neg, mul, one,130      finiteRowSums(insert(k, k), E, A, add, zero, neg, mul, one, w), k131      with ring, finiteK, rows, fresh132    have restrictedRows := restrict.domain_function at133      finiteRowSums(insert(k, k), E, A, add, zero, neg, mul, one, w), insert(k, k), A, k134      with rows, subsetK135    have sameRows : ∀ i ∈ k,136        restrict(finiteRowSums(insert(k, k), E, A, add, zero, neg, mul, one, w), k)(i) =137        finiteRowSums(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))(i)138      intros i hi139      have iIn := subsetK with i, hi140      have restrictedValue := restrict.domain_apply at141        finiteRowSums(insert(k, k), E, A, add, zero, neg, mul, one, w), insert(k, k), A, k, i142        with rows, subsetK, hi143      have rowValue := finiteRowSums.value at insert(k, k), E, A, add, zero, neg, mul, one, w, i144        with ring, finiteE, matrix, iIn145      have rowValueK := finiteRowSums.value at k, E, A, add, zero, neg, mul, one,146        restrict(w, k × E), i with ring, finiteE, restricted, hi147      have weightsI := finiteRowWeights.function at insert(k, k), E, A, w, i with matrix, iIn148      have weightsIK := finiteRowWeights.function at k, E, A, restrict(w, k × E), i149        with restricted, hi150      have entries : ∀ y ∈ E, finiteRowWeights(insert(k, k), E, A, w, i)(y) =151          finiteRowWeights(k, E, A, restrict(w, k × E), i)(y)152        intros y hy153        have left := finiteRowWeights.value at insert(k, k), E, A, w, i, y with matrix, iIn, hy154        have right := finiteRowWeights.value at k, E, A, restrict(w, k × E), i, y155          with restricted, hi, hy156        have pair := product.pair at i, y, k, E with hi, hy157        have restrictedEntry := restrict.domain_apply at w, insert(k, k) × E, A, k × E, (i, y)158          with matrix, subset, pair159        rw [left, right, restrictedEntry]160        rfl161      have congruent := finiteRingSum.congr at E, A, add, zero, neg, mul, one,162        finiteRowWeights(insert(k, k), E, A, w, i), finiteRowWeights(k, E, A, restrict(w, k × E), i)163        with ring, finiteE, weightsI, weightsIK, entries164      rw [restrictedValue, rowValue, rowValueK, congruent]165      rfl166    have productCongr := finiteRingProduct.congr at k, A, add, zero, neg, mul, one,167      restrict(finiteRowSums(insert(k, k), E, A, add, zero, neg, mul, one, w), k),168      finiteRowSums(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))169      with ring, finiteK, restrictedRows, rowsK, sameRows170    have rowK := finiteRowSums.value at insert(k, k), E, A, add, zero, neg, mul, one, w, k171      with ring, finiteE, matrix, selfK172    have finiteInsert := Finite.insert at k, k with finiteK173    have products := functionProducts.function at insert(k, k), E, A, add, zero, neg, mul, one, w174      with ring, finiteInsert, matrix175    have split := functionSplit.bijective at k, E, k with fresh176    have splitFunction := functionSplit.function at k, E, k177    have weightsQ := expansionWeights.function at k, E, A, add, zero, neg, mul, one, w, k178      with ring, finiteK, matrix179    have productsK := functionProducts.function at k, E, A, add, zero, neg, mul, one,180      restrict(w, k × E) with ring, finiteK, restricted181    have termValues : ∀ F ∈ functionSpace(insert(k, k), E),182        functionProducts(insert(k, k), E, A, add, zero, neg, mul, one, w)(F) =183        expansionWeights(k, E, A, add, zero, neg, mul, one, w, k)(functionSplit(k, E, k)(F))184      intros F hF185      have fFunction := functionSpace.mem_iff.forward with hF186      have valueF := functionProducts.value at insert(k, k), E, A, add, zero, neg, mul, one, w, F187        with ring, finiteInsert, matrix, hF188      have splitValue := functionSplit.value at k, E, k, F with hF189      have splitIn := FunctionBetween.apply_closed with splitFunction, hF190      have qValue := expansionWeights.value at k, E, A, add, zero, neg, mul, one, w, k,191        functionSplit(k, E, k)(F) with ring, finiteK, matrix, splitIn192      have pairedF := pickedWeights.function at insert(k, k), E, A, w, F with matrix, fFunction193      have splitPaired := finiteRingProduct.insert at k, A, add, zero, neg, mul, one,194        pickedWeights(insert(k, k), E, A, w, F), k with ring, finiteK, pairedF, fresh195      have restrictedF := restrict.domain_function at F, insert(k, k), E, k with fFunction, subsetK196      have restrictedFIn : restrict(F, k) ∈ functionSpace(k, E) :=197        functionSpace.mem_iff.backward with restrictedF198      have innerValue := functionProducts.value at k, E, A, add, zero, neg, mul, one,199        restrict(w, k × E), restrict(F, k) with ring, finiteK, restricted, restrictedFIn200      have pairedRestricted := restrict.domain_function at201        pickedWeights(insert(k, k), E, A, w, F), insert(k, k), A, k with pairedF, subsetK202      have pairedK := pickedWeights.function at k, E, A, restrict(w, k × E), restrict(F, k)203        with restricted, restrictedF204      have samePaired : ∀ i ∈ k, restrict(pickedWeights(insert(k, k), E, A, w, F), k)(i) =205          pickedWeights(k, E, A, restrict(w, k × E), restrict(F, k))(i)206        intros i hi207        have iIn := subsetK with i, hi208        have left := restrict.domain_apply at pickedWeights(insert(k, k), E, A, w, F),209          insert(k, k), A, k, i with pairedF, subsetK, hi210        have leftValue := pickedWeights.value at insert(k, k), E, A, w, F, i211          with matrix, fFunction, iIn212        have rightValue := pickedWeights.value at k, E, A, restrict(w, k × E), restrict(F, k), i213          with restricted, restrictedF, hi214        have fValue := restrict.domain_apply at F, insert(k, k), E, k, i with fFunction, subsetK, hi215        have imageIn := FunctionBetween.apply_closed with fFunction, iIn216        have pair := product.pair at i, F(i), k, E with hi, imageIn217        have wValue := restrict.domain_apply at w, insert(k, k) × E, A, k × E, (i, F(i))218          with matrix, subset, pair219        rw [left, leftValue, rightValue, fValue, wValue]220        rfl221      have productCongrF := finiteRingProduct.congr at k, A, add, zero, neg, mul, one,222        restrict(pickedWeights(insert(k, k), E, A, w, F), k),223        pickedWeights(k, E, A, restrict(w, k × E), restrict(F, k))224        with ring, finiteK, pairedRestricted, pairedK, samePaired225      have lastValue := pickedWeights.value at insert(k, k), E, A, w, F, k226        with matrix, fFunction, selfK227      rw [valueF, qValue, splitValue, fst.pair, snd.pair, splitPaired, productCongrF,228        innerValue, lastValue]229      rfl230    have finiteSpace := functionSpace.finite at insert(k, k), E with finiteInsert, finiteE231    have finiteSpaceK := functionSpace.finite at k, E with finiteK, finiteE232    have reindexed := finiteRingSum.reindex at functionSpace(insert(k, k), E),233      functionSpace(k, E) × E, A, add, zero, neg, mul, one,234      functionProducts(insert(k, k), E, A, add, zero, neg, mul, one, w),235      expansionWeights(k, E, A, add, zero, neg, mul, one, w, k), functionSplit(k, E, k)236      with ring, finiteSpace, products, weightsQ, split, termValues237    have doubled := finiteRingSum.product_set at functionSpace(k, E), E, A, add, zero, neg, mul,238      one, expansionWeights(k, E, A, add, zero, neg, mul, one, w, k)239      with ring, finiteSpaceK, finiteE, weightsQ240    have rowSumsQ := finiteRowSums.function at functionSpace(k, E), E, A, add, zero, neg, mul, one,241      expansionWeights(k, E, A, add, zero, neg, mul, one, w, k) with ring, finiteE, weightsQ242    have rowWeightsK := finiteRowWeights.function at insert(k, k), E, A, w, k with matrix, selfK243    have totalIn := finiteRingSum.closed at E, A, add, zero, neg, mul, one,244      finiteRowWeights(insert(k, k), E, A, w, k) with ring, finiteE, rowWeightsK245    have commutative := IsCommRing.commutative with ring246    unfold Commutative at commutative247    have innerRows : ∀ g ∈ functionSpace(k, E),248        finiteRowSums(functionSpace(k, E), E, A, add, zero, neg, mul, one,249          expansionWeights(k, E, A, add, zero, neg, mul, one, w, k))(g) =250        call2(mul, finiteRingSum(E, A, add, zero, neg, mul, one,251          finiteRowWeights(insert(k, k), E, A, w, k)),252          functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))(g))253      intros g hg254      have rowValueQ := finiteRowSums.value at functionSpace(k, E), E, A, add, zero, neg, mul,255        one, expansionWeights(k, E, A, add, zero, neg, mul, one, w, k), g256        with ring, finiteE, weightsQ, hg257      have weightsG := finiteRowWeights.function at functionSpace(k, E), E, A,258        expansionWeights(k, E, A, add, zero, neg, mul, one, w, k), g with weightsQ, hg259      have pg := FunctionBetween.apply_closed with productsK, hg260      have scaledValues : ∀ y ∈ E, finiteRowWeights(functionSpace(k, E), E, A,261          expansionWeights(k, E, A, add, zero, neg, mul, one, w, k), g)(y) =262          call2(mul, functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))(g),263            finiteRowWeights(insert(k, k), E, A, w, k)(y))264        intros y hy265        have left := finiteRowWeights.value at functionSpace(k, E), E, A,266          expansionWeights(k, E, A, add, zero, neg, mul, one, w, k), g, y with weightsQ, hg, hy267        have pair := product.pair at g, y, functionSpace(k, E), E with hg, hy268        have qValue := expansionWeights.value at k, E, A, add, zero, neg, mul, one, w, k, (g, y)269          with ring, finiteK, matrix, pair270        have right := finiteRowWeights.value at insert(k, k), E, A, w, k, y with matrix, selfK, hy271        rw [left, qValue, fst.pair, snd.pair, right]272        rfl273      have scaled := finiteRingSum.scale_eq at E, A, add, zero, neg, mul, one,274        finiteRowWeights(insert(k, k), E, A, w, k),275        finiteRowWeights(functionSpace(k, E), E, A,276          expansionWeights(k, E, A, add, zero, neg, mul, one, w, k), g),277        functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))(g)278        with ring, finiteE, rowWeightsK, weightsG, pg, scaledValues279      have swap := commutative with280        functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))(g), pg,281        finiteRingSum(E, A, add, zero, neg, mul, one, finiteRowWeights(insert(k, k), E, A, w, k)),282        totalIn283      rw [rowValueQ, scaled, swap]284      rfl285    have outer := finiteRingSum.scale_eq at functionSpace(k, E), A, add, zero, neg, mul, one,286      functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E)),287      finiteRowSums(functionSpace(k, E), E, A, add, zero, neg, mul, one,288        expansionWeights(k, E, A, add, zero, neg, mul, one, w, k)),289      finiteRingSum(E, A, add, zero, neg, mul, one, finiteRowWeights(insert(k, k), E, A, w, k))290      with ring, finiteSpaceK, productsK, rowSumsQ, totalIn, innerRows291    have sumIn := finiteRingSum.closed at functionSpace(k, E), A, add, zero, neg, mul, one,292      functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))293      with ring, finiteSpaceK, productsK294    have swapOuter := commutative with295      finiteRingSum(functionSpace(k, E), A, add, zero, neg, mul, one,296        functionProducts(k, E, A, add, zero, neg, mul, one, restrict(w, k × E))), sumIn,297      finiteRingSum(E, A, add, zero, neg, mul, one, finiteRowWeights(insert(k, k), E, A, w, k)),298      totalIn299    unfold finiteDoubleSum at doubled300    rw [splitProduct, productCongr, inner, rowK, reindexed, doubled, outer, swapOuter]301    rfl302