Grace/Cumulus/Algebra/Ring/PrimeIdeal.g17

Open in Workbench Download source

Imports

Ideal · PrimeIdealCore

Declarations

Source

1-- Prime ideals of a bundled ring: PrimeIdeal(R, I) under a ring hypothesis,2-- the bridges to the form over separate pieces, the factor laws, and the3-- primality of maximal ideals in a commutative ring; everything here is ZF4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Ring.PrimeIdeal10import Ideal11import PrimeIdealCore1213-- Under a hypothesis Ring(R), a prime ideal is a proper ideal that contains14-- a factor of every product it contains. IsPrimeIdeal(A, add, zero, neg, mul,15-- one, I) remains the form over separate pieces, bridged below.16section Definitions17variable (R : Set)18hypothesis ring : Ring(R)1920predicate PrimeIdeal (I : Set) :=21  ProperIdeal(R, I) ∧ (∀ x y ∈ R, x * y ∈ I → x ∈ I ∨ y ∈ I)2223end Definitions2425notation infixl 60 "+" => call2(R.add, _, _) via hypothesis PrimeIdeal(R, I) for I26notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis PrimeIdeal(R, I) for I27notation prefix 75 "-" => apply(R.neg, _) via hypothesis PrimeIdeal(R, I) for I28notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis PrimeIdeal(R, I) for I2930instance PrimeIdeal.parts (R I : Set)31  requires prime : PrimeIdeal(R, I)32  shows IsPrimeIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)33proof34  obtain ⟨proper, factors⟩ := prime35  have parts := ProperIdeal.parts with proper36  unfold IsPrimeIdeal37  exact ⟨parts, factors⟩3839theorem PrimeIdeal.of_projections (R I : Set)40  requires prime : IsPrimeIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one,41    I)42  shows PrimeIdeal(R, I)43proof44  obtain ⟨proper, factors⟩ := prime45  have bundled := ProperIdeal.of_projections with proper46  unfold PrimeIdeal.PrimeIdeal47  exact ⟨bundled, factors⟩4849theorem PrimeIdeal.of_parts (A add zero neg mul one I : Set)50  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)51  shows PrimeIdeal(Ring.mk(A, add, zero, neg, mul, one), I)52proof53  have shifted : IsPrimeIdeal(Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),54      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),55      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),56      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),57      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)),58      Ring.one(Ring.mk(A, add, zero, neg, mul, one)), I)59    ring_projections60  exact PrimeIdeal.of_projections with shifted6162instance PrimeIdeal.to_proper (R I : Set)63  requires prime : PrimeIdeal(R, I)64  shows ProperIdeal(R, I)65proof66  obtain ⟨proper, factors⟩ := prime67  exact proper6869theorem PrimeIdeal.to_ideal (R I : Set)70  requires prime : PrimeIdeal(R, I)71  shows Ideal(R, I)72proof73  have proper := PrimeIdeal.to_proper with prime74  exact ProperIdeal.to_ideal with proper7576section PrimeLaws77variable (R I : Set)78hypothesis ring : Ring(R)79hypothesis prime : PrimeIdeal(R, I)8081-- A product lies in a prime ideal exactly when a factor does.82theorem PrimeIdeal.mem_or_mem (x y : R)83  requires productIn : x * y ∈ I84  shows x ∈ I ∨ y ∈ I85proof86  obtain ⟨proper, factors⟩ := prime87  have xIn : x ∈ R by assumption88  have yIn : y ∈ R by assumption89  exact factors with x, xIn, y, yIn, productIn9091theorem PrimeIdeal.mem_of_mul (x y : R)92  requires productIn : x * y ∈ I93  requires absent : y ∉ I94  shows x ∈ I95proof96  have alternatives := PrimeIdeal.mem_or_mem with *97  cases alternatives with xIn | yIn98  . exact xIn99  . exfalso100    exact absent with yIn101102theorem PrimeIdeal.mul_mem_iff (x y : R)103  shows x * y ∈ I ↔ x ∈ I ∨ y ∈ I104proof105  have ideal := PrimeIdeal.to_ideal with prime106  constructor107  . intro productIn108    exact PrimeIdeal.mem_or_mem with *109  . intro alternatives110    cases alternatives with xIn | yIn111    . exact Ideal.mul_right_mem with *112    . exact Ideal.mul_left_mem with *113114end PrimeLaws115116section CommutativeRings117variable (R : Set)118hypothesis comm : CommRing(R)119120-- In a commutative ring every maximal ideal is prime.121theorem MaximalIdeal.prime (M : Set)122  requires maximal : MaximalIdeal(R, M)123  shows PrimeIdeal(R, M)124proof125  have parts := CommRing.parts with comm126  have engine := MaximalIdeal.parts with maximal127  have prime := IsMaximalIdeal.is_prime with parts, engine128  exact PrimeIdeal.of_projections with prime129130end CommutativeRings131