QuotientRingStarter

Quotient rings and integral domains, entirely in ZF

Open in Workbench View on GitHub

1-- Quotient rings and integral domains, entirely in ZF.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 QuotientRingStarter8import Grace.Cumulus.Algebra.Ring910theorem quotient_is_ring (A add zero neg mul one I : Set)11  requires ring : IsCommRing(A, add, zero, neg, mul, one)12  requires ideal : IsIdeal(A, add, zero, neg, mul, I)13  shows IsCommRing((A ⧸ idealRelation(A, add, neg, I)),14    quotientBinary(A, idealRelation(A, add, neg, I), add),15    ⟦zero⟧[A, idealRelation(A, add, neg, I)],16    quotientUnary(A, idealRelation(A, add, neg, I), neg),17    quotientBinary(A, idealRelation(A, add, neg, I), mul),18    ⟦one⟧[A, idealRelation(A, add, neg, I)])19proof20  exact idealQuotient.comm_ring at A, add, zero, neg, mul, one, I with *2122-- R/I is an integral domain precisely when I is prime.23theorem domain_iff_prime (A add zero neg mul one I : Set)24  requires ring : IsCommRing(A, add, zero, neg, mul, one)25  requires ideal : IsIdeal(A, add, zero, neg, mul, I)26  shows IsIntegralDomain((A ⧸ idealRelation(A, add, neg, I)),27    quotientBinary(A, idealRelation(A, add, neg, I), add),28    ⟦zero⟧[A, idealRelation(A, add, neg, I)],29    quotientUnary(A, idealRelation(A, add, neg, I), neg),30    quotientBinary(A, idealRelation(A, add, neg, I), mul),31    ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔32      IsPrimeIdeal(A, add, zero, neg, mul, one, I)33proof34  exact idealQuotient.domain_iff_prime at A, add, zero, neg, mul, one, I with *3536-- Polynomial normalization works directly inside ideal membership.37theorem rearrange_member (A add zero neg mul one I x y : Set)38  requires ring : IsCommRing(A, add, zero, neg, mul, one)39  requires hx : x ∈ A40  requires hy : y ∈ A41  requires member : call2(add, x, y) ∈ I42  shows call2(add, y, x) ∈ I43proof44  ring_nf at member45  ring_nf46  exact member4748-- Partial constructors preserve the authored nesting and leave focused goals.49theorem proof_patterns (x y : Set)50  requires h : x = x ∧ (y = y ∧ x = x)51  shows (y = y ∧ x = x) ∧ (∃ z, z = x ∧ x = x)52proof53  simp54