Grace/Cumulus/Algebra/Ring/FiniteCombination.g17

Open in Workbench Download source

Imports

FiniteSum

Declarations

Source

1-- Generated ideals are finite sums of coefficient-generator products (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.FiniteCombination8import FiniteSum910def idealProducts (A mul G : Set) : Set :=11  {t ∈ A | ∃ a ∈ A, ∃ p ∈ G, t = call2(mul, a, p)}1213notation scoped idealProducts(R, G) => idealProducts(R.carrier, R.mul, G)1415def finiteIdealSums (A add zero mul G : Set) : Set :=16  {x ∈ A | ∃ xs, List(idealProducts(A, mul, G), xs) ∧ x = ringSum{idealProducts(A, mul, G)}(add, zero, xs)}1718theorem idealProducts.subset (A mul G : Set)19  shows idealProducts(A, mul, G) ⊆ A20proof21  simp2223section Rings24variable (A add zero neg mul one G : Set)25hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)26hypothesis bounded : G ⊆ A27notation ring R := (A, add, zero, neg, mul, one)2829theorem idealProducts.scale (a t : Set)30  requires ha : a ∈ A31  requires ht : t ∈ idealProducts(A, mul, G)32  shows a * t ∈ idealProducts(A, mul, G)33proof34  obtain ⟨tIn, b, hb, p, hp, shape⟩ := idealProducts.membership.forward with ht35  have ordinary := IsCommRing.ring with ring36  have pIn := bounded with p, hp37  have coefficient := IsRing.mul_closed with ordinary, ha, hb38  have product := IsRing.mul_closed with ordinary, ha, tIn39  have equation : a * t = (a * b) * p40    rw shape41    ring42  exact idealProducts.membership.backward with ⟨product, a * b, coefficient, p, hp, equation⟩4344theorem idealProducts.contains45  shows G ⊆ idealProducts(A, mul, G)46proof47  have ordinary := IsCommRing.ring with ring48  have monoid := IsRing.multiplicative with ordinary49  have oneIn := IsMonoid.unit_in_carrier with monoid50  intros p hp51  have pIn := bounded with p, hp52  have identity : p = 1 * p by ring53  exact idealProducts.membership.backward with ⟨pIn, one, oneIn, p, hp, identity⟩5455theorem finiteIdealSums.zero56  shows 0 ∈ finiteIdealSums(A, add, zero, mul, G)57proof58  have ordinary := IsCommRing.ring with ring59  have zeroIn := IsRing.zero_in_carrier with ordinary60  have nil : List(idealProducts(A, mul, G), []) by typecheck61  have value : zero = ringSum{idealProducts(A, mul, G)}(add, zero, [])62    rw ringSum63    rfl64  exact finiteIdealSums.membership.backward with ⟨zeroIn, [], nil, value⟩6566theorem finiteIdealSums.contains67  shows G ⊆ finiteIdealSums(A, add, zero, mul, G)68proof69  have products := idealProducts.contains with ring, bounded70  intros p hp71  have pIn := bounded with p, hp72  have product := products with p, hp73  have singleton : List(idealProducts(A, mul, G), [p]) by typecheck74  have value : p = ringSum{idealProducts(A, mul, G)}(add, zero, [p])75    rw [ringSum, ringSum]76    ring77  exact finiteIdealSums.membership.backward with ⟨pIn, [p], singleton, value⟩7879theorem finiteIdealSums.add (x y : Set)80  requires hx : x ∈ finiteIdealSums(A, add, zero, mul, G)81  requires hy : y ∈ finiteIdealSums(A, add, zero, mul, G)82  shows x + y ∈ finiteIdealSums(A, add, zero, mul, G)83proof84  obtain ⟨xIn, xs, listX, valueX⟩ := finiteIdealSums.membership.forward with hx85  obtain ⟨yIn, ys, listY, valueY⟩ := finiteIdealSums.membership.forward with hy86  have ordinary := IsCommRing.ring with ring87  have sumIn := IsRing.add_closed with ordinary, xIn, yIn88  have products := idealProducts.subset at A, mul, G89  have combined : List(idealProducts(A, mul, G), ListOps.append{idealProducts(A, mul, G)}(ys, xs)) by typecheck90  have value := ringSum.append at A, add, zero, neg, mul, one, idealProducts(A, mul, G), ys, xs with *91  have equation : x + y = ringSum{idealProducts(A, mul, G)}(add, zero, ListOps.append{idealProducts(A, mul, G)}(ys, xs))92    cc93  exact finiteIdealSums.membership.backward with ⟨sumIn, ListOps.append{idealProducts(A, mul, G)}(ys, xs), combined, equation⟩9495theorem finiteIdealSums.scale (a x : Set)96  requires ha : a ∈ A97  requires hx : x ∈ finiteIdealSums(A, add, zero, mul, G)98  shows a * x ∈ finiteIdealSums(A, add, zero, mul, G)99proof100  obtain ⟨xIn, xs, listX, valueX⟩ := finiteIdealSums.membership.forward with hx101  have ordinary := IsCommRing.ring with ring102  have productIn := IsRing.mul_closed with ordinary, ha, xIn103  have products := idealProducts.subset at A, mul, G104  have closed : ∀ t ∈ idealProducts(A, mul, G), a * t ∈ idealProducts(A, mul, G)105    intros t ht106    exact idealProducts.scale with ring, bounded, ha, ht107  have scaled := ringScale.closed with *108  have value := ringSum.scale at A, add, zero, neg, mul, one, idealProducts(A, mul, G), a, xs with *109  have equation : a * x = ringSum{idealProducts(A, mul, G)}(add, zero, ringScale{idealProducts(A, mul, G)}(mul, a, xs))110    cc111  exact finiteIdealSums.membership.backward with ⟨productIn, ringScale{idealProducts(A, mul, G)}(mul, a, xs), scaled, equation⟩112113theorem finiteIdealSums.ideal114  shows IsIdeal(A, add, zero, neg, mul, finiteIdealSums(A, add, zero, mul, G))115proof116  have ordinary := IsCommRing.ring with ring117  have monoid := IsRing.multiplicative with ordinary118  have oneIn := IsMonoid.unit_in_carrier with monoid119  have negOneIn := IsRing.neg_closed with ordinary, oneIn120  unfold IsIdeal121  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩122  . settle with Subset, finiteIdealSums.membership123  . exact finiteIdealSums.zero with ring, bounded124  . intros x hx y hy125    exact finiteIdealSums.add with ring, bounded, hx, hy126  . intros x hx127    have data := finiteIdealSums.membership.forward with hx128    have xIn := data.left129    have scaled := finiteIdealSums.scale with ring, bounded, negOneIn, hx130    have equation : -1 * x = -x by ring131    rwa equation at scaled132  . intros a ha x hx133    have data := finiteIdealSums.membership.forward with hx134    have xIn := data.left135    have scaled := finiteIdealSums.scale with ring, bounded, ha, hx136    have commute : x * a = a * x by ring137    constructor138    . exact scaled139    . rw commute140      exact scaled141142theorem idealProducts.subset_span143  shows idealProducts(A, mul, G) ⊆ idealSpan(A, add, zero, neg, mul, G)144proof145  have ideal := idealSpan.ideal at A, add, zero, neg, mul, one, G with ring146  have includes := idealSpan.contains at A, add, zero, neg, mul, G with bounded147  intros t ht148  obtain ⟨tIn, a, ha, p, hp, shape⟩ := idealProducts.membership.forward with ht149  have member := includes with p, hp150  have product := IsIdeal.mul_left_closed with ideal, ha, member151  rwa shape152153theorem idealSpan.eq_finite_sums154  shows idealSpan(A, add, zero, neg, mul, G) = finiteIdealSums(A, add, zero, mul, G)155proof156  have sumsIdeal := finiteIdealSums.ideal with ring, bounded157  have includes := finiteIdealSums.contains with ring, bounded158  have left := idealSpan.least with sumsIdeal, includes159  apply Subset.antisymmetric with left160  intros x hx161  obtain ⟨xIn, xs, listX, valueX⟩ := finiteIdealSums.membership.forward with hx162  have spanIdeal := idealSpan.ideal at A, add, zero, neg, mul, one, G with ring163  have products := idealProducts.subset_span with ring, bounded164  have sum := IsIdeal.sum_mem with *165  rwa valueX166167-- The number of summands is arbitrary: a witness is any finite list of products.168theorem idealSpan.finite_certificate (x : Set)169  shows x ∈ idealSpan(A, add, zero, neg, mul, G) ↔170    ∃ xs, List(idealProducts(A, mul, G), xs) ∧ x = ringSum{idealProducts(A, mul, G)}(add, zero, xs)171proof172  have representation := idealSpan.eq_finite_sums with ring, bounded173  constructor174  . intro member175    rw representation at member176    have data := finiteIdealSums.membership.forward with member177    exact data.right178  . intro certificate179    obtain ⟨xs, listX, valueX⟩ := certificate180    have products := idealProducts.subset at A, mul, G181    have sumIn := ringSum.closed with *182    have xIn : x ∈ A by cc183    rw representation184    exact finiteIdealSums.membership.backward with ⟨xIn, xs, listX, valueX⟩185186theorem idealSpan.unit_iff_finite_certificate187  shows 1 ∈ idealSpan(A, add, zero, neg, mul, G) ↔188    ∃ xs, List(idealProducts(A, mul, G), xs) ∧ 1 = ringSum{idealProducts(A, mul, G)}(add, zero, xs)189proof190  exact idealSpan.finite_certificate with ring, bounded191192section Evaluations193variable (f B plus z minus times unit : Set)194hypothesis target : IsCommRing(B, plus, z, minus, times, unit)195hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)196hypothesis nontrivial : Nontrivial(B, z, unit)197notation ring S := (B, plus, z, minus, times, unit)198199theorem idealSpan.finite_certificate_obstructs_vanishing (xs : List(idealProducts(A, mul, G)))200  requires identity : R[1] = ringSum{idealProducts(A, mul, G)}(add, zero, xs)201  shows ¬(∀ p ∈ G, f(p) = S[0])202proof203  have listX : List(idealProducts(A, mul, G), xs) by assumption204  have certificate : ∃ terms, List(idealProducts(A, mul, G), terms) ∧ one = ringSum{idealProducts(A, mul, G)}(add, zero, terms)205    refine ⟨xs, listX, identity⟩206  have unitIn := idealSpan.unit_iff_finite_certificate.backward with ring, bounded, certificate207  exact idealSpan.unit_obstructs_vanishing with ring, target, hom, nontrivial, bounded, unitIn208209end Evaluations210211end Rings212