IdealCorrespondenceStarter

Ideal correspondence with shared theorem parameters and hypotheses

Open in Workbench View on GitHub

1-- Ideal correspondence with shared theorem parameters and hypotheses.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 IdealCorrespondenceStarter8import Grace.Cumulus.Algebra.Ring910section RingMaps11variable (f A add zero neg mul one B plus z minus times unit : Set)12hypothesis source : IsCommRing(A, add, zero, neg, mul, one)13hypothesis target : IsCommRing(B, plus, z, minus, times, unit)14hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)1516theorem inverse_image (J : Set)17  requires ideal : IsIdeal(B, plus, z, minus, times, J)18  shows IsIdeal(A, add, zero, neg, mul, idealComap(f, A, J))19proof20  exact IsRingHom.comap_ideal with source, target, hom, ideal2122theorem recover_source (I : Set)23  requires ideal : IsIdeal(A, add, zero, neg, mul, I)24  requires contains : ringKernel(f, A, z) ⊆ I25  shows idealComap(f, A, idealMap(f, B, I)) = I26proof27  exact IsRingHom.comap_map_eq with source, target, hom, ideal, contains2829section Surjections30hypothesis onto : SurjectiveBetween(f, A, B)3132theorem image (I : Set)33  requires ideal : IsIdeal(A, add, zero, neg, mul, I)34  shows IsIdeal(B, plus, z, minus, times, idealMap(f, B, I))35proof36  exact IsRingHom.map_ideal with source, target, hom, onto, ideal3738end Surjections39end RingMaps4041-- Outside the section, no ring parameter or hypothesis remains in scope.42theorem inclusion_equivalence (f A B I J : Set)43  requires function : f : A → B44  requires bounded : I ⊆ A45  shows idealMap(f, B, I) ⊆ J ↔ I ⊆ idealComap(f, A, J)46proof47  exact idealMap.galois with function, bounded48