ZornApplications

Classical maximality results from the axiom of choice, with checked ZF foundations

Open in Workbench View on GitHub

1-- Classical maximality results from the axiom of choice, with checked ZF foundations.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 ZornApplications8import Grace.Cumulus.Algebra.Field.Quotient9import Grace.Cumulus.Algebra.Ring.MaximalIdeal10import Grace.Cumulus.Algebra.Ring.Quotient1112-- Hausdorff's maximal principle, preserving any chain we already have.13theorem extend_chain (A r C : Set)14  requires chain : Chain(A, r, C)15  shows ∃ M, Chain(A, r, M) ∧ C ⊆ M ∧16    (∀ D, Chain(A, r, D) → M ⊆ D → D = M)17proof18  exact Chain.extends_maximal at A, r, C with *1920-- Starting at a specified element, and obtaining a maximal element above it.21theorem maximal_above (A r a : Set)22  requires zorn : ZornCondition(A, r)23  requires start : a ∈ A24  shows ∃ m, Maximal(A, r, m) ∧ relates(r, a, m)25proof26  exact Zorn.above at A, r, a with *2728-- Krull's theorem. The carrier and all ring operations are sets.29-- This works for arbitrary unital rings and two-sided ideals.30theorem maximal_ideal (A add zero neg mul one : Set)31  requires ring : IsRing(A, add, zero, neg, mul, one)32  requires nontrivial : Nontrivial(A, zero, one)33  shows ∃ M, IsMaximalIdeal(A, add, zero, neg, mul, one, M)34proof35  exact IsMaximalIdeal.exists_of_nontrivial at A, add, zero, neg, mul,36    one with *3738-- The usual textbook formulation, with a prescribed proper ideal I.39theorem extend_ideal (A add zero neg mul one I : Set)40  requires ring : IsRing(A, add, zero, neg, mul, one)41  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)42  shows ∃ M, IsProperIdeal(A, add, zero, neg, mul, one, M) ∧ I ⊆ M ∧43    (∀ J, IsIdeal(A, add, zero, neg, mul, J) → M ⊆ J → J = M ∨ J = A)44proof45  obtain ⟨M, maximal, contains⟩ := IsMaximalIdeal.exists_above at A, add, zero, neg, mul, one, I with proper46  have properM : IsProperIdeal(A, add, zero, neg, mul, one, M) by settle with IsMaximalIdeal47  witness M48  constructor49  . exact properM50  . constructor51    . exact contains52    . intros J ideal includes53      exact IsMaximalIdeal.eq_or_whole at A, add, zero, neg, mul, one, M,54        J with *5556-- Ordinary AC gives a prime ideal extending any given proper ideal.57theorem extend_to_prime (A add zero neg mul one I : Set)58  requires ring : IsCommRing(A, add, zero, neg, mul, one)59  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)60  shows ∃ P, IsPrimeIdeal(A, add, zero, neg, mul, one, P) ∧ I ⊆ P61proof62  exact IsPrimeIdeal.exists_above at A, add, zero, neg, mul, one, I with *6364-- Zorn supplies a domain quotient whose kernel contains the prescribed ideal.65theorem exists_domain_quotient (A add zero neg mul one I : Set)66  requires ring : IsCommRing(A, add, zero, neg, mul, one)67  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)68  shows ∃ P, I ⊆ P ∧ IsIntegralDomain((A ⧸ idealRelation(A, add, neg, P)),69    quotientBinary(A, idealRelation(A, add, neg, P), add),70    ⟦zero⟧[A, idealRelation(A, add, neg, P)],71    quotientUnary(A, idealRelation(A, add, neg, P), neg),72    quotientBinary(A, idealRelation(A, add, neg, P), mul),73    ⟦one⟧[A, idealRelation(A, add, neg, P)])74proof75  obtain ⟨P, prime, contains⟩ := IsPrimeIdeal.exists_above at A, add, zero, neg, mul, one, I with *76  have domain := idealQuotient.domain_of_prime at A, add, zero, neg, mul, one, P with *77  refine ⟨P, contains, domain⟩7879-- Every prescribed proper ideal lies in the kernel of a field quotient.80-- Choice is used to obtain M; constructing the quotient and inverse is ZF.81theorem exists_field_quotient (A add zero neg mul one I : Set)82  requires ring : IsCommRing(A, add, zero, neg, mul, one)83  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)84  shows ∃ M, I ⊆ M ∧ IsFieldWithInverse((A ⧸ idealRelation(A, add, neg, M)),85    quotientBinary(A, idealRelation(A, add, neg, M), add), ⟦zero⟧[A, idealRelation(A, add, neg, M)],86    quotientUnary(A, idealRelation(A, add, neg, M), neg), quotientBinary(A, idealRelation(A, add, neg, M), mul), ⟦one⟧[A, idealRelation(A, add, neg, M)],87    idealQuotientInverse(A, add, zero, neg, mul, one, M))88proof89  obtain ⟨M, maximal, contains⟩ := IsMaximalIdeal.exists_above at A, add, zero, neg, mul, one, I with proper90  have field := idealQuotient.field_of_maximal at A, add, zero, neg, mul, one, M with *91  refine ⟨M, contains, field⟩92