ImageRingStarter

Images, reversible isomorphisms, and concise premise-driven applications

Open in Workbench View on GitHub

1-- Images, reversible isomorphisms, and concise premise-driven applications.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 ImageRingStarter8import Grace.Cumulus.Algebra.Ring910theorem image_comm_ring (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  shows IsCommRing(functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)15proof16  exact IsRingHom.image_comm_ring with source, target, hom1718theorem first_isomorphism_image (f A add zero neg mul one B plus z minus times unit : Set)19  requires source : IsCommRing(A, add, zero, neg, mul, one)20  requires target : IsCommRing(B, plus, z, minus, times, unit)21  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)22  shows IsRingIso(quotientMap(f, A, functionImage(f, A, B), idealRelation(A, add, neg, ringKernel(f, A, z))), (A ⧸ idealRelation(A, add, neg, ringKernel(f, A, z))),23    quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), add), ⟦zero⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],24    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))],25    functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)26proof27  exact IsRingHom.first_isomorphism_image with source, target, hom2829theorem image_factorization (f A add zero neg mul one B plus z minus times unit : Set)30  requires source : IsCommRing(A, add, zero, neg, mul, one)31  requires target : IsCommRing(B, plus, z, minus, times, unit)32  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)33  shows compose(identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B) = f34proof35  exact IsRingHom.image_factorization with source, target, hom3637theorem inverse_isomorphism (f A add zero neg mul one B plus z minus times unit : Set)38  requires source : IsCommRing(A, add, zero, neg, mul, one)39  requires target : IsCommRing(B, plus, z, minus, times, unit)40  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)41  shows IsRingIso(converse(f, A, B), B, plus, z, minus, times, unit, A, add, zero, neg, mul, one)42proof43  exact IsRingIso.inverse with source, target, iso44