Grace/Cumulus/Algebra/Ring/QuotientCore.g17

Open in Workbench Download source

Imports

PrimeIdealCore · Relation.QuotientOperations

Declarations

Source

1-- Ideal congruences and quotient rings over separate pieces, constructed2-- in ZF: the engine under Quotient3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Ring.QuotientCore9import PrimeIdealCore10import Relation.QuotientOperations1112predicate Congruent (add neg I x y : Set) := call2(add, x, neg(y)) ∈ I1314theorem Congruent.refl (A add zero neg mul one I x : Set)15  requires ring : IsCommRing(A, add, zero, neg, mul, one)16  requires ideal : IsIdeal(A, add, zero, neg, mul, I)17  requires hx : x ∈ A18  shows Congruent(add, neg, I, x, x)19proof20  have zeroIn : zero ∈ I by simp [IsIdeal]21  have cancel : call2(add, x, neg(x)) = zero by ring22  unfold Congruent23  rwa cancel2425theorem Congruent.symm (A add zero neg mul one I x y : Set)26  requires ring : IsCommRing(A, add, zero, neg, mul, one)27  requires ideal : IsIdeal(A, add, zero, neg, mul, I)28  requires hx : x ∈ A29  requires hy : y ∈ A30  requires same : Congruent(add, neg, I, x, y)31  shows Congruent(add, neg, I, y, x)32proof33  have negative := IsIdeal.neg_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)) with *34  unfold Congruent35  ring_nf at negative36  ring_nf37  exact negative3839theorem Congruent.trans (A add zero neg mul one I x y z : Set)40  requires ring : IsCommRing(A, add, zero, neg, mul, one)41  requires ideal : IsIdeal(A, add, zero, neg, mul, I)42  requires hx : x ∈ A43  requires hy : y ∈ A44  requires hz : z ∈ A45  requires xy : Congruent(add, neg, I, x, y)46  requires yz : Congruent(add, neg, I, y, z)47  shows Congruent(add, neg, I, x, z)48proof49  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)), call2(add, y, neg(z)) with *50  unfold Congruent51  ring_nf at sum52  ring_nf53  exact sum5455theorem Congruent.add (A add zero neg mul one I x y u v : Set)56  requires ring : IsCommRing(A, add, zero, neg, mul, one)57  requires ideal : IsIdeal(A, add, zero, neg, mul, I)58  requires hx : x ∈ A59  requires hy : y ∈ A60  requires hu : u ∈ A61  requires hv : v ∈ A62  requires xy : Congruent(add, neg, I, x, y)63  requires uv : Congruent(add, neg, I, u, v)64  shows Congruent(add, neg, I, call2(add, x, u), call2(add, y, v))65proof66  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)), call2(add, u, neg(v)) with *67  unfold Congruent68  ring_nf at sum69  ring_nf70  exact sum7172theorem Congruent.neg (A add zero neg mul one I x y : Set)73  requires ring : IsCommRing(A, add, zero, neg, mul, one)74  requires ideal : IsIdeal(A, add, zero, neg, mul, I)75  requires hx : x ∈ A76  requires hy : y ∈ A77  requires xy : Congruent(add, neg, I, x, y)78  shows Congruent(add, neg, I, neg(x), neg(y))79proof80  have negative := IsIdeal.neg_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)) with *81  unfold Congruent82  ring_nf at negative83  ring_nf84  exact negative8586theorem Congruent.mul (A add zero neg mul one I x y u v : Set)87  requires ring : IsCommRing(A, add, zero, neg, mul, one)88  requires ideal : IsIdeal(A, add, zero, neg, mul, I)89  requires hx : x ∈ A90  requires hy : y ∈ A91  requires hu : u ∈ A92  requires hv : v ∈ A93  requires xy : Congruent(add, neg, I, x, y)94  requires uv : Congruent(add, neg, I, u, v)95  shows Congruent(add, neg, I, call2(mul, x, u), call2(mul, y, v))96proof97  have first := IsIdeal.mul_left_closed at A, add, zero, neg, mul, I, u, call2(add, x, neg(y)) with *98  have second := IsIdeal.mul_left_closed at A, add, zero, neg, mul, I, y, call2(add, u, neg(v)) with *99  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, I, call2(mul, u, call2(add, x, neg(y))), call2(mul, y, call2(add, u, neg(v))) with *100  unfold Congruent101  ring_nf at sum102  ring_nf103  exact sum104105def idealRelation (A add neg I : Set) : Set :=106  {p ∈ A × A | ∃ x ∈ A, ∃ y ∈ A, p = (x, y) ∧ Congruent(add, neg, I, x, y)}107108notation scoped idealRelation(R, I) => idealRelation(R.carrier, R.add, R.neg, I)109110theorem idealRelation.relates (A add neg I x y : Set)111  requires hx : x ∈ A112  requires hy : y ∈ A113  shows relates(idealRelation(A, add, neg, I), x, y) ↔ Congruent(add, neg, I, x, y)114proof115  constructor116  . intro related117    obtain ⟨bounded, u, hu, v, hv, shape, same⟩ := idealRelation.membership.forward at118      A, add, neg, I, (x, y) with related119    have coordinates := orderedPair.injective with shape120    rwa [coordinates.left, coordinates.right]121  . intro same122    unfold relates123    apply idealRelation.membership.backward124    have bounded := product.pair at x, y, A, A with *125    refine ⟨bounded, x, hx, y, hy, rfl, same⟩126127theorem idealRelation.equivalence (A add zero neg mul one I : Set)128  requires ring : IsCommRing(A, add, zero, neg, mul, one)129  requires ideal : IsIdeal(A, add, zero, neg, mul, I)130  shows Equivalence(A, idealRelation(A, add, neg, I))131proof132  unfold Equivalence133  refine ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩134  . settle with RelationOn, RelationBetween, Subset, idealRelation.membership135    intros x hx136    apply idealRelation.relates.backward with hx, hx137    exact Congruent.refl with *138    intros x hx y hy related139    have same := idealRelation.relates.forward with hx, hy, related140    have reverse := Congruent.symm with *141    exact idealRelation.relates.backward with hy, hx, reverse142    intros x hx y hy z hz xy yz143    have first := idealRelation.relates.forward with hx, hy, xy144    have second := idealRelation.relates.forward with hy, hz, yz145    have composed := Congruent.trans at A, add, zero, neg, mul, one, I, x, y, z with *146    exact idealRelation.relates.backward with hx, hz, composed147148theorem idealRelation.add_compatible (A add zero neg mul one I : Set)149  requires ring : IsCommRing(A, add, zero, neg, mul, one)150  requires ideal : IsIdeal(A, add, zero, neg, mul, I)151  shows CompatibleBinary(A, idealRelation(A, add, neg, I), add)152proof153  intros x hx y hy u hu v hv xy uv154  have first := idealRelation.relates.forward with hx, hy, xy155  have second := idealRelation.relates.forward with hu, hv, uv156  have congruence := Congruent.add at A, add, zero, neg, mul, one, I, x, y, u, v with *157  have ordinary := IsCommRing.ring with ring158  have leftClosed := IsRing.add_closed at A, add, zero, neg, mul, one, x,159    u with *160  have rightClosed := IsRing.add_closed at A, add, zero, neg, mul, one, y, v with *161  exact idealRelation.relates.backward with leftClosed, rightClosed, congruence162163theorem idealRelation.neg_compatible (A add zero neg mul one I : Set)164  requires ring : IsCommRing(A, add, zero, neg, mul, one)165  requires ideal : IsIdeal(A, add, zero, neg, mul, I)166  shows CompatibleUnary(A, idealRelation(A, add, neg, I), neg)167proof168  intros x hx y hy xy169  have first := idealRelation.relates.forward with hx, hy, xy170  have congruence := Congruent.neg with *171  have ordinary := IsCommRing.ring with ring172  have leftClosed := IsRing.neg_closed with hx173  have rightClosed := IsRing.neg_closed with hy174  exact idealRelation.relates.backward with leftClosed, rightClosed, congruence175176theorem idealRelation.mul_compatible (A add zero neg mul one I : Set)177  requires ring : IsCommRing(A, add, zero, neg, mul, one)178  requires ideal : IsIdeal(A, add, zero, neg, mul, I)179  shows CompatibleBinary(A, idealRelation(A, add, neg, I), mul)180proof181  intros x hx y hy u hu v hv xy uv182  have first := idealRelation.relates.forward with hx, hy, xy183  have second := idealRelation.relates.forward with hu, hv, uv184  have congruence := Congruent.mul at A, add, zero, neg, mul, one, I, x, y, u, v with *185  have ordinary := IsCommRing.ring with ring186  have leftClosed := IsRing.mul_closed at A, add, zero, neg, mul, one, x,187    u with *188  have rightClosed := IsRing.mul_closed at A, add, zero, neg, mul, one, y, v with *189  exact idealRelation.relates.backward with leftClosed, rightClosed, congruence190191-- A ring on the quotient set, with graph-valued operations.192theorem idealQuotient.comm_ring (A add zero neg mul one I : Set)193  requires ring : IsCommRing(A, add, zero, neg, mul, one)194  requires ideal : IsIdeal(A, add, zero, neg, mul, I)195  shows IsCommRing((A ⧸ idealRelation(A, add, neg, I)),196    quotientBinary(A, idealRelation(A, add, neg, I), add),197    ⟦zero⟧[A, idealRelation(A, add, neg, I)],198    quotientUnary(A, idealRelation(A, add, neg, I), neg),199    quotientBinary(A, idealRelation(A, add, neg, I), mul),200    ⟦one⟧[A, idealRelation(A, add, neg, I)])201proof202  have equivalence := idealRelation.equivalence with *203  have addCompatible := idealRelation.add_compatible with *204  have mulCompatible := idealRelation.mul_compatible with *205  have negCompatible := idealRelation.neg_compatible with *206  exact quotient.comm_ring with *207208theorem idealClass.eq_iff_congruent (A add zero neg mul one I x y : Set)209  requires ring : IsCommRing(A, add, zero, neg, mul, one)210  requires ideal : IsIdeal(A, add, zero, neg, mul, I)211  requires hx : x ∈ A212  requires hy : y ∈ A213  shows ⟦x⟧[A, idealRelation(A, add, neg, I)] = ⟦y⟧[A, idealRelation(A, add, neg, I)] ↔214    Congruent(add, neg, I, x, y)215proof216  have equivalence := idealRelation.equivalence with *217  constructor218  . intro equal219    have related := equivalenceClass.related_of_eq with *220    exact idealRelation.relates.forward with hx, hy, related221  . intro same222    have related := idealRelation.relates.backward with hx, hy, same223    exact equivalenceClass.eq with *224225theorem idealClass.eq_zero (A add zero neg mul one I x : Set)226  requires ring : IsCommRing(A, add, zero, neg, mul, one)227  requires ideal : IsIdeal(A, add, zero, neg, mul, I)228  requires hx : x ∈ A229  shows ⟦x⟧[A, idealRelation(A, add, neg, I)] = ⟦zero⟧[A, idealRelation(A, add, neg, I)] ↔ x ∈ I230proof231  have ordinary := IsCommRing.ring with ring232  have zeroInA := IsRing.zero_in_carrier with ordinary233  have equivalence := idealRelation.equivalence with *234  have subtractZero : call2(add, x, neg(zero)) = x by ring235  constructor236  . intro equal237    have related := equivalenceClass.related_of_eq with *238    have same := idealRelation.relates.forward with hx, zeroInA, related239    unfold Congruent at same240    rwa subtractZero at same241  . intro member242    have same : Congruent(add, neg, I, x, zero)243      unfold Congruent244      rwa subtractZero245    have related := idealRelation.relates.backward with hx, zeroInA, same246    exact equivalenceClass.eq with *247248theorem idealQuotient.nontrivial_iff (A add zero neg mul one I : Set)249  requires ring : IsCommRing(A, add, zero, neg, mul, one)250  requires ideal : IsIdeal(A, add, zero, neg, mul, I)251  shows Nontrivial((A ⧸ idealRelation(A, add, neg, I)), ⟦zero⟧[A, idealRelation(A, add, neg, I)], ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔252    IsProperIdeal(A, add, zero, neg, mul, one, I)253proof254  have ordinary := IsCommRing.ring with ring255  have zeroInA := IsRing.zero_in_carrier with ordinary256  have monoid := IsRing.multiplicative with ordinary257  have oneInA := IsMonoid.unit_in_carrier with monoid258  have equivalence := idealRelation.equivalence with *259  have zeroIn := quotient.contains_class at A, idealRelation(A, add, neg, I), zero with *260  have oneIn := quotient.contains_class at A, idealRelation(A, add, neg, I), one with *261  have criterion := idealClass.eq_zero at A, add, zero, neg, mul, one, I, one with *262  constructor263  . intro nontrivial264    unfold IsProperIdeal265    refine ⟨ideal, ?_⟩266    intro member267    have equal := criterion.backward with member268    apply nontrivial.right.right269    symm270    exact equal271  . intro proper272    unfold Nontrivial273    refine ⟨zeroIn, oneIn, ?_⟩274    intro equal275    have reversed : ⟦one⟧[A, idealRelation(A, add, neg, I)] = ⟦zero⟧[A, idealRelation(A, add, neg, I)]276      symm277      exact equal278    have member := criterion.forward with reversed279    exact proper.right with member280281theorem idealQuotient.domain_of_prime (A add zero neg mul one I : Set)282  requires ring : IsCommRing(A, add, zero, neg, mul, one)283  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)284  shows IsIntegralDomain((A ⧸ idealRelation(A, add, neg, I)),285    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],286    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])287proof288  have proper := IsPrimeIdeal.proper with prime289  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsProperIdeal]290  have ordinary := IsCommRing.ring with ring291  have equivalence := idealRelation.equivalence with *292  have compatible := idealRelation.mul_compatible with *293  have closed : IsMagma(A, mul) by simp [IsRing, IsMonoid, IsSemigroup]294  have quotientRing := idealQuotient.comm_ring with *295  have nontrivial := idealQuotient.nontrivial_iff.backward with ring, ideal, proper296  unfold IsIntegralDomain297  refine ⟨quotientRing, nontrivial, ?_⟩298  intros X hX Y hY productZero299  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX300  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY301  have multiply := quotientBinary.classes with equivalence, closed, compatible, hx, hy302  have productInA := IsRing.mul_closed with hx, hy303  have zeroProduct : ⟦call2(mul, x, y)⟧[A, idealRelation(A, add, neg, I)] = ⟦zero⟧[A, idealRelation(A, add, neg, I)]304    cc305  have productIn := idealClass.eq_zero.forward with ring, ideal, productInA, zeroProduct306  have factors := prime.right with x, hx, y, hy, productIn307  cases factors with xIn | yIn308  . left309    have equal := idealClass.eq_zero.backward with ring, ideal, hx, xIn310    cc311  . right312    have equal := idealClass.eq_zero.backward with ring, ideal, hy, yIn313    cc314315theorem idealQuotient.domain_iff_prime (A add zero neg mul one I : Set)316  requires ring : IsCommRing(A, add, zero, neg, mul, one)317  requires ideal : IsIdeal(A, add, zero, neg, mul, I)318  shows IsIntegralDomain((A ⧸ idealRelation(A, add, neg, I)),319    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],320    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔ IsPrimeIdeal(A, add, zero, neg, mul, one, I)321proof322  constructor323  . intro domain324    have proper := idealQuotient.nontrivial_iff.forward with ring, ideal, domain.right.left325    have factors := domain.right.right326    have ordinary := IsCommRing.ring with ring327    have equivalence := idealRelation.equivalence with *328    have compatible := idealRelation.mul_compatible with *329    have closed : IsMagma(A, mul) by simp [IsRing, IsMonoid, IsSemigroup]330    unfold IsPrimeIdeal331    refine ⟨proper, ?_⟩332    intros x hx y hy productIn333    have xIn := quotient.contains_class with hx334    have yIn := quotient.contains_class with hy335    have productInA := IsRing.mul_closed with hx, hy336    have zeroProduct := idealClass.eq_zero.backward with ring, ideal, productInA, productIn337    have multiply := quotientBinary.classes with hx, hy338    have equation : (quotientBinary(A, idealRelation(A, add, neg, I), mul))(⟦x⟧[A, idealRelation(A, add, neg, I)], ⟦y⟧[A, idealRelation(A, add, neg, I)]) = ⟦zero⟧[A, idealRelation(A, add, neg, I)]339      cc340    have alternatives := factors with ⟦x⟧[A, idealRelation(A, add, neg, I)], xIn, ⟦y⟧[A, idealRelation(A, add, neg, I)], yIn, equation341    cases alternatives with xZero | yZero342    . left343      exact idealClass.eq_zero.forward with ring, ideal, hx, xZero344    . right345      exact idealClass.eq_zero.forward with ring, ideal, hy, yZero346  . intro prime347    exact idealQuotient.domain_of_prime with *348349theorem idealQuotient.projection_kernel (A add zero neg mul one I x : Set)350  requires ring : IsCommRing(A, add, zero, neg, mul, one)351  requires ideal : IsIdeal(A, add, zero, neg, mul, I)352  requires hx : x ∈ A353  shows quotientProjection(A, idealRelation(A, add, neg, I))[x] =354    ⟦zero⟧[A, idealRelation(A, add, neg, I)] ↔ x ∈ I355proof356  have equivalence := idealRelation.equivalence with *357  have value := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *358  rw value359  exact idealClass.eq_zero with *360