Grace/Cumulus/Algebra/Ring/GeneratedIdeal.g17

Open in Workbench Download source

Imports

Homomorphism

Declarations

Source

1-- Ideals generated by arbitrary sets and soundness of unit certificates (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.GeneratedIdeal8import Homomorphism910-- The bounded intersection of all ambient ideals containing the generators.11def idealSpan (A add zero neg mul G : Set) : Set :=12  {x ∈ A | ∀ J, IsIdeal(A, add, zero, neg, mul, J) → G ⊆ J → x ∈ J}1314notation scoped idealSpan(R, G) => idealSpan(R.carrier, R.add, R.zero, R.neg, R.mul, G)1516theorem idealSpan.subset (A add zero neg mul G : Set)17  shows idealSpan(A, add, zero, neg, mul, G) ⊆ A18proof19  simp2021theorem idealSpan.contains (A add zero neg mul G : Set)22  requires bounded : G ⊆ A23  shows G ⊆ idealSpan(A, add, zero, neg, mul, G)24proof25  intros x hx26  apply idealSpan.membership.backward27  refine ⟨?_, ?_⟩28  . exact bounded with x, hx29  . intros J ideal includes30    exact includes with x, hx3132theorem idealSpan.least (A add zero neg mul G J : Set)33  requires ideal : IsIdeal(A, add, zero, neg, mul, J)34  requires includes : G ⊆ J35  shows idealSpan(A, add, zero, neg, mul, G) ⊆ J36proof37  intros x hx38  have data := idealSpan.membership.forward with hx39  exact data.right with J, ideal, includes4041section Ring42variable (A add zero neg mul one : Set)43hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)44notation ring R := (A, add, zero, neg, mul, one)4546theorem idealSpan.ideal (G : Set)47  shows IsIdeal(A, add, zero, neg, mul, idealSpan(A, add, zero, neg, mul, G))48proof49  have ordinary := IsCommRing.ring with ring50  have zeroIn := IsRing.zero_in_carrier with ordinary51  have bounded := idealSpan.subset at A, add, zero, neg, mul, G52  unfold IsIdeal53  refine ⟨bounded, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩54  . apply idealSpan.membership.backward at A, add, zero, neg, mul, G, zero55    refine ⟨zeroIn, ?_⟩56    intros J ideal includes57    exact IsIdeal.zero_closed with ideal58  . intros x hx y hy59    have dx := idealSpan.membership.forward with hx60    have dy := idealSpan.membership.forward with hy61    have closed := IsRing.add_closed with ordinary, dx.left, dy.left62    apply idealSpan.membership.backward63    refine ⟨closed, ?_⟩64    intros J ideal includes65    have xIn := dx.right with J, ideal, includes66    have yIn := dy.right with J, ideal, includes67    exact IsIdeal.add_closed with ideal, xIn, yIn68  . intros x hx69    have data := idealSpan.membership.forward with hx70    have closed := IsRing.neg_closed with ordinary, data.left71    apply idealSpan.membership.backward72    refine ⟨closed, ?_⟩73    intros J ideal includes74    have member := data.right with J, ideal, includes75    exact IsIdeal.neg_closed with ideal, member76  . intros a ha x hx77    have data := idealSpan.membership.forward with hx78    have leftClosed := IsRing.mul_closed with ordinary, ha, data.left79    have rightClosed := IsRing.mul_closed with ordinary, data.left, ha80    constructor81    . apply idealSpan.membership.backward at A, add, zero, neg, mul, G, a * x82      refine ⟨leftClosed, ?_⟩83      intros J ideal includes84      have member := data.right with J, ideal, includes85      exact IsIdeal.mul_left_closed with ideal, ha, member86    . apply idealSpan.membership.backward at A, add, zero, neg, mul, G, x * a87      refine ⟨rightClosed, ?_⟩88      intros K idealK includesK89      have memberK := data.right with K, idealK, includesK90      exact IsIdeal.mul_right_closed with idealK, ha, memberK9192theorem idealSpan.mono (G H : Set)93  requires inclusion : G ⊆ H94  requires bounded : H ⊆ A95  shows idealSpan(A, add, zero, neg, mul, G) ⊆ idealSpan(A, add, zero, neg, mul, H)96proof97  have ideal := idealSpan.ideal at A, add, zero, neg, mul, one, H with ring98  have includes := idealSpan.contains at A, add, zero, neg, mul, H with bounded99  have generators := Subset.transitive with inclusion, includes100  exact idealSpan.least with ideal, generators101102theorem idealSpan.eq_of_ideal (J : Set)103  requires ideal : IsIdeal(A, add, zero, neg, mul, J)104  shows idealSpan(A, add, zero, neg, mul, J) = J105proof106  have bounded := IsIdeal.subset_carrier with ideal107  have reflexive : J ⊆ J by simp [Subset]108  have left := idealSpan.least with ideal, reflexive109  have right := idealSpan.contains at A, add, zero, neg, mul, J with bounded110  exact Subset.antisymmetric with left, right111112theorem idealSpan.idempotent (G : Set)113  shows idealSpan(A, add, zero, neg, mul, idealSpan(A, add, zero, neg, mul, G)) = idealSpan(A, add, zero, neg, mul, G)114proof115  have ideal := idealSpan.ideal at A, add, zero, neg, mul, one, G with ring116  exact idealSpan.eq_of_ideal with ring, ideal117118theorem idealSpan.unit_iff (G : Set)119  shows 1 ∈ idealSpan(A, add, zero, neg, mul, G) ↔ idealSpan(A, add, zero, neg, mul, G) = A120proof121  have ideal := idealSpan.ideal at A, add, zero, neg, mul, one, G with ring122  have ordinary := IsCommRing.ring with ring123  constructor124  . intro member125    exact IsIdeal.whole_of_one with ordinary, ideal, member126  . intro equal127    have monoid := IsRing.multiplicative with ordinary128    have member := IsMonoid.unit_in_carrier with monoid129    rwa equal130131-- A two-term convenience; arbitrary finite certificates live in FiniteCombination.132theorem idealSpan.unit_of_linear_combination2 (G p q a b : Set)133  requires bounded : G ⊆ A134  requires hp : p ∈ G135  requires hq : q ∈ G136  requires ha : a ∈ A137  requires hb : b ∈ A138  requires identity : a * p + b * q = 1139  shows 1 ∈ idealSpan(A, add, zero, neg, mul, G)140proof141  have ideal := idealSpan.ideal at A, add, zero, neg, mul, one, G with ring142  have includes := idealSpan.contains at A, add, zero, neg, mul, G with bounded143  have pIn := includes with p, hp144  have qIn := includes with q, hq145  have left := IsIdeal.mul_left_closed with ideal, ha, pIn146  have right := IsIdeal.mul_left_closed with ideal, hb, qIn147  have sum := IsIdeal.add_closed with ideal, left, right148  rwa identity at sum149150end Ring151152-- Abstract certificate soundness: evaluation maps will instantiate this theorem.153theorem idealSpan.unit_obstructs_vanishing (f A add zero neg mul one B plus z minus times unit G : Set)154  requires source : IsCommRing(A, add, zero, neg, mul, one)155  requires target : IsCommRing(B, plus, z, minus, times, unit)156  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)157  requires nontrivial : Nontrivial(B, z, unit)158  requires bounded : G ⊆ A159  requires certificate : one ∈ idealSpan(A, add, zero, neg, mul, G)160  shows ¬(∀ p ∈ G, f(p) = z)161proof162  intro vanishes163  have kernel := IsRingHom.kernel_ideal with source, target, hom164  have generators : G ⊆ ringKernel(f, A, z)165    intros p hp166    have pIn := bounded with p, hp167    have value := vanishes with p, hp168    exact ringKernel.membership.backward with ⟨pIn, value⟩169  have included := idealSpan.least with kernel, generators170  have unitIn := included with one, certificate171  have data := ringKernel.membership.forward with unitIn172  have identity := IsRingHom.one with hom173  have distinct := Nontrivial.distinct with nontrivial174  have equal : z = unit by cc175  exact distinct with equal176177-- The ideal generated by a subset of a bundled ring.178def generatedIdeal (R G : Set) : Set :=179  idealSpan(R.carrier, R.add, R.zero, R.neg, R.mul, G)180181theorem generatedIdeal.value (R G : Set)182  shows generatedIdeal(R, G) = idealSpan(R.carrier, R.add, R.zero, R.neg, R.mul, G)183proof184  simp [generatedIdeal]185186section GeneratedIdeals187variable (R : Set)188hypothesis comm : CommRing(R)189190theorem generatedIdeal.ideal (G : Set)191  shows Ideal(R, generatedIdeal(R, G))192proof193  have parts := CommRing.parts with comm194  have engine := idealSpan.ideal at R.carrier, R.add, R.zero, R.neg, R.mul,195    R.one, G with parts196  rw generatedIdeal.value197  exact Ideal.of_projections with engine198199theorem generatedIdeal.contains (G : Set)200  requires bounded : G ⊆ R201  shows G ⊆ generatedIdeal(R, G)202proof203  rw generatedIdeal.value204  exact idealSpan.contains at R.carrier, R.add, R.zero, R.neg, R.mul, G205    with bounded206207theorem generatedIdeal.least (G J : Set)208  requires ideal : Ideal(R, J)209  requires includes : G ⊆ J210  shows generatedIdeal(R, G) ⊆ J211proof212  have parts := Ideal.parts with ideal213  rw generatedIdeal.value214  exact idealSpan.least with parts, includes215216theorem generatedIdeal.mono (G H : Set)217  requires inclusion : G ⊆ H218  requires bounded : H ⊆ R219  shows generatedIdeal(R, G) ⊆ generatedIdeal(R, H)220proof221  have ideal := generatedIdeal.ideal at R, H with comm222  have includes := generatedIdeal.contains with comm, bounded223  have generators := Subset.transitive with inclusion, includes224  exact generatedIdeal.least with comm, ideal, generators225226theorem generatedIdeal.eq_of_ideal (J : Set)227  requires ideal : Ideal(R, J)228  shows generatedIdeal(R, J) = J229proof230  have parts := Ideal.parts with ideal231  rw generatedIdeal.value232  exact idealSpan.eq_of_ideal with (CommRing.parts with comm), parts233234theorem generatedIdeal.unit_iff (G : Set)235  shows R[1] ∈ generatedIdeal(R, G) ↔ generatedIdeal(R, G) = R.carrier236proof237  have ideal := generatedIdeal.ideal at R, G with comm238  have ring := CommRing.to_ring with comm239  constructor240  . intro member241    exact Ideal.contains_one with ring, ideal, member242  . intro equal243    have oneIn : R[1] ∈ R := Ring.one_mem with *244    rwa equal245246end GeneratedIdeals247