Grace/Cumulus/Algebra/Ring/Quotient.g17

Open in Workbench Download source

Imports

QuotientCore · PrimeIdeal

Declarations

Source

1-- Quotient rings of a bundled ring: the congruence modulo an ideal, the2-- quotient ring R ⧸ I (the value quotientRing(R, I)) on its classes, the ring laws of the3-- quotient, and the classes of sums, products, and negations; everything4-- here is ZF5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.Quotient11import QuotientCore12import PrimeIdeal1314-- x and y are related modulo I when x - y lies in I.15def quotientRelation (R I : Set) : Set :=16  idealRelation(R.carrier, R.add, R.neg, I)1718-- The quotient ring of R by I: the classes modulo I with the induced19-- operations and the classes of zero and one.20def quotientRing (R I : Set) : Set :=21  Ring.mk((R.carrier ⧸ quotientRelation(R, I)),22    quotientBinary(R.carrier, quotientRelation(R, I), R.add),23    ⟦R.zero⟧[R.carrier, quotientRelation(R, I)],24    quotientUnary(R.carrier, quotientRelation(R, I), R.neg),25    quotientBinary(R.carrier, quotientRelation(R, I), R.mul),26    ⟦R.one⟧[R.carrier, quotientRelation(R, I)])2728-- The quotient is written R ⧸ I wherever R is the ring of a hypothesis in29-- scope; the set quotient A ⧸ r keeps its meaning on every other left30-- operand.31notation infixl 70 "⧸" => quotientRing(R, _) via hypothesis Ring(R) for R32notation infixl 70 "⧸" => quotientRing(R, _) via hypothesis CommRing(R) for R33notation infixl 70 "⧸" => quotientRing(R, _) via hypothesis Ideal(R, I) for R3435theorem quotientRelation.value (R I : Set)36  shows quotientRelation(R, I) = idealRelation(R.carrier, R.add, R.neg, I)37proof38  simp [quotientRelation]3940theorem quotientRing.carrierOf (R I : Set)41  shows Ring.carrier(quotientRing(R, I)) =42    (R.carrier ⧸ quotientRelation(R, I))43proof44  simp [quotientRing, Ring.mk.carrier]4546theorem quotientRing.addOf (R I : Set)47  shows Ring.add(quotientRing(R, I)) =48    quotientBinary(R.carrier, quotientRelation(R, I), R.add)49proof50  simp [quotientRing, Ring.mk.add]5152theorem quotientRing.zeroOf (R I : Set)53  shows Ring.zero(quotientRing(R, I)) =54    ⟦R.zero⟧[R.carrier, quotientRelation(R, I)]55proof56  simp [quotientRing, Ring.mk.zero]5758theorem quotientRing.negOf (R I : Set)59  shows Ring.neg(quotientRing(R, I)) =60    quotientUnary(R.carrier, quotientRelation(R, I), R.neg)61proof62  simp [quotientRing, Ring.mk.neg]6364theorem quotientRing.mulOf (R I : Set)65  shows Ring.mul(quotientRing(R, I)) =66    quotientBinary(R.carrier, quotientRelation(R, I), R.mul)67proof68  simp [quotientRing, Ring.mk.mul]6970theorem quotientRing.oneOf (R I : Set)71  shows Ring.one(quotientRing(R, I)) =72    ⟦R.one⟧[R.carrier, quotientRelation(R, I)]73proof74  simp [quotientRing, Ring.mk.one]7576section QuotientRings77variable (R I : Set)78hypothesis comm : CommRing(R)79hypothesis ideal : Ideal(R, I)8081theorem quotientRelation.relates (x y : R)82  shows relates(quotientRelation(R, I), x, y) ↔ x - y ∈ I83proof84  have xIn : x ∈ R by assumption85  have yIn : y ∈ R by assumption86  have criterion := idealRelation.relates at R.carrier, R.add, R.neg, I, x, y87    with xIn, yIn88  rw [quotientRelation.value, Ring.sub.value]89  constructor90  . intro related91    have same := criterion.forward with related92    unfold Congruent at same93    exact same94  . intro member95    have same : Congruent(R.add, R.neg, I, x, y)96      unfold Congruent97      exact member98    exact criterion.backward with same99100theorem quotientRelation.equivalence101  shows Equivalence(R.carrier, quotientRelation(R, I))102proof103  have parts := CommRing.parts with comm104  have idealParts := Ideal.parts with ideal105  rw quotientRelation.value106  exact idealRelation.equivalence with parts, idealParts107108-- The quotient is a commutative ring.109theorem quotientRing.comm_ring110  shows CommRing(R ⧸ I)111proof112  have parts := CommRing.parts with comm113  have idealParts := Ideal.parts with ideal114  have engine := idealQuotient.comm_ring with parts, idealParts115  unfold quotientRing116  apply CommRing.of_parts117  rw quotientRelation.value118  exact engine119120instance quotientRing.class_mem (x : R)121  shows ⟦x⟧[R.carrier, quotientRelation(R, I)] ∈122    Ring.carrier(R ⧸ I)123proof124  have equivalence := quotientRelation.equivalence with comm, ideal125  rw quotientRing.carrierOf126  exact quotient.contains_class with equivalence, *127128theorem quotientRing.representative (X : Set)129  requires hX : X ∈ Ring.carrier(R ⧸ I)130  shows ∃ x ∈ R, X = ⟦x⟧[R.carrier, quotientRelation(R, I)]131proof132  rw quotientRing.carrierOf at hX133  exact quotient.representative with hX134135-- Two classes are equal exactly when the difference of representatives136-- lies in the ideal; a class is zero exactly when its representative does.137theorem quotientRing.class_eq_iff (x y : R)138  shows ⟦x⟧[R.carrier, quotientRelation(R, I)] =139    ⟦y⟧[R.carrier, quotientRelation(R, I)] ↔ x - y ∈ I140proof141  have parts := CommRing.parts with comm142  have idealParts := Ideal.parts with ideal143  have xIn : x ∈ R by assumption144  have yIn : y ∈ R by assumption145  have criterion := idealClass.eq_iff_congruent with parts, idealParts, xIn, yIn146  rw [quotientRelation.value, Ring.sub.value]147  constructor148  . intro equal149    have same := criterion.forward with equal150    unfold Congruent at same151    exact same152  . intro member153    have same : Congruent(R.add, R.neg, I, x, y)154      unfold Congruent155      exact member156    exact criterion.backward with same157158theorem quotientRing.class_eq_zero_iff (x : R)159  shows ⟦x⟧[R.carrier, quotientRelation(R, I)] =160    ⟦R[0]⟧[R.carrier, quotientRelation(R, I)] ↔ x ∈ I161proof162  have parts := CommRing.parts with comm163  have idealParts := Ideal.parts with ideal164  have xIn : x ∈ R by assumption165  rw quotientRelation.value166  exact idealClass.eq_zero with parts, idealParts, xIn167168-- The operations on classes are the classes of the operations.169theorem quotientRing.add_class (x y : R)170  shows Ring.add(R ⧸ I)(⟦x⟧[R.carrier, quotientRelation(R, I)],171      ⟦y⟧[R.carrier, quotientRelation(R, I)]) =172    ⟦x + y⟧[R.carrier, quotientRelation(R, I)]173proof174  have parts := CommRing.parts with comm175  have idealParts := Ideal.parts with ideal176  have equivalence := quotientRelation.equivalence with comm, ideal177  have compatible := idealRelation.add_compatible with parts, idealParts178  have magma : IsMagma(R.carrier, R.add) := IsGroup.magma with179    (IsAbelianGroup.group with (IsRing.additive with (IsCommRing.ring with parts)))180  rw [quotientRing.addOf, quotientRelation.value]181  rw quotientRelation.value at equivalence182  exact quotientBinary.classes with equivalence, magma, compatible, *183184theorem quotientRing.mul_class (x y : R)185  shows Ring.mul(R ⧸ I)(⟦x⟧[R.carrier, quotientRelation(R, I)],186      ⟦y⟧[R.carrier, quotientRelation(R, I)]) =187    ⟦x * y⟧[R.carrier, quotientRelation(R, I)]188proof189  have parts := CommRing.parts with comm190  have idealParts := Ideal.parts with ideal191  have equivalence := quotientRelation.equivalence with comm, ideal192  have compatible := idealRelation.mul_compatible with parts, idealParts193  have monoid := IsRing.multiplicative with (IsCommRing.ring with parts)194  have magma : IsMagma(R.carrier, R.mul) := IsSemigroup.magma with195    (IsMonoid.semigroup with monoid)196  rw [quotientRing.mulOf, quotientRelation.value]197  rw quotientRelation.value at equivalence198  exact quotientBinary.classes with equivalence, magma, compatible, *199200theorem quotientRing.neg_class (x : R)201  shows Ring.neg(R ⧸ I)(⟦x⟧[R.carrier, quotientRelation(R, I)])202    = ⟦-x⟧[R.carrier, quotientRelation(R, I)]203proof204  have parts := CommRing.parts with comm205  have idealParts := Ideal.parts with ideal206  have equivalence := quotientRelation.equivalence with comm, ideal207  have compatible := idealRelation.neg_compatible with parts, idealParts208  obtain ⟨negF, inverses⟩ := IsGroup.inverse with209    (IsAbelianGroup.group with (IsRing.additive with (IsCommRing.ring with parts)))210  rw [quotientRing.negOf, quotientRelation.value]211  rw quotientRelation.value at equivalence212  exact quotientUnary.classes with equivalence, negF, compatible, *213214end QuotientRings215