Grace/Cumulus/Algebra/Ring/FiniteLinearity.g17

Open in Workbench Download source

Imports

FiniteProduct

Declarations

Source

1-- Pointwise linearity for finite products and sums over commutative rings (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.FiniteLinearity8import FiniteProduct910section Rings11variable (V A add zero neg mul one : Set)12notation ring R := (A, add, zero, neg, mul, one)13hypothesis ring : IsCommRing(R)14hypothesis finite : Finite(V)1516theorem finiteRingProduct.remove (w i : Set)17  requires weights : w : V → A18  requires member : i ∈ V19  shows finiteRingProduct(V, R, w) = finiteRingProduct(V ∖ {i}, R, restrict(w, V ∖ {i})) * w(i)20proof21  have subset : V ∖ {i} ⊆ V by simp [Subset, difference.membership]22  have smaller := Finite.subset with finite, subset23  have fresh : ¬(i ∈ V ∖ {i}) by simp [difference.membership, singleton.membership]24  have restore := insert.restore with member25  have expanded : w : insert(i, V ∖ {i}) → A by rwa restore26  have equation := finiteRingProduct.insert with *27  rwa restore at equation2829-- Only the distinguished factor varies. Callers supply pointwise equations,30-- without constructing graphs for their sums or scalar multiples.31theorem finiteRingProduct.linear_at (w v h i a b : Set)32  requires weightsW : w : V → A33  requires weightsV : v : V → A34  requires weightsH : h : V → A35  requires member : i ∈ V36  requires scalarA : a ∈ A37  requires scalarB : b ∈ A38  requires outsideV : ∀ j ∈ V, ¬(j = i) → v(j) = w(j)39  requires outsideH : ∀ j ∈ V, ¬(j = i) → h(j) = w(j)40  requires entry : h(i) = a * w(i) + b * v(i)41  shows finiteRingProduct(V, R, h) = a * finiteRingProduct(V, R, w) + b * finiteRingProduct(V, R, v)42proof43  have subset : V ∖ {i} ⊆ V by simp [Subset, difference.membership]44  have smaller := Finite.subset with finite, subset45  have restrictedW := restrict.domain_function at w, V, A, V ∖ {i} with *46  have restrictedV := restrict.domain_function at v, V, A, V ∖ {i} with *47  have restrictedH := restrict.domain_function at h, V, A, V ∖ {i} with *48  have sameV : ∀ j ∈ V ∖ {i}, restrict(v, V ∖ {i})(j) = restrict(w, V ∖ {i})(j)49    intros j hj50    have inV : j ∈ V by simp [difference.membership]51    have distinct : ¬(j = i) by simp [difference.membership, singleton.membership]52    have leftValue := restrict.domain_apply at v, V, A, V ∖ {i}, j with *53    have rightValue := restrict.domain_apply at w, V, A, V ∖ {i}, j with *54    rw [leftValue, rightValue]55    exact outsideV with j, inV, distinct56  have equalV := finiteRingProduct.congr with *57  have sameH : ∀ j ∈ V ∖ {i}, restrict(h, V ∖ {i})(j) = restrict(w, V ∖ {i})(j)58    intros j hj59    have inV : j ∈ V by simp [difference.membership]60    have distinct : ¬(j = i) by simp [difference.membership, singleton.membership]61    have leftValue := restrict.domain_apply at h, V, A, V ∖ {i}, j with *62    have rightValue := restrict.domain_apply at w, V, A, V ∖ {i}, j with *63    rw [leftValue, rightValue]64    exact outsideH with j, inV, distinct65  have equalH := finiteRingProduct.congr at V ∖ {i}, A, add, zero, neg, mul, one, restrict(h, V ∖ {i}), restrict(w, V ∖ {i}) with *66  have equationW := finiteRingProduct.remove at V, A, add, zero, neg, mul, one, w, i with *67  have equationV := finiteRingProduct.remove at V, A, add, zero, neg, mul, one, v, i with *68  have equationH := finiteRingProduct.remove at V, A, add, zero, neg, mul, one, h, i with *69  have rest := finiteRingProduct.closed at V ∖ {i}, A, add, zero, neg, mul, one, restrict(w, V ∖ {i}) with *70  have valueW := FunctionBetween.apply_closed at w, V, A, i with *71  have valueV := FunctionBetween.apply_closed at v, V, A, i with *72  rw [equationH, equationW, equationV, equalH, equalV, entry]73  ring7475theorem finiteRingSum.linear (w v h a b : Set)76  requires weightsW : w : V → A77  requires weightsV : v : V → A78  requires weightsH : h : V → A79  requires scalarA : a ∈ A80  requires scalarB : b ∈ A81  requires entries : ∀ i ∈ V, h(i) = a * w(i) + b * v(i)82  shows finiteRingSum(V, R, h) = a * finiteRingSum(V, R, w) + b * finiteRingSum(V, R, v)83proof84  have scaledW := coefficientScale.function at V, A, add, zero, neg, mul, one, a, w with *85  have scaledV := coefficientScale.function at V, A, add, zero, neg, mul, one, b, v with *86  have combined := coefficientAdd.function at V, A, add, zero, neg, mul, one, coefficientScale(V, R, a, w), coefficientScale(V, R, b, v) with *87  have equations : ∀ i ∈ V, h(i) = coefficientAdd(V, R, coefficientScale(V, R, a, w), coefficientScale(V, R, b, v))(i)88    intros i hi89    have sum := coefficientAdd.value at V, A, add, zero, neg, mul, one, coefficientScale(V, R, a, w), coefficientScale(V, R, b, v), i with *90    have leftValue := coefficientScale.value at V, A, add, zero, neg, mul, one, a, w, i with *91    have rightValue := coefficientScale.value at V, A, add, zero, neg, mul, one, b, v, i with *92    rw [sum, leftValue, rightValue]93    exact entries with i, hi94  have equal := finiteRingSum.congr with *95  have sum := finiteRingSum.add at V, A, add, zero, neg, mul, one, coefficientScale(V, R, a, w), coefficientScale(V, R, b, v) with *96  have leftSum := finiteRingSum.scale at V, A, add, zero, neg, mul, one, w, a with *97  have rightSum := finiteRingSum.scale at V, A, add, zero, neg, mul, one, v, b with *98  rw [equal, sum, leftSum, rightSum]99  rfl100101-- Pointwise scaling avoids an auxiliary coefficientScale graph at call sites.102theorem finiteRingSum.scale_eq (w v a : Set)103  requires weightsW : w : V → A104  requires weightsV : v : V → A105  requires scalar : a ∈ R106  requires entries : ∀ i ∈ V, v(i) = a * w(i)107  shows finiteRingSum(V, R, v) = a * finiteRingSum(V, R, w)108proof109  have zeroIn : R[0] ∈ R by typecheck110  have linear : ∀ i ∈ V, v(i) = a * w(i) + R[0] * w(i)111    intros i hi112    have closed := FunctionBetween.apply_closed at w, V, A, i with *113    have entry := entries with i, hi114    rw entry115    ring116  have equation := finiteRingSum.linear with *117  have closed := finiteRingSum.closed at V, A, add, zero, neg, mul, one, w with *118  rw equation119  ring120121end Rings122