Grace/Cumulus/Algebra/Ring/PrimeCorrespondence.g17

Open in Workbench Download source

Imports

Correspondence · PrimeIdeal

Declarations

Source

1-- Prime and maximal ideal correspondence under surjective ring maps (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 Grace.Cumulus.Algebra.Ring.PrimeCorrespondence8import Correspondence9import PrimeIdeal1011section RingMaps12variable (f A add zero neg mul one B plus z minus times unit : Set)13hypothesis source : IsCommRing(A, add, zero, neg, mul, one)14hypothesis target : IsCommRing(B, plus, z, minus, times, unit)15hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)16notation ring R := (A, add, zero, neg, mul, one)17notation ring S := (B, plus, z, minus, times, unit)1819theorem IsRingHom.comap_proper (J : Set)20  requires proper : IsProperIdeal(B, plus, z, minus, times, unit, J)21  shows IsProperIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J))22proof23  have preimage := IsRingHom.comap_ideal with source, target, hom, proper.left24  have identity := IsRingHom.one with hom25  unfold IsProperIdeal26  refine ⟨preimage, ?_⟩27  intro member28  have data := idealComap.membership.forward with member29  have forbidden : unit ∈ J by cc30  exact proper.right with forbidden3132theorem IsRingHom.comap_prime (J : Set)33  requires prime : IsPrimeIdeal(B, plus, z, minus, times, unit, J)34  shows IsPrimeIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J))35proof36  have proper := IsRingHom.comap_proper with source, target, hom, prime.left37  unfold IsPrimeIdeal38  refine ⟨proper, ?_⟩39  intros x hx y hy product40  have fx := IsRingHom.closed with hom, hx41  have fy := IsRingHom.closed with hom, hy42  have value := IsRingHom.mul with hom, hx, hy43  have data := idealComap.membership.forward with product44  have mapped : S[f(x) * f(y)] ∈ J by cc45  have alternatives := prime.right with f(x), f(y), mapped46  cases alternatives with leftMember | rightMember47  . left48    exact idealComap.membership.backward with ⟨hx, leftMember⟩49  . right50    exact idealComap.membership.backward with ⟨hy, rightMember⟩5152section Surjections53hypothesis onto : SurjectiveBetween(f, A, B)5455theorem IsRingHom.map_proper (I : Set)56  requires proper : IsProperIdeal(A, add, zero, neg, mul, one, I)57  requires contains : ringKernel(f, A, z) ⊆ I58  shows IsProperIdeal(B, plus, z, minus, times, unit, idealMap(f, B, I))59proof60  have image := IsRingHom.map_ideal with source, target, hom, onto, proper.left61  have roundtrip := IsRingHom.comap_map_eq with source, target, hom, proper.left, contains62  have ring := IsCommRing.ring with source63  have monoid := IsRing.multiplicative with ring64  have oneIn := IsMonoid.unit_in_carrier with monoid65  have identity := IsRingHom.one with hom66  unfold IsProperIdeal67  refine ⟨image, ?_⟩68  intro member69  have mapped : f(one) ∈ idealMap(f, B, I) by cc70  have preimage : one ∈ idealComap(f, A, idealMap(f, B, I)) := idealComap.membership.backward with ⟨oneIn, mapped⟩71  rw roundtrip at preimage72  exact proper.right with preimage7374theorem IsRingHom.prime_of_comap (J : Set)75  requires ideal : IsIdeal(B, plus, z, minus, times, J)76  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one,77    idealComap(f, A, J))78  shows IsPrimeIdeal(B, plus, z, minus, times, unit, J)79proof80  have contains := IsRingHom.kernel_subset_comap with source, target, hom, ideal81  have imageProper := IsRingHom.map_proper with source, target, hom, onto, prime.left, contains82  have bounded := IsIdeal.subset_carrier with ideal83  have roundtrip := idealMap.comap_eq with onto, bounded84  rw roundtrip at imageProper85  have function := IsRingHom.function with hom86  have ring := IsCommRing.ring with source87  have ontoLaw := onto88  unfold IsPrimeIdeal89  refine ⟨imageProper, ?_⟩90  intros a ha b hb product91  obtain ⟨x, hx, edgeX⟩ := ontoLaw.right with a, ha92  obtain ⟨y, hy, edgeY⟩ := ontoLaw.right with b, hb93  have valueX := FunctionBetween.apply_value at f, A, B, x, a with *94  have valueY := FunctionBetween.apply_value at f, A, B, y, b with *95  have closed := IsRing.mul_closed with ring, hx, hy96  have value := IsRingHom.mul with hom, hx, hy97  have mapped : f(R[x * y]) ∈ J by cc98  have preimage : R[x * y] ∈ idealComap(f, A, J) := idealComap.membership.backward with ⟨closed, mapped⟩99  have alternatives := prime.right with x, hx, y, hy, preimage100  cases alternatives with leftMember | rightMember101  . left102    have data := idealComap.membership.forward with leftMember103    cc104  . right105    have data := idealComap.membership.forward with rightMember106    cc107108theorem IsRingHom.comap_prime_iff (J : Set)109  requires ideal : IsIdeal(B, plus, z, minus, times, J)110  shows IsPrimeIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J)) ↔ IsPrimeIdeal(B, plus, z, minus, times, unit, J)111proof112  constructor113  . intro prime114    exact IsRingHom.prime_of_comap with source, target, hom, onto, ideal, prime115  . intro prime116    exact IsRingHom.comap_prime with source, target, hom, prime117118theorem IsRingHom.map_prime (I : Set)119  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)120  requires contains : ringKernel(f, A, z) ⊆ I121  shows IsPrimeIdeal(B, plus, z, minus, times, unit, idealMap(f, B, I))122proof123  have ideal := IsPrimeIdeal.ideal with prime124  have image := IsRingHom.map_ideal with source, target, hom, onto, ideal125  have roundtrip := IsRingHom.comap_map_eq with source, target, hom, ideal, contains126  have preimage : IsPrimeIdeal(A, add, zero, neg, mul, one, idealComap(f, A, idealMap(f, B, I))) by rwa roundtrip127  exact IsRingHom.prime_of_comap with source, target, hom, onto, image, preimage128129theorem IsRingHom.comap_maximal (J : Set)130  requires maximal : IsMaximalIdeal(B, plus, z, minus, times, unit, J)131  shows IsMaximalIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J))132proof133  have proper := IsRingHom.comap_proper with source, target, hom, maximal.left134  have data := maximal.left135  have kernelIn := IsRingHom.kernel_subset_comap with source, target, hom, data.left136  have bounded := IsIdeal.subset_carrier with data.left137  have targetRoundtrip := idealMap.comap_eq with onto, bounded138  unfold IsMaximalIdeal139  refine ⟨proper, ?_⟩140  intros K properK inclusion141  have contains := Subset.transitive with kernelIn, inclusion142  have imageProper := IsRingHom.map_proper with source, target, hom, onto, properK, contains143  have imageInclusion := idealMap.monotone at f, B, idealComap(f, A, J), K with inclusion144  rw targetRoundtrip at imageInclusion145  have imageEqual := maximal.right with idealMap(f, B, K), imageProper, imageInclusion146  have sourceRoundtrip := IsRingHom.comap_map_eq with source, target, hom, properK.left, contains147  cc148149theorem IsRingHom.maximal_of_comap (J : Set)150  requires ideal : IsIdeal(B, plus, z, minus, times, J)151  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J))152  shows IsMaximalIdeal(B, plus, z, minus, times, unit, J)153proof154  have contains := IsRingHom.kernel_subset_comap with source, target, hom, ideal155  have proper := IsRingHom.map_proper with source, target, hom, onto, maximal.left, contains156  have bounded := IsIdeal.subset_carrier with ideal157  have roundtrip := idealMap.comap_eq with onto, bounded158  rw roundtrip at proper159  unfold IsMaximalIdeal160  refine ⟨proper, ?_⟩161  intros K properK inclusion162  have preimageProper := IsRingHom.comap_proper with source, target, hom,163    properK164  have preimageInclusion := idealComap.monotone at f, A, J, K with inclusion165  have preimageEqual := maximal.right with idealComap(f, A, K), preimageProper, preimageInclusion166  have boundedK := IsIdeal.subset_carrier with properK.left167  have roundtripK := idealMap.comap_eq with onto, boundedK168  cc169170theorem IsRingHom.comap_maximal_iff (J : Set)171  requires ideal : IsIdeal(B, plus, z, minus, times, J)172  shows IsMaximalIdeal(A, add, zero, neg, mul, one, idealComap(f, A, J)) ↔ IsMaximalIdeal(B, plus, z, minus, times, unit, J)173proof174  constructor175  . intro maximal176    exact IsRingHom.maximal_of_comap with source, target, hom, onto, ideal, maximal177  . intro maximal178    exact IsRingHom.comap_maximal with source, target, hom, onto, maximal179180theorem IsRingHom.map_maximal (I : Set)181  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)182  requires contains : ringKernel(f, A, z) ⊆ I183  shows IsMaximalIdeal(B, plus, z, minus, times, unit, idealMap(f, B, I))184proof185  have ideal := IsMaximalIdeal.ideal with maximal186  have image := IsRingHom.map_ideal with source, target, hom, onto, ideal187  have roundtrip := IsRingHom.comap_map_eq with source, target, hom, ideal, contains188  have preimage : IsMaximalIdeal(A, add, zero, neg, mul, one, idealComap(f, A, idealMap(f, B, I))) by rwa roundtrip189  exact IsRingHom.maximal_of_comap with source, target, hom, onto, image,190    preimage191192end Surjections193end RingMaps194195-- The same results for bundled rings.196section BundledRingMaps197variable (f R S : Set)198hypothesis source : CommRing(R)199hypothesis target : CommRing(S)200hypothesis hom : f : R →+* S201202theorem idealComap.proper (J : Set)203  requires proper : ProperIdeal(S, J)204  shows ProperIdeal(R, idealComap(f, R, J))205proof206  have sourceParts := CommRing.parts with source207  have targetParts := CommRing.parts with target208  have parts := RingHom.parts with hom209  have properParts := ProperIdeal.parts with proper210  have engine := IsRingHom.comap_proper with sourceParts, targetParts, parts,211    properParts212  exact ProperIdeal.of_projections with engine213214theorem idealComap.prime (J : Set)215  requires prime : PrimeIdeal(S, J)216  shows PrimeIdeal(R, idealComap(f, R, J))217proof218  have sourceParts := CommRing.parts with source219  have targetParts := CommRing.parts with target220  have parts := RingHom.parts with hom221  have primeParts := PrimeIdeal.parts with prime222  have engine := IsRingHom.comap_prime with sourceParts, targetParts, parts,223    primeParts224  exact PrimeIdeal.of_projections with engine225226section BundledSurjections227hypothesis onto : SurjectiveBetween(f, R.carrier, S.carrier)228229theorem idealMap.proper (I : Set)230  requires proper : ProperIdeal(R, I)231  requires contains : ker(f) ⊆ I232  shows ProperIdeal(S, idealMap(f, S, I))233proof234  have sourceParts := CommRing.parts with source235  have targetParts := CommRing.parts with target236  have parts := RingHom.parts with hom237  have properParts := ProperIdeal.parts with proper238  have engine := IsRingHom.map_proper with sourceParts, targetParts, parts, onto,239    properParts, contains240  exact ProperIdeal.of_projections with engine241242theorem idealMap.prime (I : Set)243  requires prime : PrimeIdeal(R, I)244  requires contains : ker(f) ⊆ I245  shows PrimeIdeal(S, idealMap(f, S, I))246proof247  have sourceParts := CommRing.parts with source248  have targetParts := CommRing.parts with target249  have parts := RingHom.parts with hom250  have primeParts := PrimeIdeal.parts with prime251  have engine := IsRingHom.map_prime with sourceParts, targetParts, parts, onto,252    primeParts, contains253  exact PrimeIdeal.of_projections with engine254255theorem idealMap.maximal (I : Set)256  requires maximal : MaximalIdeal(R, I)257  requires contains : ker(f) ⊆ I258  shows MaximalIdeal(S, idealMap(f, S, I))259proof260  have sourceParts := CommRing.parts with source261  have targetParts := CommRing.parts with target262  have parts := RingHom.parts with hom263  have maximalParts := MaximalIdeal.parts with maximal264  have engine := IsRingHom.map_maximal with sourceParts, targetParts, parts, onto,265    maximalParts, contains266  exact MaximalIdeal.of_projections with engine267268theorem idealComap.maximal (J : Set)269  requires maximal : MaximalIdeal(S, J)270  shows MaximalIdeal(R, idealComap(f, R, J))271proof272  have sourceParts := CommRing.parts with source273  have targetParts := CommRing.parts with target274  have parts := RingHom.parts with hom275  have maximalParts := MaximalIdeal.parts with maximal276  have engine := IsRingHom.comap_maximal with sourceParts, targetParts, parts,277    onto, maximalParts278  exact MaximalIdeal.of_projections with engine279280theorem idealComap.prime_iff (J : Set)281  requires ideal : Ideal(S, J)282  shows PrimeIdeal(R, idealComap(f, R, J)) ↔ PrimeIdeal(S, J)283proof284  have sourceParts := CommRing.parts with source285  have targetParts := CommRing.parts with target286  have parts := RingHom.parts with hom287  have idealParts := Ideal.parts with ideal288  have criterion := IsRingHom.comap_prime_iff with sourceParts, targetParts, parts,289    onto, idealParts290  constructor291  . intro prime292    have engine := criterion.forward with (PrimeIdeal.parts with prime)293    exact PrimeIdeal.of_projections with engine294  . intro prime295    have engine := criterion.backward with (PrimeIdeal.parts with prime)296    exact PrimeIdeal.of_projections with engine297298theorem idealComap.maximal_iff (J : Set)299  requires ideal : Ideal(S, J)300  shows MaximalIdeal(R, idealComap(f, R, J)) ↔ MaximalIdeal(S, J)301proof302  have sourceParts := CommRing.parts with source303  have targetParts := CommRing.parts with target304  have parts := RingHom.parts with hom305  have idealParts := Ideal.parts with ideal306  have criterion := IsRingHom.comap_maximal_iff with sourceParts, targetParts,307    parts, onto, idealParts308  constructor309  . intro maximal310    have engine := criterion.forward with (MaximalIdeal.parts with maximal)311    exact MaximalIdeal.of_projections with engine312  . intro maximal313    have engine := criterion.backward with (MaximalIdeal.parts with maximal)314    exact MaximalIdeal.of_projections with engine315316end BundledSurjections317end BundledRingMaps318