QuotientFieldStarter

Quotient fields and canonical inverses, entirely in ZF

Open in Workbench View on GitHub

1-- Quotient fields and canonical inverses, 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 QuotientFieldStarter8import Grace.Cumulus.Algebra.Field910theorem field_iff_maximal (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 IsField((A ⧸ idealRelation(A, add, neg, I)),14    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],15    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔ IsMaximalIdeal(A, add, zero, neg, mul, one, I)16proof17  exact idealQuotient.is_field_iff_maximal at A, add, zero, neg, mul, one, I with *1819-- Fieldness need not carry an arbitrarily supplied inverse operation.20theorem canonical_field (A add zero neg mul one : Set)21  requires structure : IsField(A, add, zero, neg, mul, one)22  shows IsFieldWithInverse(A, add, zero, neg, mul, one, fieldInverse(A, add, zero, neg, mul, one))23proof24  exact IsField.field at A, add, zero, neg, mul, one with *2526theorem inverse_at_zero (A add zero neg mul one : Set)27  requires structure : IsField(A, add, zero, neg, mul, one)28  shows (fieldInverse(A, add, zero, neg, mul, one))(zero) = zero29proof30  exact fieldInverse.zero at A, add, zero, neg, mul, one with *31