PrimeIdealStarter

All results in this example check in ZF: no existence choice is needed

Open in Workbench View on GitHub

1-- All results in this example check in ZF: no existence choice is needed.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 PrimeIdealStarter8import Grace.Cumulus.Algebra.Ring910theorem maximal_is_prime (A add zero neg mul one M : Set)11  requires ring : IsCommRing(A, add, zero, neg, mul, one)12  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, M)13  shows IsPrimeIdeal(A, add, zero, neg, mul, one, M)14proof15  exact IsMaximalIdeal.is_prime at A, add, zero, neg, mul, one, M with *1617-- If xy lies in a prime ideal and y does not, then x lies in the ideal.18theorem cancel_outside_factor (A add zero neg mul one P x y : Set)19  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, P)20  requires hx : x ∈ A21  requires hy : y ∈ A22  requires productIn : call2(mul, x, y) ∈ P23  requires outside : ¬(y ∈ P)24  shows x ∈ P25proof26  exact IsPrimeIdeal.left_of_mul at A, add, zero, neg, mul, one, P, x, y with *2728-- The zero ideal is prime precisely when the commutative ring is a domain.29theorem zero_prime_iff_domain (A add zero neg mul one : Set)30  requires ring : IsCommRing(A, add, zero, neg, mul, one)31  shows IsPrimeIdeal(A, add, zero, neg, mul, one, {zero}) ↔32    IsIntegralDomain(A, add, zero, neg, mul, one)33proof34  exact IsPrimeIdeal.zero_iff_domain at A, add, zero, neg, mul, one with *35