Grace/Cumulus/Algebra/Ring/Correspondence.g17

Open in Workbench Download source

Imports

Image

Declarations

Source

1-- Ideal images, inverse images, and correspondence under surjections.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.Correspondence8import Image910def idealComap (f A J : Set) : Set := {x ∈ A | f(x) ∈ J}11def idealMap (f B I : Set) : Set := functionImage(f, I, B)1213theorem idealMap.membership (f B I y : Set)14  shows y ∈ idealMap(f, B, I) ↔ y ∈ B ∧ ∃ x ∈ I, y = f(x)15proof16  simpa [idealMap] using functionImage.membership at f, I, B, y1718theorem idealMap.value (f A B I x : Set)19  requires function : f : A → B20  requires hx : x ∈ A21  requires member : x ∈ I22  shows f(x) ∈ idealMap(f, B, I)23proof24  have valueIn := FunctionBetween.apply_closed with function, hx25  exact idealMap.membership.backward with ⟨valueIn, x, member, rfl⟩2627theorem idealComap.monotone (f A I J : Set)28  requires subset : I ⊆ J29  shows idealComap(f, A, I) ⊆ idealComap(f, A, J)30proof31  intros x hx32  have data := idealComap.membership.forward with hx33  have mapped := subset with f(x), data.right34  exact idealComap.membership.backward with ⟨data.left, mapped⟩3536theorem idealMap.monotone (f B I J : Set)37  requires subset : I ⊆ J38  shows idealMap(f, B, I) ⊆ idealMap(f, B, J)39proof40  intros y hy41  obtain ⟨yIn, x, hx, shape⟩ := idealMap.membership.forward with hy42  have xIn := subset with x, hx43  exact idealMap.membership.backward with ⟨yIn, x, xIn, shape⟩4445theorem idealMap.galois (f A B I J : Set)46  requires function : f : A → B47  requires bounded : I ⊆ A48  shows idealMap(f, B, I) ⊆ J ↔ I ⊆ idealComap(f, A, J)49proof50  constructor51  . intros mapped x hx52    have xIn := bounded with x, hx53    have image := idealMap.value with function, xIn, hx54    have output := mapped with f(x), image55    exact idealComap.membership.backward with ⟨xIn, output⟩56  . intros included y hy57    obtain ⟨yIn, u, hu, shape⟩ := idealMap.membership.forward with hy58    have preimage := included with u, hu59    have data := idealComap.membership.forward with preimage60    rw shape61    exact data.right6263theorem idealMap.comap_eq (f A B J : Set)64  requires onto : SurjectiveBetween(f, A, B)65  requires bounded : J ⊆ B66  shows idealMap(f, B, idealComap(f, A, J)) = J67proof68  have function := Surjective.function with onto69  ext y70  constructor71  . intro hy72    obtain ⟨yIn, x, hx, shape⟩ := idealMap.membership.forward with hy73    have data := idealComap.membership.forward with hx74    rw shape75    exact data.right76  . intro hy77    have yIn := bounded with y, hy78    obtain ⟨u, hu, edge⟩ := onto.right with y, yIn79    have value := FunctionBetween.apply_value with *80    have preimage : u ∈ idealComap(f, A, J)81      apply idealComap.membership.backward82      refine ⟨hu, ?_⟩83      rwa value84    apply idealMap.membership.backward85    refine ⟨yIn, u, preimage, ?_⟩86    cc8788section RingMaps89variable (f A add zero neg mul one B plus z minus times unit : Set)90hypothesis source : IsCommRing(A, add, zero, neg, mul, one)91hypothesis target : IsCommRing(B, plus, z, minus, times, unit)92hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)9394theorem IsRingHom.comap_ideal (J : Set)95  requires ideal : IsIdeal(B, plus, z, minus, times, J)96  shows IsIdeal(A, add, zero, neg, mul, idealComap(f, A, J))97proof98  have function := IsRingHom.function with hom99  have ring := IsCommRing.ring with source100  have zeroIn := IsRing.zero_in_carrier with ring101  have zeroValue := IsRingHom.zero with hom102  have zeroMember := IsIdeal.zero_closed with ideal103  unfold IsIdeal104  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩105  . settle with Subset, idealComap.membership106  . apply idealComap.membership.backward at f, A, J, zero107    refine ⟨zeroIn, ?_⟩108    rwa zeroValue109  . intros x hx y hy110    have dx := idealComap.membership.forward with hx111    have dy := idealComap.membership.forward with hy112    have closed := IsRing.add_closed with ring, dx.left, dy.left113    have mapped := IsRingHom.add with hom, dx.left, dy.left114    have member := IsIdeal.add_closed with ideal, dx.right, dy.right115    apply idealComap.membership.backward116    refine ⟨closed, ?_⟩117    rwa mapped118  . intros x hx119    have data := idealComap.membership.forward with hx120    have closed := IsRing.neg_closed with ring, data.left121    have mapped := IsRingHom.neg with hom, data.left122    have member := IsIdeal.neg_closed with ideal, data.right123    apply idealComap.membership.backward124    refine ⟨closed, ?_⟩125    rwa mapped126  . intros a ha x hx127    have data := idealComap.membership.forward with hx128    have fa := IsRingHom.closed with hom, ha129    have leftClosed := IsRing.mul_closed with ring, ha, data.left130    have rightClosed := IsRing.mul_closed with ring, data.left, ha131    have leftValue := IsRingHom.mul with hom, ha, data.left132    have rightValue := IsRingHom.mul with hom, data.left, ha133    have leftMember := IsIdeal.mul_left_closed with ideal, data.right134    have rightMember := IsIdeal.mul_right_closed with ideal, data.right135    constructor136    . apply idealComap.membership.backward at f, A, J, call2(mul, a, x)137      refine ⟨leftClosed, ?_⟩138      rwa leftValue139    . apply idealComap.membership.backward at f, A, J, call2(mul, x, a)140      refine ⟨rightClosed, ?_⟩141      rwa rightValue142143theorem IsRingHom.kernel_subset_comap (J : Set)144  requires ideal : IsIdeal(B, plus, z, minus, times, J)145  shows ringKernel(f, A, z) ⊆ idealComap(f, A, J)146proof147  have zeroMember := IsIdeal.zero_closed with ideal148  intros x hx149  have data := ringKernel.membership.forward with hx150  apply idealComap.membership.backward151  refine ⟨data.left, ?_⟩152  rwa data.right153154theorem IsRingHom.comap_map_eq (I : Set)155  requires ideal : IsIdeal(A, add, zero, neg, mul, I)156  requires contains : ringKernel(f, A, z) ⊆ I157  shows idealComap(f, A, idealMap(f, B, I)) = I158proof159  have function := IsRingHom.function with hom160  have bounded := IsIdeal.subset_carrier with ideal161  have included := contains162  ext x163  constructor164  . intro hx165    obtain ⟨xIn, imageMember⟩ := idealComap.membership.forward with hx166    obtain ⟨fxIn, y, hy, images⟩ := idealMap.membership.forward with imageMember167    have yIn := bounded with y, hy168    have congruent := IsRingHom.kernel_congruent.backward with source, target, hom, xIn, yIn, images169    have difference := included with call2(add, x, neg(y)), congruent170    have sum := IsIdeal.add_closed with ideal, difference, hy171    ring_nf at sum172    exact sum173  . intro hx174    have xIn := bounded with x, hx175    have image := idealMap.value with function, xIn, hx176    exact idealComap.membership.backward with ⟨xIn, image⟩177178section Surjections179hypothesis onto : SurjectiveBetween(f, A, B)180181theorem IsRingHom.map_ideal (I : Set)182  requires ideal : IsIdeal(A, add, zero, neg, mul, I)183  shows IsIdeal(B, plus, z, minus, times, idealMap(f, B, I))184proof185  have function := IsRingHom.function with hom186  have ring := IsCommRing.ring with source187  have bounded := IsIdeal.subset_carrier with ideal188  have ontoLaw := onto189  have zeroMember := IsIdeal.zero_closed with ideal190  have zeroIn := bounded with zero, zeroMember191  have zeroImage := idealMap.value with function, zeroIn, zeroMember192  have zeroValue := IsRingHom.zero with hom193  unfold IsIdeal194  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩195    intros y hy196    have data := idealMap.membership.forward with hy197    exact data.left198  . cc199  . intros y hy w hw200    obtain ⟨yIn, a, ha, sy⟩ := idealMap.membership.forward with hy201    obtain ⟨wIn, b, hb, sw⟩ := idealMap.membership.forward with hw202    have aIn := bounded with a, ha203    have bIn := bounded with b, hb204    have closed := IsRing.add_closed with ring, aIn, bIn205    have member := IsIdeal.add_closed with ideal, ha, hb206    have mapped := IsRingHom.add with hom, aIn, bIn207    have image := idealMap.value with function, closed, member208    cc209  . intros y hy210    obtain ⟨yIn, c, hc, shape⟩ := idealMap.membership.forward with hy211    have cIn := bounded with c, hc212    have closed := IsRing.neg_closed with ring, cIn213    have member := IsIdeal.neg_closed with ideal, hc214    have mapped := IsRingHom.neg with hom, cIn215    have image := idealMap.value with function, closed, member216    cc217  . intros b hb y hy218    obtain ⟨u, hu, edge⟩ := ontoLaw.right with b, hb219    have value := FunctionBetween.apply_value with *220    obtain ⟨yIn, x, hx, shape⟩ := idealMap.membership.forward with hy221    have xIn := bounded with x, hx222    have leftClosed := IsRing.mul_closed with ring, hu, xIn223    have rightClosed := IsRing.mul_closed with ring, xIn, hu224    have leftMember := IsIdeal.mul_left_closed with ideal, hu, hx225    have rightMember := IsIdeal.mul_right_closed with ideal, hu, hx226    have leftValue := IsRingHom.mul with hom, hu, xIn227    have rightValue := IsRingHom.mul with hom, xIn, hu228    have leftImage := idealMap.value with function, leftClosed, leftMember229    have rightImage := idealMap.value with function, rightClosed, rightMember230    constructor231    . cc232    . cc233234-- The two assignments preserve ideals and are mutually inverse on their domains.235theorem IsRingHom.ideal_correspondence236  shows237    (∀ J, IsIdeal(B, plus, z, minus, times, J) →238      IsIdeal(A, add, zero, neg, mul, idealComap(f, A, J)) ∧239      ringKernel(f, A, z) ⊆ idealComap(f, A, J) ∧240      idealMap(f, B, idealComap(f, A, J)) = J) ∧241    (∀ I, IsIdeal(A, add, zero, neg, mul, I) → ringKernel(f, A, z) ⊆ I →242      IsIdeal(B, plus, z, minus, times, idealMap(f, B, I)) ∧243      idealComap(f, A, idealMap(f, B, I)) = I)244proof245  constructor246  . intros J ideal247    have preimage := IsRingHom.comap_ideal with source, target, hom, ideal248    have contains := IsRingHom.kernel_subset_comap with source, target, hom,249      ideal250    have bounded := IsIdeal.subset_carrier with ideal251    have roundtrip := idealMap.comap_eq with onto, bounded252    refine ⟨preimage, contains, roundtrip⟩253  . intros I ideal contains254    have image := IsRingHom.map_ideal with source, target, hom, onto, ideal255    have roundtrip := IsRingHom.comap_map_eq with source, target, hom, ideal, contains256    refine ⟨image, roundtrip⟩257258end Surjections259260end RingMaps261section QuotientIdeals262variable (A add zero neg mul one I : Set)263hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)264hypothesis ideal : IsIdeal(A, add, zero, neg, mul, I)265266theorem idealQuotient.kernel_eq267  shows ringKernel(quotientProjection(A, idealRelation(A, add, neg, I)), A, ⟦zero⟧[A, idealRelation(A, add, neg, I)]) = I268proof269  have bounded := IsIdeal.subset_carrier with ideal270  ext x271  constructor272  . intro hx273    have data := ringKernel.membership.forward with hx274    exact idealQuotient.projection_kernel.forward with ring, ideal, data.left, data.right275  . intro hx276    have xIn := bounded with x, hx277    have value := idealQuotient.projection_kernel.backward with ring, ideal, xIn, hx278    exact ringKernel.membership.backward with ⟨xIn, value⟩279280theorem idealQuotient.comap_map_eq (J : Set)281  requires idealJ : IsIdeal(A, add, zero, neg, mul, J)282  requires contains : I ⊆ J283  shows idealComap(quotientProjection(A, idealRelation(A, add, neg, I)), A, idealMap(quotientProjection(A, idealRelation(A, add, neg, I)), (A ⧸ idealRelation(A, add, neg, I)), J)) = J284proof285  have quotientRing := idealQuotient.comm_ring with ring, ideal286  have projection := idealQuotient.projection_hom with ring, ideal287  have kernel := idealQuotient.kernel_eq with ring, ideal288  have containsKernel : ringKernel(quotientProjection(A, idealRelation(A, add, neg, I)), A, ⟦zero⟧[A, idealRelation(A, add, neg, I)]) ⊆ J289    rwa kernel290  exact IsRingHom.comap_map_eq with ring, quotientRing, projection, idealJ, containsKernel291292end QuotientIdeals293294-- The same results for bundled rings.295section BundledRingMaps296variable (f R S : Set)297hypothesis source : CommRing(R)298hypothesis target : CommRing(S)299hypothesis hom : f : R →+* S300301theorem idealComap.ideal (J : Set)302  requires ideal : Ideal(S, J)303  shows Ideal(R, idealComap(f, R, J))304proof305  have sourceParts := CommRing.parts with source306  have targetParts := CommRing.parts with target307  have parts := RingHom.parts with hom308  have idealParts := Ideal.parts with ideal309  have engine := IsRingHom.comap_ideal with sourceParts, targetParts, parts,310    idealParts311  exact Ideal.of_projections with engine312313theorem idealComap.kernel_subset (J : Set)314  requires ideal : Ideal(S, J)315  shows ker(f) ⊆ idealComap(f, R, J)316proof317  have sourceParts := CommRing.parts with source318  have targetParts := CommRing.parts with target319  have parts := RingHom.parts with hom320  have idealParts := Ideal.parts with ideal321  exact IsRingHom.kernel_subset_comap with sourceParts, targetParts, parts,322    idealParts323324theorem idealComap.map_eq (I : Set)325  requires ideal : Ideal(R, I)326  requires contains : ker(f) ⊆ I327  shows idealComap(f, R, idealMap(f, S, I)) = I328proof329  have sourceParts := CommRing.parts with source330  have targetParts := CommRing.parts with target331  have parts := RingHom.parts with hom332  have idealParts := Ideal.parts with ideal333  exact IsRingHom.comap_map_eq with sourceParts, targetParts, parts, idealParts,334    contains335336section BundledSurjections337hypothesis onto : SurjectiveBetween(f, R.carrier, S.carrier)338339theorem idealMap.ideal (I : Set)340  requires ideal : Ideal(R, I)341  shows Ideal(S, idealMap(f, S, I))342proof343  have sourceParts := CommRing.parts with source344  have targetParts := CommRing.parts with target345  have parts := RingHom.parts with hom346  have idealParts := Ideal.parts with ideal347  have engine := IsRingHom.map_ideal with sourceParts, targetParts, parts, onto,348    idealParts349  exact Ideal.of_projections with engine350351-- The ideals of S correspond to the ideals of R containing the kernel.352theorem RingHom.correspondence353  shows354    (∀ J, Ideal(S, J) →355      Ideal(R, idealComap(f, R, J)) ∧356      ker(f) ⊆ idealComap(f, R, J) ∧357      idealMap(f, S, idealComap(f, R, J)) = J) ∧358    (∀ I, Ideal(R, I) → ker(f) ⊆ I →359      Ideal(S, idealMap(f, S, I)) ∧360      idealComap(f, R, idealMap(f, S, I)) = I)361proof362  constructor363  . intros J ideal364    have preimage := idealComap.ideal with source, target, hom, ideal365    have contains := idealComap.kernel_subset with source, target, hom, ideal366    have bounded := Ideal.subset with ideal367    have roundtrip := idealMap.comap_eq with onto, bounded368    refine ⟨preimage, contains, roundtrip⟩369  . intros I ideal contains370    have image := idealMap.ideal with source, target, hom, onto, ideal371    have roundtrip := idealComap.map_eq with source, target, hom, ideal, contains372    refine ⟨image, roundtrip⟩373374end BundledSurjections375end BundledRingMaps376377section BundledQuotientIdeals378variable (R I : Set)379hypothesis comm : CommRing(R)380hypothesis ideal : Ideal(R, I)381382theorem quotientRing.projection_kernel383  shows ringKernel(quotientProjection(R.carrier, quotientRelation(R, I)), R,384    Ring.zero(R ⧸ I)) = I385proof386  have parts := CommRing.parts with comm387  have idealParts := Ideal.parts with ideal388  have engine := idealQuotient.kernel_eq with parts, idealParts389  rw [quotientRing.zeroOf, quotientRelation.value]390  exact engine391392end BundledQuotientIdeals393