Grace/Cumulus/Algebra/Ring/ProductSetSum.g17

Imports

Declarations

finiteRingSum.product_set theorem derivation
Source

1-- The sum over a product set is the double sum: push forward along the2-- first projection, and each fibre {x} × Y is a copy of Y3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Ring.ProductSetSum9import Regrouping10import FiniteDoubleSum1112theorem finiteRingSum.product_set (X Y A add zero neg mul one u : Set)13  requires ring : IsCommRing(A, add, zero, neg, mul, one)14  requires finiteX : Finite(X)15  requires finiteY : Finite(Y)16  requires matrix : u : X × Y → A17  shows finiteRingSum(X × Y, A, add, zero, neg, mul, one, u) =18    finiteDoubleSum(X, Y, A, add, zero, neg, mul, one, u)19proof20  have finiteXY := Finite.product with finiteX, finiteY21  have projection := firstProjection.function at X, Y22  have ordinary := IsCommRing.ring with ring23  have zeroIn : zero ∈ A := IsRing.zero_in_carrier with ordinary24  have push := finitePushforward.sum at X × Y, X, A, add, zero, neg, mul, one,25    firstProjection(X, Y), u with ring, matrix, finiteXY, finiteX, projection26  have pushFunction := finitePushforward.function at X × Y, X, A, add, zero, neg, mul, one,27    firstProjection(X, Y), u with ring, finiteXY, matrix28  have rows := finiteRowSums.function at X, Y, A, add, zero, neg, mul, one, u29    with ring, finiteY, matrix30  have values : ∀ x ∈ X,31      finitePushforward(X × Y, X, A, add, zero, neg, mul, one, firstProjection(X, Y), u)(x) =32      finiteRowSums(X, Y, A, add, zero, neg, mul, one, u)(x)33    intros x hx34    have pushValue := finitePushforward.value at X × Y, X, A, add, zero, neg, mul, one,35      firstProjection(X, Y), u, x with ring, finiteXY, matrix, hx36    have rowValue := finiteRowSums.value at X, Y, A, add, zero, neg, mul, one, u, x37      with ring, finiteY, matrix, hx38    have pushWeights := pushforwardWeights.function at X × Y, A, add, zero, neg, mul, one,39      firstProjection(X, Y), u, x with ring, matrix40    have rowWeights := finiteRowWeights.function at X, Y, A, u, x with matrix, hx41    have fibreSubset : {x} × Y ⊆ X × Y42      intros p hp43      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp44      have aIs := singleton.membership.forward with ha45      rw [shape, aIs]46      exact product.pair with hx, hy47    have fibreWeights := restrict.domain_function at u, X × Y, A, {x} × Y with matrix, fibreSubset48    have agreement : ∀ p ∈ {x} × Y,49        pushforwardWeights(X × Y, A, add, zero, neg, mul, one, firstProjection(X, Y), u, x)(p) =50        restrict(u, {x} × Y)(p)51      intros p hp52      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp53      have aIs := singleton.membership.forward with ha54      have inXY := fibreSubset with p, hp55      have weight := pushforwardWeights.value at X × Y, A, add, zero, neg, mul, one,56        firstProjection(X, Y), u, x, p with ring, matrix, inXY57      have restricted := restrict.domain_apply at u, X × Y, A, {x} × Y, p58        with matrix, fibreSubset, hp59      have first : firstProjection(X, Y)(p) = x60        rw [shape, aIs]61        exact firstProjection.pair at X, Y, x, y with hx, hy62      have coefficient := FunctionBetween.apply_closed with matrix, inXY63      symm at first64      have same := singleValue.same at A, zero, u(p), firstProjection(X, Y)(p), x65        with zeroIn, coefficient, first66      rw [weight, restricted, same]67      rfl68    have vanishing : ∀ p ∈ X × Y, ¬(p ∈ {x} × Y) →69        pushforwardWeights(X × Y, A, add, zero, neg, mul, one, firstProjection(X, Y), u, x)(p) =70        zero71      intros p hp outside72      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp73      have weight := pushforwardWeights.value at X × Y, A, add, zero, neg, mul, one,74        firstProjection(X, Y), u, x, p with ring, matrix, hp75      have first : firstProjection(X, Y)(p) = a76        rw shape77        exact firstProjection.pair at X, Y, a, y with ha, hy78      have different : x ≠ firstProjection(X, Y)(p)79        intro equal80        rw [first] at equal81        have inFibre : p ∈ {x} × Y82          rw [shape, equal]83          exact product.pair with (singleton.self at a), hy84        exact outside with inFibre85      have coefficient := FunctionBetween.apply_closed with matrix, hp86      have other := singleValue.other at A, zero, u(p), firstProjection(X, Y)(p), x87        with zeroIn, coefficient, different88      rw [weight, other]89      rfl90    have fibreSum := finiteRingSum.zero_extension at X × Y, {x} × Y, A, add, zero, neg, mul, one,91      pushforwardWeights(X × Y, A, add, zero, neg, mul, one, firstProjection(X, Y), u, x),92      restrict(u, {x} × Y) with ring, finiteXY, pushWeights, fibreWeights, fibreSubset,93      agreement, vanishing94    have finiteFibre := Finite.subset with finiteXY, fibreSubset95    have copy := secondProjection.bijective_singleton at x, Y96    have copyValues : ∀ p ∈ {x} × Y, restrict(u, {x} × Y)(p) =97        finiteRowWeights(X, Y, A, u, x)(secondProjection({x}, Y)(p))98      intros p hp99      obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp100      have aIs := singleton.membership.forward with ha101      have restricted := restrict.domain_apply at u, X × Y, A, {x} × Y, p102        with matrix, fibreSubset, hp103      have second : secondProjection({x}, Y)(p) = y104        rw shape105        exact secondProjection.pair at {x}, Y, a, y with ha, hy106      have rowWeight := finiteRowWeights.value at X, Y, A, u, x, y with matrix, hx, hy107      rw [restricted, second, rowWeight, shape, aIs]108      rfl109    have reindexed := finiteRingSum.reindex at {x} × Y, Y, A, add, zero, neg, mul, one,110      restrict(u, {x} × Y), finiteRowWeights(X, Y, A, u, x), secondProjection({x}, Y)111      with ring, finiteFibre, fibreWeights, rowWeights, copy, copyValues112    rw [pushValue, rowValue, fibreSum, reindexed]113    rfl114  have congruent := finiteRingSum.congr at X, A, add, zero, neg, mul, one,115    finitePushforward(X × Y, X, A, add, zero, neg, mul, one, firstProjection(X, Y), u),116    finiteRowSums(X, Y, A, add, zero, neg, mul, one, u)117    with ring, finiteX, pushFunction, rows, values118  unfold finiteDoubleSum119  rw [← push, congruent]120  rfl121