Grace/Cumulus/Algebra/Ring/Ideal.g17

Open in Workbench Download source

Imports

Basic · IdealCore

Declarations

Source

1-- Two-sided ideals of a bundled ring: Ideal(R, I) under a ring hypothesis,2-- the proper and maximal ideals, the ring notation on the elements of an3-- ideal, the bridges to the forms over separate pieces, and the closure4-- instances; everything here is ZF5-- 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.Ideal11import Basic12import IdealCore1314-- Under a hypothesis Ring(R), an ideal of R is a subset containing zero and15-- closed under addition, negation, and multiplication by any element of R16-- on either side; a proper ideal omits one, and a maximal ideal is a proper17-- ideal contained in no larger proper ideal. The predicates take the ring18-- first, Ideal(R, I), and their bodies read the operations off the19-- hypothesis, so each is a formula over R.add, R.zero, R.neg, and R.mul20-- alone. IsIdeal(A, add, zero, neg, mul, I), IsProperIdeal(A, …, one, I),21-- and IsMaximalIdeal(A, …, one, M) remain the forms over separate pieces,22-- bridged below.23section Definitions24variable (R : Set)25hypothesis ring : Ring(R)2627predicate Ideal (I : Set) :=28  I ⊆ R ∧ R[0] ∈ I ∧ (∀ x y ∈ I, x + y ∈ I) ∧29  (∀ x ∈ I, -x ∈ I) ∧ (∀ a ∈ R, ∀ x ∈ I, a * x ∈ I ∧ x * a ∈ I)30predicate ProperIdeal (I : Set) := Ideal(I) ∧ R[1] ∉ I31predicate MaximalIdeal (M : Set) :=32  ProperIdeal(M) ∧ (∀ J, ProperIdeal(J) → M ⊆ J → J = M)3334end Definitions3536-- On the elements of an ideal the operations are written as in the ring:37-- under Ideal(R, I) a binder (x : I) is x ∈ I, and x + y, x * y, -x, and38-- x - y are the operations of R.39notation infixl 60 "+" => call2(R.add, _, _) via hypothesis Ideal(R, I) for I40notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis Ideal(R, I) for I41notation prefix 75 "-" => apply(R.neg, _) via hypothesis Ideal(R, I) for I42notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis Ideal(R, I) for I43notation infixl 60 "+" => call2(R.add, _, _) via hypothesis ProperIdeal(R, I) for I44notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis ProperIdeal(R, I) for I45notation prefix 75 "-" => apply(R.neg, _) via hypothesis ProperIdeal(R, I) for I46notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis ProperIdeal(R, I) for I47notation infixl 60 "+" => call2(R.add, _, _) via hypothesis MaximalIdeal(R, I) for I48notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis MaximalIdeal(R, I) for I49notation prefix 75 "-" => apply(R.neg, _) via hypothesis MaximalIdeal(R, I) for I50notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis MaximalIdeal(R, I) for I5152-- Bridges between the bundled predicates and the forms over separate53-- pieces. The bundled-to-unbundled directions are instances, so `with *`54-- reads the unbundled form off a bundled hypothesis; of_projections comes55-- back for a ring value, and of_parts for a constructed ring.56instance Ideal.parts (R I : Set)57  requires ideal : Ideal(R, I)58  shows IsIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, I)59proof60  obtain ⟨bounded, zeroIn, sums, negatives, products⟩ := ideal61  unfold IsIdeal62  exact ⟨bounded, zeroIn, sums, negatives, products⟩6364theorem Ideal.of_projections (R I : Set)65  requires ideal : IsIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, I)66  shows Ideal(R, I)67proof68  obtain ⟨bounded, zeroIn, sums, negatives, products⟩ := ideal69  unfold Ideal.Ideal70  exact ⟨bounded, zeroIn, sums, negatives, products⟩7172theorem Ideal.of_parts (A add zero neg mul one I : Set)73  requires ideal : IsIdeal(A, add, zero, neg, mul, I)74  shows Ideal(Ring.mk(A, add, zero, neg, mul, one), I)75proof76  have shifted : IsIdeal(Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),77      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),78      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),79      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),80      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)), I)81    ring_projections82  exact Ideal.of_projections with shifted8384instance ProperIdeal.parts (R I : Set)85  requires proper : ProperIdeal(R, I)86  shows IsProperIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)87proof88  obtain ⟨ideal, oneOut⟩ := proper89  have parts := Ideal.parts with ideal90  unfold IsProperIdeal91  exact ⟨parts, oneOut⟩9293theorem ProperIdeal.of_projections (R I : Set)94  requires proper : IsProperIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)95  shows ProperIdeal(R, I)96proof97  obtain ⟨ideal, oneOut⟩ := proper98  have bundled := Ideal.of_projections with ideal99  unfold Ideal.ProperIdeal100  exact ⟨bundled, oneOut⟩101102theorem ProperIdeal.of_parts (A add zero neg mul one I : Set)103  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)104  shows ProperIdeal(Ring.mk(A, add, zero, neg, mul, one), I)105proof106  have shifted : IsProperIdeal(Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),107      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),108      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),109      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),110      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)),111      Ring.one(Ring.mk(A, add, zero, neg, mul, one)), I)112    ring_projections113  exact ProperIdeal.of_projections with shifted114115instance MaximalIdeal.parts (R M : Set)116  requires maximal : MaximalIdeal(R, M)117  shows IsMaximalIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)118proof119  obtain ⟨proper, largest⟩ := maximal120  have parts := ProperIdeal.parts with proper121  unfold IsMaximalIdeal122  refine ⟨parts, ?_⟩123  intros J properJ contains124  have bundledJ := ProperIdeal.of_projections with properJ125  exact largest with J, bundledJ, contains126127theorem MaximalIdeal.of_projections (R M : Set)128  requires maximal : IsMaximalIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)129  shows MaximalIdeal(R, M)130proof131  obtain ⟨proper, largest⟩ := maximal132  have bundled := ProperIdeal.of_projections with proper133  unfold Ideal.MaximalIdeal134  refine ⟨bundled, ?_⟩135  intros J properJ contains136  have partsJ := ProperIdeal.parts with properJ137  exact largest with J, partsJ, contains138139theorem MaximalIdeal.of_parts (A add zero neg mul one M : Set)140  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, M)141  shows MaximalIdeal(Ring.mk(A, add, zero, neg, mul, one), M)142proof143  have shifted : IsMaximalIdeal(Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),144      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),145      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),146      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),147      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)),148      Ring.one(Ring.mk(A, add, zero, neg, mul, one)), M)149    ring_projections150  exact MaximalIdeal.of_projections with shifted151152-- The projections down the hierarchy; the instance paths form a chain.153instance ProperIdeal.to_ideal (R I : Set)154  requires proper : ProperIdeal(R, I)155  shows Ideal(R, I)156proof157  obtain ⟨ideal, oneOut⟩ := proper158  exact ideal159160theorem ProperIdeal.one_not_mem (R I : Set)161  requires proper : ProperIdeal(R, I)162  shows R[1] ∉ I163proof164  obtain ⟨ideal, oneOut⟩ := proper165  exact oneOut166167instance MaximalIdeal.to_proper (R M : Set)168  requires maximal : MaximalIdeal(R, M)169  shows ProperIdeal(R, M)170proof171  obtain ⟨proper, largest⟩ := maximal172  exact proper173174theorem MaximalIdeal.to_ideal (R M : Set)175  requires maximal : MaximalIdeal(R, M)176  shows Ideal(R, M)177proof178  have proper := MaximalIdeal.to_proper with maximal179  exact ProperIdeal.to_ideal with proper180181section IdealLaws182variable (R I : Set)183hypothesis ideal : Ideal(R, I)184185theorem Ideal.subset186  shows I ⊆ R.carrier187proof188  obtain ⟨bounded, rest⟩ := ideal189  exact bounded190191-- Closure: the carrier membership of an element of the ideal is a typing192-- rule, and the membership of zero, a sum, and a negation are instances,193-- so each is synthesized.194theorem Ideal.mem_carrier (x : I)195  shows x ∈ R.carrier196proof197  have bounded := Ideal.subset with ideal198  have xIn : x ∈ I by assumption199  exact bounded with x, xIn200201instance Ideal.zero_mem202  shows R[0] ∈ I203proof204  obtain ⟨bounded, zeroIn, rest⟩ := ideal205  exact zeroIn206207instance Ideal.add_mem (x y : I)208  shows x + y ∈ I209proof210  obtain ⟨bounded, zeroIn, sums, negatives, products⟩ := ideal211  have xIn : x ∈ I by assumption212  have yIn : y ∈ I by assumption213  exact sums with x, xIn, y, yIn214215instance Ideal.neg_mem (x : I)216  shows -x ∈ I217proof218  obtain ⟨bounded, zeroIn, sums, negatives, products⟩ := ideal219  have xIn : x ∈ I by assumption220  exact negatives with x, xIn221222theorem Ideal.nonempty223  shows Nonempty(I)224proof225  have zeroIn : R[0] ∈ I := Ideal.zero_mem with *226  exact ⟨R[0], zeroIn⟩227228end IdealLaws229230section IdealAbsorption231variable (R I : Set)232hypothesis ring : Ring(R)233hypothesis ideal : Ideal(R, I)234235-- Absorption on either side, and closure under subtraction.236instance Ideal.mul_left_mem (a : R) (x : I)237  shows a * x ∈ I238proof239  obtain ⟨bounded, zeroIn, sums, negatives, products⟩ := ideal240  have aIn : a ∈ R by assumption241  have xIn : x ∈ I by assumption242  have both := products with a, aIn, x, xIn243  exact both.left244245instance Ideal.mul_right_mem (a : R) (x : I)246  shows x * a ∈ I247proof248  obtain ⟨bounded, zeroIn, sums, negatives, products⟩ := ideal249  have aIn : a ∈ R by assumption250  have xIn : x ∈ I by assumption251  have both := products with a, aIn, x, xIn252  exact both.right253254instance Ideal.sub_mem (x y : I)255  shows x - y ∈ I256proof257  have xIn : x ∈ R := Ideal.mem_carrier with *258  have yIn : y ∈ R := Ideal.mem_carrier with *259  have negIn : -y ∈ I := Ideal.neg_mem with *260  rw Ring.sub.value261  exact Ideal.add_mem with *262263end IdealAbsorption264265section IdealConstructions266variable (R : Set)267hypothesis ring : Ring(R)268269-- The constructor.270theorem Ideal.mk (I : Set)271  requires bounded : I ⊆ R272  requires zeroIn : R[0] ∈ I273  requires sums : ∀ x y ∈ I, x + y ∈ I274  requires negatives : ∀ x ∈ I, -x ∈ I275  requires products : ∀ a ∈ R, ∀ x ∈ I, a * x ∈ I ∧ x * a ∈ I276  shows Ideal(R, I)277proof278  unfold Ideal.Ideal279  exact ⟨bounded, zeroIn, sums, negatives, products⟩280281theorem ProperIdeal.mk (I : Set)282  requires ideal : Ideal(R, I)283  requires oneOut : R[1] ∉ I284  shows ProperIdeal(R, I)285proof286  unfold Ideal.ProperIdeal287  exact ⟨ideal, oneOut⟩288289-- The ideals every ring has: the whole ring and the zero ideal.290theorem Ideal.whole291  shows Ideal(R, R.carrier)292proof293  have reflexive := Subset.reflexive at R.carrier294  have zeroIn : R[0] ∈ R := Ring.zero_mem with *295  apply Ideal.mk with ring, reflexive, zeroIn296  . intros x hx y hy297    exact Ring.add_mem with *298  . intros x hx299    exact Ring.neg_mem with *300  . intros a ha x hx301    constructor302    . exact Ring.mul_mem with *303    . exact Ring.mul_mem with *304305theorem Ideal.zero306  shows Ideal(R, {R[0]})307proof308  have parts := Ring.parts with ring309  have engine := IsIdeal.zero_ideal with parts310  exact Ideal.of_projections with engine311312-- An ideal containing one is the whole ring, so a proper ideal is exactly313-- an ideal different from the ring.314theorem Ideal.contains_one (I : Set)315  requires ideal : Ideal(R, I)316  requires oneIn : R[1] ∈ I317  shows I = R.carrier318proof319  have parts := Ring.parts with ring320  have engine := Ideal.parts with ideal321  exact IsIdeal.whole_of_one with parts, engine, oneIn322323theorem ProperIdeal.iff_ne_carrier (I : Set)324  requires ideal : Ideal(R, I)325  shows ProperIdeal(R, I) ↔ I ≠ R.carrier326proof327  have parts := Ring.parts with ring328  have engine := Ideal.parts with ideal329  have criterion := IsProperIdeal.iff_ne_whole with parts, engine330  constructor331  . intro proper332    exact criterion.forward with (ProperIdeal.parts with proper)333  . intro distinct334    exact ProperIdeal.of_projections with (criterion.backward with distinct)335336theorem ProperIdeal.zero337  requires nontrivial : R[0] ≠ R[1]338  shows ProperIdeal(R, {R[0]})339proof340  have parts := Ring.parts with ring341  have zeroIn : R[0] ∈ R := Ring.zero_mem with *342  have oneIn : R[1] ∈ R := Ring.one_mem with *343  have distinct : Nontrivial(R.carrier, R.zero, R.one)344    unfold Nontrivial345    exact ⟨zeroIn, oneIn, nontrivial⟩346  have engine := IsProperIdeal.zero_ideal with parts, distinct347  exact ProperIdeal.of_projections with engine348349-- An ideal above a maximal ideal is the maximal ideal or the whole ring.350theorem MaximalIdeal.overideal (M J : Set)351  requires maximal : MaximalIdeal(R, M)352  requires ideal : Ideal(R, J)353  requires contains : M ⊆ J354  shows J = M ∨ J = R.carrier355proof356  have parts := Ring.parts with ring357  have engineM := MaximalIdeal.parts with maximal358  have engineJ := Ideal.parts with ideal359  exact IsMaximalIdeal.eq_or_whole with parts, engineM, engineJ, contains360361end IdealConstructions362