Grace/Cumulus/Algebra/Ring/MaximalIdeal.g17

Open in Workbench Download source

Imports

PrimeIdeal · GeneratedIdeal · Set.MaximalPrinciple

Declarations

Source

1-- Krull's maximal ideal theorem, using the axiom of choice through Zorn.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.MaximalIdeal8import PrimeIdeal9import GeneratedIdeal10import Set.MaximalPrinciple1112def properIdeals (A add zero neg mul one : Set) : Set :=13  {I ∈ 𝒫(A) | IsProperIdeal(A, add, zero, neg, mul, one, I)}1415theorem properIdeals.contains (I A add zero neg mul one : Set)16  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)17  shows I ∈ properIdeals(A, add, zero, neg, mul, one)18proof19  have subset : I ⊆ A by simp [IsProperIdeal, IsIdeal]20  unfold Subset at subset21  have bounded := set.powerset.backward with subset22  exact properIdeals.membership.backward with ⟨bounded, proper⟩2324theorem IsMaximalIdeal.exists_above (A add zero neg mul one I : Set)25  requires initial : IsProperIdeal(A, add, zero, neg, mul, one, I)26  shows ∃ M, IsMaximalIdeal(A, add, zero, neg, mul, one, M) ∧ I ⊆ M27proof28  have seed := properIdeals.contains with initial29  have closed : ∀ S, Nonempty(S) → S ⊆ properIdeals(A, add, zero, neg, mul, one) →30    (∀ C ∈ S, ∀ D ∈ S, C ⊆ D ∨ D ⊆ C) → ⋃(S) ∈ properIdeals(A, add, zero, neg, mul, one)31    intros S inhabited subset nested32    have ideals : ∀ J ∈ S, IsProperIdeal(A, add, zero, neg, mul, one, J)33      intros J hJ34      have member := subset with J, hJ35      obtain ⟨boundedJ, properJ⟩ := properIdeals.membership.forward with member36      exact properJ37    have unionProper := IsProperIdeal.union_chain with inhabited, ideals, nested38    exact properIdeals.contains with unionProper39  obtain ⟨M, memberM, extends, maximal⟩ := maximal_extension with seed, closed40  obtain ⟨boundedM, properM⟩ := properIdeals.membership.forward with memberM41  witness M42  constructor43    constructor44    . exact properM45    . intros J properJ contains46      have memberJ := properIdeals.contains with properJ47      exact maximal with J, memberJ, contains48  . exact extends4950-- In a nontrivial unital ring the zero ideal supplies the seed.51theorem IsMaximalIdeal.exists_of_nontrivial (A add zero neg mul one : Set)52  requires ring : IsRing(A, add, zero, neg, mul, one)53  requires nontrivial : Nontrivial(A, zero, one)54  shows ∃ M, IsMaximalIdeal(A, add, zero, neg, mul, one, M)55proof56  have initial := IsProperIdeal.zero_ideal with ring, nontrivial57  obtain ⟨M, maximal, extends⟩ := IsMaximalIdeal.exists_above with initial58  refine ⟨M, maximal⟩5960-- Every proper ideal in a commutative ring is contained in a prime ideal.61theorem IsPrimeIdeal.exists_above (A add zero neg mul one I : Set)62  requires commRing : IsCommRing(A, add, zero, neg, mul, one)63  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)64  shows ∃ P, IsPrimeIdeal(A, add, zero, neg, mul, one, P) ∧ I ⊆ P65proof66  obtain ⟨P, maximal, contains⟩ := IsMaximalIdeal.exists_above with proper67  have prime := IsMaximalIdeal.is_prime with *68  refine ⟨P, prime, contains⟩6970theorem IsPrimeIdeal.exists_of_nontrivial (A add zero neg mul one : Set)71  requires commRing : IsCommRing(A, add, zero, neg, mul, one)72  requires nontrivial : Nontrivial(A, zero, one)73  shows ∃ P, IsPrimeIdeal(A, add, zero, neg, mul, one, P)74proof75  have ring := IsCommRing.ring with commRing76  obtain ⟨P, maximal⟩ := IsMaximalIdeal.exists_of_nontrivial at A, add, zero, neg, mul, one with *77  have prime := IsMaximalIdeal.is_prime with *78  refine ⟨P, prime⟩7980-- The maximal-ideal reduction needed by the weak Nullstellensatz.81section GeneratedIdeals82variable (A add zero neg mul one G : Set)83hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)84hypothesis bounded : G ⊆ A85notation ring R := (A, add, zero, neg, mul, one)8687theorem idealSpan.exists_maximal88  requires proper : ¬(1 ∈ idealSpan(A, add, zero, neg, mul, G))89  shows ∃ M, IsMaximalIdeal(A, add, zero, neg, mul, one, M) ∧ G ⊆ M90proof91  have ideal := idealSpan.ideal at A, add, zero, neg, mul, one, G with ring92  have properSpan : IsProperIdeal(A, add, zero, neg, mul, one, idealSpan(A, add, zero, neg, mul, G))93    unfold IsProperIdeal94    refine ⟨ideal, proper⟩95  obtain ⟨M, maximal, includes⟩ := IsMaximalIdeal.exists_above with properSpan96  have generators := idealSpan.contains at A, add, zero, neg, mul, G with bounded97  have contains := Subset.transitive with generators, includes98  refine ⟨M, maximal, contains⟩99100theorem idealSpan.unit_iff_no_maximal101  shows 1 ∈ idealSpan(A, add, zero, neg, mul, G) ↔102    ¬(∃ M, IsMaximalIdeal(A, add, zero, neg, mul, one, M) ∧ G ⊆ M)103proof104  constructor105  . intros certificate witness106    obtain ⟨M, maximal, contains⟩ := witness107    have ideal := IsMaximalIdeal.ideal with maximal108    have proper := IsMaximalIdeal.proper with maximal109    have included := idealSpan.least with ideal, contains110    have member := included with one, certificate111    exact proper.right with member112  . intro absent113    have alternatives : 1 ∈ idealSpan(A, add, zero, neg, mul, G) ∨ ¬(1 ∈ idealSpan(A, add, zero, neg, mul, G))114      tauto115    cases alternatives with certificate | proper116    . exact certificate117    . exfalso118      have witness := idealSpan.exists_maximal with ring, bounded, proper119      exact absent with witness120121end GeneratedIdeals122123-- The same results for a bundled ring.124section BundledMaximal125variable (R : Set)126hypothesis ring : Ring(R)127128theorem ProperIdeal.extends_maximal (I : Set)129  requires proper : ProperIdeal(R, I)130  shows ∃ M, MaximalIdeal(R, M) ∧ I ⊆ M131proof132  have parts := ProperIdeal.parts with proper133  obtain ⟨M, maximal, includes⟩ := IsMaximalIdeal.exists_above with parts134  have bundled := MaximalIdeal.of_projections with maximal135  refine ⟨M, bundled, includes⟩136137theorem MaximalIdeal.exists138  requires nontrivial : R[0] ≠ R[1]139  shows ∃ M, MaximalIdeal(R, M)140proof141  have proper := ProperIdeal.zero with ring, nontrivial142  obtain ⟨M, maximal, includes⟩ := ProperIdeal.extends_maximal with ring, proper143  refine ⟨M, maximal⟩144145end BundledMaximal146147section BundledPrime148variable (R : Set)149hypothesis comm : CommRing(R)150151theorem ProperIdeal.extends_prime (I : Set)152  requires proper : ProperIdeal(R, I)153  shows ∃ P, PrimeIdeal(R, P) ∧ I ⊆ P154proof155  have ring := CommRing.to_ring with comm156  obtain ⟨P, maximal, includes⟩ := ProperIdeal.extends_maximal with ring, proper157  have prime := MaximalIdeal.prime with comm, maximal158  refine ⟨P, prime, includes⟩159160theorem PrimeIdeal.exists161  requires nontrivial : R[0] ≠ R[1]162  shows ∃ P, PrimeIdeal(R, P)163proof164  have ring := CommRing.to_ring with comm165  obtain ⟨M, maximal⟩ := MaximalIdeal.exists with ring, nontrivial166  have prime := MaximalIdeal.prime with comm, maximal167  refine ⟨M, prime⟩168169-- A set generating a proper ideal lies in a maximal ideal.170theorem generatedIdeal.exists_maximal (G : Set)171  requires bounded : G ⊆ R172  requires proper : R[1] ∉ generatedIdeal(R, G)173  shows ∃ M, MaximalIdeal(R, M) ∧ G ⊆ M174proof175  have ring := CommRing.to_ring with comm176  have ideal := generatedIdeal.ideal at R, G with comm177  have properSpan := ProperIdeal.mk with ring, ideal, proper178  obtain ⟨M, maximal, includes⟩ := ProperIdeal.extends_maximal with ring, properSpan179  have generators := generatedIdeal.contains with comm, bounded180  have contains := Subset.transitive with generators, includes181  refine ⟨M, maximal, contains⟩182183end BundledPrime184