Grace/Cumulus/Algebra/Ring/IdealCore.g17

Open in Workbench Download source

Imports

Core · Set.Order

Declarations

Source

1-- Two-sided ideals over separate pieces: the engine under Ideal, with the2-- proper and maximal ideals and the closure results, all in ZF3-- 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.IdealCore9import Core10import Set.Order1112-- IsIdeal(A, add, zero, neg, mul, I) is the two-sided ideal over separate13-- pieces; the bundled Ideal(R, I) under a ring hypothesis is defined in14-- Ideal and bridged to this form. Ring laws appear as hypotheses of the15-- ring-specific results.16predicate IsIdeal (A add zero neg mul I : Set) :=17  I ⊆ A ∧ zero ∈ I ∧18  (∀ x ∈ I, ∀ y ∈ I, call2(add, x, y) ∈ I) ∧19  (∀ x ∈ I, neg(x) ∈ I) ∧20  (∀ a ∈ A, ∀ x ∈ I, call2(mul, a, x) ∈ I ∧ call2(mul, x, a) ∈ I)21predicate IsProperIdeal (A add zero neg mul one I : Set) :=22  IsIdeal(A, add, zero, neg, mul, I) ∧ ¬(one ∈ I)23predicate IsMaximalIdeal (A add zero neg mul one M : Set) :=24  IsProperIdeal(A, add, zero, neg, mul, one, M) ∧25  (∀ J, IsProperIdeal(A, add, zero, neg, mul, one, J) → M ⊆ J → J = M)2627notation scoped IsIdeal(R, I) => IsIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, I)2829notation scoped IsProperIdeal(R, I) => IsProperIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)3031notation scoped IsMaximalIdeal(R, M) => IsMaximalIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)323334theorem IsMaximalIdeal.proper (A add zero neg mul one I : Set)35  requires h : IsMaximalIdeal(A, add, zero, neg, mul, one, I)36  shows IsProperIdeal(A, add, zero, neg, mul, one, I)37proof38  exact h.left3940theorem IsMaximalIdeal.ideal (A add zero neg mul one I : Set)41  requires h : IsMaximalIdeal(A, add, zero, neg, mul, one, I)42  shows IsIdeal(A, add, zero, neg, mul, I)43proof44  have proper := IsMaximalIdeal.proper with h45  exact proper.left4647theorem IsIdeal.subset_carrier (A add zero neg mul I : Set)48  requires ideal : IsIdeal(A, add, zero, neg, mul, I)49  shows I ⊆ A50proof51  simp [IsIdeal]5253theorem IsIdeal.zero_closed (A add zero neg mul I : Set)54  requires ideal : IsIdeal(A, add, zero, neg, mul, I)55  shows zero ∈ I56proof57  simp [IsIdeal]5859theorem IsIdeal.add_closed (A add zero neg mul I x y : Set)60  requires ideal : IsIdeal(A, add, zero, neg, mul, I)61  requires hx : x ∈ I62  requires hy : y ∈ I63  shows call2(add, x, y) ∈ I64proof65  exact ideal.right.right.left with x, hx, y, hy6667theorem IsIdeal.neg_closed (A add zero neg mul I x : Set)68  requires ideal : IsIdeal(A, add, zero, neg, mul, I)69  requires hx : x ∈ I70  shows neg(x) ∈ I71proof72  exact ideal.right.right.right.left with x, hx7374theorem IsIdeal.mul_left_closed (A add zero neg mul I a x : Set)75  requires ideal : IsIdeal(A, add, zero, neg, mul, I)76  requires ha : a ∈ A77  requires hx : x ∈ I78  shows call2(mul, a, x) ∈ I79proof80  have products := ideal.right.right.right.right with a, ha, x, hx81  exact products.left8283theorem IsIdeal.mul_right_closed (A add zero neg mul I a x : Set)84  requires ideal : IsIdeal(A, add, zero, neg, mul, I)85  requires ha : a ∈ A86  requires hx : x ∈ I87  shows call2(mul, x, a) ∈ I88proof89  have products := ideal.right.right.right.right with a, ha, x, hx90  exact products.right9192theorem IsIdeal.union_chain (A add zero neg mul S : Set)93  requires inhabited : Nonempty(S)94  requires ideals : ∀ I ∈ S, IsIdeal(A, add, zero, neg, mul, I)95  requires nested : ∀ I ∈ S, ∀ J ∈ S, I ⊆ J ∨ J ⊆ I96  shows IsIdeal(A, add, zero, neg, mul, ⋃(S))97proof98  obtain ⟨I0, hI0⟩ := inhabited99  obtain ⟨subset0, zero0, add0, neg0, mul0⟩ := ideals with I0, hI0100  have bounded : ⋃(S) ⊆ A101    apply union.subset102    intros B hB103    obtain ⟨subsetI, restI⟩ := ideals with B, hB104    exact subsetI105  have zeroIn : zero ∈ ⋃(S) := set.union.backward with ⟨I0, hI0, zero0⟩106  constructor107  . exact bounded108  . constructor109    . exact zeroIn110    . constructor111      . intros x hx y hy112        obtain ⟨I, hI, xI⟩ := set.union.forward with hx113        obtain ⟨J, hJ, yJ⟩ := set.union.forward with hy114        have alternatives := nested with I, hI, J, hJ115        cases alternatives with ij | ji116          have xJ := ij with x, xI117          obtain ⟨boundedJ, zeroJ, addJ, negJ, mulJ⟩ := ideals with J, hJ118          have sum := addJ with x, xJ, y, yJ119          exact set.union.backward with ⟨J, hJ, sum⟩120          have yI := ji with y, yJ121          obtain ⟨boundedI, zeroI, addI, negI, mulI⟩ := ideals with I, hI122          have sum := addI with x, xI, y, yI123          exact set.union.backward with ⟨I, hI, sum⟩124      . constructor125        . intros x hx126          obtain ⟨N, hI, xI⟩ := set.union.forward with hx127          obtain ⟨boundedI, zeroI, addI, negI, mulI⟩ := ideals with N, hI128          have negative := negI with x, xI129          exact set.union.backward with ⟨N, hI, negative⟩130        . intros a ha x hx131          obtain ⟨P, hI, xI⟩ := set.union.forward with hx132          obtain ⟨boundedI, zeroI, addI, negI, mulI⟩ := ideals with P, hI133          obtain ⟨leftProduct, rightProduct⟩ := mulI with a, ha, x, xI134          constructor135          . apply set.union.backward at S, call2(mul, a, x)136            refine ⟨P, hI, leftProduct⟩137          . apply set.union.backward at S, call2(mul, x, a)138            refine ⟨P, hI, rightProduct⟩139140theorem IsProperIdeal.union_chain (A add zero neg mul one S : Set)141  requires inhabited : Nonempty(S)142  requires ideals : ∀ I ∈ S, IsProperIdeal(A, add, zero, neg, mul, one, I)143  requires nested : ∀ I ∈ S, ∀ J ∈ S, I ⊆ J ∨ J ⊆ I144  shows IsProperIdeal(A, add, zero, neg, mul, one, ⋃(S))145proof146  have underlying : ∀ I ∈ S, IsIdeal(A, add, zero, neg, mul, I)147    intros B hB148    obtain ⟨idealI, absent⟩ := ideals with B, hB149    exact idealI150  have unionIdeal := IsIdeal.union_chain with inhabited, underlying, nested151  constructor152  . exact unionIdeal153  . intro oneIn154    obtain ⟨I, hI, oneI⟩ := set.union.forward with oneIn155    obtain ⟨idealI, absent⟩ := ideals with I, hI156    exact absent with oneI157158theorem IsIdeal.whole_of_one (A add zero neg mul one I : Set)159  requires ring : IsRing(A, add, zero, neg, mul, one)160  requires ideal : IsIdeal(A, add, zero, neg, mul, I)161  requires contains : one ∈ I162  shows I = A163proof164  rcases ideal with ⟨bounded, zeroIn, addClosed, negClosed, absorbs⟩165  have monoid := IsRing.multiplicative with ring166  apply Subset.antisymmetric with bounded167  intros x hx168  obtain ⟨product, unused⟩ := absorbs with x, hx, one, contains169  have identity := IsMonoid.right_identity with monoid, hx170  rwa identity at product171172theorem IsIdeal.zero_ideal (A add zero neg mul one : Set)173  requires ring : IsRing(A, add, zero, neg, mul, one)174  shows IsIdeal(A, add, zero, neg, mul, {zero})175proof176  have zeroIn := IsRing.zero_in_carrier with ring177  have additive := IsRing.additive with ring178  have group := IsAbelianGroup.group with additive179  have negZero := IsGroup.inverse_unit with group180  have addZero := IsRing.add_left_identity with ring, zeroIn181  constructor182    intros x hx183    have equal := singleton.membership.forward with hx184    rwa equal185  . constructor186    . exact singleton.self at zero187    . constructor188      . intros x hx y hy189        have ex := singleton.membership.forward with hx190        have ey := singleton.membership.forward with hy191        rw [ex, ey, addZero]192        exact singleton.self193      . constructor194        . intros x hx195          have ex := singleton.membership.forward with hx196          rw [ex, negZero]197          exact singleton.self198        . intros a ha x hx199          have ex := singleton.membership.forward with hx200          rw ex201          have leftZero := IsRing.mul_zero with ring, ha202          have rightZero := IsRing.zero_mul with ring, ha203          constructor204          . rw leftZero205            exact singleton.self206          . rw rightZero207            exact singleton.self208209theorem IsProperIdeal.zero_ideal (A add zero neg mul one : Set)210  requires ring : IsRing(A, add, zero, neg, mul, one)211  requires nontrivial : Nontrivial(A, zero, one)212  shows IsProperIdeal(A, add, zero, neg, mul, one, {zero})213proof214  have ideal := IsIdeal.zero_ideal with ring215  rcases nontrivial with ⟨zeroIn, oneIn, distinct⟩216  constructor217  . exact ideal218  . intro member219    have equal := singleton.membership.forward with member220    apply distinct221    symm222    exact equal223224theorem IsProperIdeal.iff_ne_whole (A add zero neg mul one I : Set)225  requires ring : IsRing(A, add, zero, neg, mul, one)226  requires ideal : IsIdeal(A, add, zero, neg, mul, I)227  shows IsProperIdeal(A, add, zero, neg, mul, one, I) ↔ I ≠ A228proof229  constructor230  . intros proper equal231    rcases proper with ⟨underlying, absent⟩232    have monoid := IsRing.multiplicative with ring233    have oneIn := IsMonoid.unit_in_carrier with monoid234    rw ← equal at oneIn235    exact absent with oneIn236  . intro distinct237    constructor238    . exact ideal239    . intro oneIn240      have equal := IsIdeal.whole_of_one with ring, ideal, oneIn241      exact distinct with equal242243theorem IsMaximalIdeal.eq_or_whole (A add zero neg mul one M J : Set)244  requires ring : IsRing(A, add, zero, neg, mul, one)245  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, M)246  requires ideal : IsIdeal(A, add, zero, neg, mul, J)247  requires contains : M ⊆ J248  shows J = M ∨ J = A249proof250  have alternatives : one ∈ J ∨ ¬(one ∈ J) by tauto251  cases alternatives with oneIn | absent252  . right253    exact IsIdeal.whole_of_one with ring, ideal, oneIn254  . left255    rcases maximal with ⟨properM, largest⟩256    have properJ : IsProperIdeal(A, add, zero, neg, mul, one, J)257      unfold IsProperIdeal258      refine ⟨ideal, absent⟩259    exact largest with J, properJ, contains260