FirstIsomorphismStarter

Ring maps and the first isomorphism theorem, entirely in ZF

Open in Workbench View on GitHub

1-- Ring maps and the first isomorphism theorem, 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 FirstIsomorphismStarter8import Grace.Cumulus.Algebra.Ring910theorem first_isomorphism (f A add zero neg mul one B plus z minus times unit : Set)11  requires source : IsCommRing(A, add, zero, neg, mul, one)12  requires target : IsCommRing(B, plus, z, minus, times, unit)13  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)14  requires onto : SurjectiveBetween(f, A, B)15  shows IsRingIso(quotientMap(f, A, B, idealRelation(A, add, neg, ringKernel(f, A, z))), (A ⧸ idealRelation(A, add, neg, ringKernel(f, A, z))),16    quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), add), ⟦zero⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],17    quotientUnary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), neg), quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), mul), ⟦one⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))], B, plus, z, minus, times, unit)18proof19  exact idealQuotient.first_isomorphism at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit with *2021-- The mathematical argument does not expose graph encodings.22theorem equal_mod_kernel (f A add zero neg mul one B plus z minus times unit x y : Set)23  requires source : IsCommRing(A, add, zero, neg, mul, one)24  requires target : IsCommRing(B, plus, z, minus, times, unit)25  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)26  requires hx : x ∈ A27  requires hy : y ∈ A28  requires same : f(x) = f(y)29  shows ⟦x⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))] =30    ⟦y⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))]31proof32  have ideal := IsRingHom.kernel_ideal at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit with *33  have congruent := IsRingHom.kernel_congruent.backward at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *34  exact idealClass.eq_iff_congruent.backward with *3536-- Uniqueness is now pointwise reasoning on quotient elements.37theorem unique_descent (f g A B r : Set)38  requires function : f : A → B39  requires equivalence : Equivalence(A, r)40  requires respects : Respects(f, A, r)41  requires candidate : g : (A ⧸ r) → B42  requires factors : ∀ x ∈ A, g(⟦x⟧[A, r]) = f(x)43  shows g = quotientMap(f, A, B, r)44proof45  exact quotientMap.unique at f, g, A, B, r with *46