PrimeCorrespondenceStarter

Prime and maximal ideals transported through surjective homomorphisms

Open in Workbench View on GitHub

1-- Prime and maximal ideals transported through surjective homomorphisms.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 PrimeCorrespondenceStarter8import 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)1516-- This direction works even when the homomorphism is not surjective.17theorem pullback_prime (J : Set)18  requires prime : IsPrimeIdeal(B, plus, z, minus, times, unit, J)19  shows IsPrimeIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J))20proof21  exact IsRingHom.comap_prime with source, target, hom, prime2223section Surjections24hypothesis onto : SurjectiveBetween(f, A, B)2526theorem prime_equivalence (J : Set)27  requires ideal : IsIdeal(B, plus, z, minus, times, J)28  shows IsPrimeIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J)) ↔ IsPrimeIdeal(B, plus, z, minus, times, unit, J)29proof30  exact IsRingHom.comap_prime_iff with source, target, hom, onto, ideal3132theorem maximal_equivalence (J : Set)33  requires ideal : IsIdeal(B, plus, z, minus, times, J)34  shows IsMaximalIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J)) ↔ IsMaximalIdeal(B, plus, z, minus, times, unit, J)35proof36  exact IsRingHom.comap_maximal_iff with source, target, hom, onto, ideal3738theorem pushforward_maximal (I : Set)39  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)40  requires contains : ringKernel(f, A, z) ⊆ I41  shows IsMaximalIdeal(B, plus, z, minus, times, unit, idealMap(f, B, I))42proof43  exact IsRingHom.map_maximal with source, target, hom, onto, maximal, contains4445end Surjections46end RingMaps47