Grace/Cumulus/Algebra/Ring/FirstIsomorphism.g17

Open in Workbench Download source

Imports

Homomorphism

Declarations

Source

1-- Quotient factorization and the surjective first isomorphism theorem in 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.FirstIsomorphism8import Homomorphism910theorem idealQuotient.projection_hom (A add zero neg mul one I : Set)11  requires source : IsCommRing(A, add, zero, neg, mul, one)12  requires ideal : IsIdeal(A, add, zero, neg, mul, I)13  shows IsRingHom(quotientProjection(A, idealRelation(A, add, neg, I)), A, add, zero, neg, mul, one, (A ⧸ idealRelation(A, add, neg, I)),14    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],15    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])16proof17  have equivalence := idealRelation.equivalence with *18  have function := quotientProjection.function at A, idealRelation(A, add, neg, I) with *19  have ring := IsCommRing.ring with *20  have addClosed : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]21  have mulClosed : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]22  have negClosed : neg : A → A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, Inverse]23  have zeroIn := IsRing.zero_in_carrier with *24  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsMonoid, Identity]25  have addCompatible := idealRelation.add_compatible with *26  have mulCompatible := idealRelation.mul_compatible with *27  have negCompatible := idealRelation.neg_compatible with *28  have zeroValue := quotientProjection.value at A, idealRelation(A, add, neg, I), zero with *29  have oneValue := quotientProjection.value at A, idealRelation(A, add, neg, I), one with *30  unfold IsRingHom31  refine ⟨function, ⟨zeroValue, ⟨oneValue, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩32  . intros x hx33    have closed := IsRing.neg_closed with hx34    have vx := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *35    have output := quotientProjection.value at A, idealRelation(A, add, neg, I), neg(x) with *36    have lifted := quotientUnary.classes with hx37    cc38  . intros x hx y hy39    have closed := IsRing.add_closed with hx, hy40    have vx := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *41    have vy := quotientProjection.value at A, idealRelation(A, add, neg, I), y with *42    have output := quotientProjection.value at A, idealRelation(A, add, neg, I), call2(add, x, y) with *43    have lifted := quotientBinary.classes at A, idealRelation(A, add, neg, I), add, x, y with *44    cc45  . intros x hx y hy46    have closed := IsRing.mul_closed with hx, hy47    have vx := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *48    have vy := quotientProjection.value at A, idealRelation(A, add, neg, I), y with *49    have output := quotientProjection.value at A, idealRelation(A, add, neg, I), call2(mul, x, y) with *50    have lifted := quotientBinary.classes at A, idealRelation(A, add, neg, I), mul, x, y with *51    cc5253theorem IsRingHom.quotient (f A add zero neg mul one B plus z minus times unit I : Set)54  requires source : IsCommRing(A, add, zero, neg, mul, one)55  requires target : IsCommRing(B, plus, z, minus, times, unit)56  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)57  requires ideal : IsIdeal(A, add, zero, neg, mul, I)58  requires killed : I ⊆ ringKernel(f, A, z)59  shows IsRingHom(quotientMap(f, A, B, idealRelation(A, add, neg, I)), (A ⧸ idealRelation(A, add, neg, I)),60    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],61    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)], B, plus, z, minus, times, unit)62proof63  have function := IsRingHom.function with hom64  have equivalence := idealRelation.equivalence with *65  have respects := IsRingHom.respects_ideal with *66  have mapped := quotientMap.function at f, A, B, idealRelation(A, add, neg, I) with *67  have addClosed : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]68  have mulClosed : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]69  have negClosed : neg : A → A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, Inverse]70  have zeroIn : zero ∈ A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, Identity]71  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsMonoid, Identity]72  have addCompatible := idealRelation.add_compatible with *73  have mulCompatible := idealRelation.mul_compatible with *74  have negCompatible := idealRelation.neg_compatible with *75  have zeroClass := quotientMap.class at f, A, B, idealRelation(A, add, neg, I), zero with *76  have oneClass := quotientMap.class at f, A, B, idealRelation(A, add, neg, I), one with *77  have zeroValue := IsRingHom.zero with hom78  have oneValue := IsRingHom.one with hom79  unfold IsRingHom80  refine ⟨mapped, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩81  . cc82  . cc83  . intros X hX84    exact quotientMap.unary with function, equivalence, respects, negClosed, negCompatible, hom.right.right.right.left, hX85  . intros X hX Y hY86    exact quotientMap.binary with function, equivalence, respects, addClosed, addCompatible, hom.right.right.right.right.left, hX, hY87  . intros X hX Y hY88    exact quotientMap.binary with function, equivalence, respects, mulClosed, mulCompatible, hom.right.right.right.right.right, hX, hY8990theorem IsRingHom.factorization (f A add zero neg mul one B plus z minus times unit I : Set)91  requires source : IsCommRing(A, add, zero, neg, mul, one)92  requires target : IsCommRing(B, plus, z, minus, times, unit)93  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)94  requires ideal : IsIdeal(A, add, zero, neg, mul, I)95  requires killed : I ⊆ ringKernel(f, A, z)96  shows compose(quotientMap(f, A, B, idealRelation(A, add, neg, I)), quotientProjection(A, idealRelation(A, add, neg, I)), A, (A ⧸ idealRelation(A, add, neg, I)), B) = f97proof98  have function := IsRingHom.function with hom99  have equivalence := idealRelation.equivalence with *100  have respects := IsRingHom.respects_ideal with *101  exact quotientMap.factorization with *102103theorem IsRingHom.factor_unique (f A add zero neg mul one B plus z minus times unit I g : Set)104  requires source : IsCommRing(A, add, zero, neg, mul, one)105  requires target : IsCommRing(B, plus, z, minus, times, unit)106  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)107  requires ideal : IsIdeal(A, add, zero, neg, mul, I)108  requires killed : I ⊆ ringKernel(f, A, z)109  requires candidate : g : (A ⧸ idealRelation(A, add, neg, I)) → B110  requires factors : ∀ x ∈ A, g(⟦x⟧[A, idealRelation(A, add, neg, I)]) = f(x)111  shows g = quotientMap(f, A, B, idealRelation(A, add, neg, I))112proof113  have function := IsRingHom.function with hom114  have equivalence := idealRelation.equivalence with *115  have respects := IsRingHom.respects_ideal with *116  exact quotientMap.unique with *117118-- For a surjective unital homomorphism, R/ker(f) is isomorphic to the target.119-- The quotient ring structure is supplied separately by idealQuotient.comm_ring.120theorem idealQuotient.first_isomorphism (f A add zero neg mul one B plus z minus times unit : Set)121  requires source : IsCommRing(A, add, zero, neg, mul, one)122  requires target : IsCommRing(B, plus, z, minus, times, unit)123  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)124  requires onto : SurjectiveBetween(f, A, B)125  shows IsRingIso(quotientMap(f, A, B, idealRelation(A, add, neg, ringKernel(f, A, z))), (A ⧸ idealRelation(A, add, neg, ringKernel(f, A, z))),126    quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), add), ⟦zero⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],127    quotientUnary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), neg), quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), mul), ⟦one⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))], B, plus, z, minus, times, unit)128proof129  have ideal := IsRingHom.kernel_ideal with *130  have killed : ringKernel(f, A, z) ⊆ ringKernel(f, A, z) by simp [Subset]131  have quotientHom := IsRingHom.quotient with *132  have function := IsRingHom.function at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit with *133  have equivalence := idealRelation.equivalence with *134  have respects := IsRingHom.respects_ideal with *135  have reflects : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → relates(idealRelation(A, add, neg, ringKernel(f, A, z)), x, y)136    intros x hx y hy equal137    have congruent := IsRingHom.kernel_congruent.backward with *138    exact idealRelation.relates.backward with *139  have injective := quotientMap.injective with *140  have surjective := quotientMap.surjective with *141  unfold IsRingIso142  refine ⟨quotientHom, ?_⟩143  unfold BijectiveBetween144  refine ⟨injective, surjective⟩145146-- The same results for bundled rings: the projection onto a quotient ring,147-- descent of a homomorphism to a quotient by an ideal inside its kernel,148-- and the first isomorphism theorem.149section BundledQuotients150variable (R I : Set)151hypothesis comm : CommRing(R)152hypothesis ideal : Ideal(R, I)153154theorem quotientRing.projection_hom155  shows quotientProjection(R.carrier, quotientRelation(R, I)) : R →+* R ⧸ I156proof157  have parts := CommRing.parts with comm158  have idealParts := Ideal.parts with ideal159  have engine := idealQuotient.projection_hom with parts, idealParts160  have target := quotientRing.comm_ring with comm, ideal161  have shifted : IsRingHom(quotientProjection(R.carrier, quotientRelation(R, I)),162      R.carrier, R.add, R.zero, R.neg, R.mul, R.one,163      Ring.carrier(R ⧸ I), Ring.add(R ⧸ I),164      Ring.zero(R ⧸ I), Ring.neg(R ⧸ I),165      Ring.mul(R ⧸ I), Ring.one(R ⧸ I))166    rw [quotientRing.carrierOf, quotientRing.addOf, quotientRing.zeroOf,167      quotientRing.negOf, quotientRing.mulOf, quotientRing.oneOf,168      quotientRelation.value]169    exact engine170  exact RingHom.of_projections with (CommRing.to_ring with comm),171    (CommRing.to_ring with target), shifted172173theorem quotientRing.projection_surjective174  shows SurjectiveBetween(quotientProjection(R.carrier, quotientRelation(R, I)),175    R.carrier, Ring.carrier(R ⧸ I))176proof177  have equivalence := quotientRelation.equivalence with comm, ideal178  rw quotientRing.carrierOf179  exact quotientProjection.surjective with equivalence180181end BundledQuotients182183-- The map a homomorphism induces on the quotient by its kernel is written184-- inducedMap(f) under f : R →+* S: the descent of f along the projection,185-- quotientMap(f, R.carrier, S.carrier, quotientRelation(R, ker(f))).186notation function "inducedMap(f)" => quotientMap(f, R.carrier, S.carrier, quotientRelation(R, ker(f))) via hypothesis RingHom(f, R, S)187188section Descent189variable (f R S : Set)190hypothesis source : CommRing(R)191hypothesis target : CommRing(S)192hypothesis hom : f : R →+* S193194theorem RingHom.quotient_hom (I : Set)195  requires ideal : Ideal(R, I)196  requires killed : I ⊆ ker(f)197  shows quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I)) :198    R ⧸ I →+* S199proof200  have sourceParts := CommRing.parts with source201  have targetParts := CommRing.parts with target202  have parts := RingHom.parts with hom203  have idealParts := Ideal.parts with ideal204  have engine := IsRingHom.quotient with sourceParts, targetParts, parts,205    idealParts, killed206  have quotientComm := quotientRing.comm_ring with source, ideal207  have shifted : IsRingHom(quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I)),208      Ring.carrier(R ⧸ I), Ring.add(R ⧸ I),209      Ring.zero(R ⧸ I), Ring.neg(R ⧸ I),210      Ring.mul(R ⧸ I), Ring.one(R ⧸ I),211      S.carrier, S.add, S.zero, S.neg, S.mul, S.one)212    rw [quotientRing.carrierOf, quotientRing.addOf, quotientRing.zeroOf,213      quotientRing.negOf, quotientRing.mulOf, quotientRing.oneOf,214      quotientRelation.value]215    exact engine216  exact RingHom.of_projections with (CommRing.to_ring with quotientComm),217    (CommRing.to_ring with target), shifted218219theorem RingHom.quotient_factorization (I : Set)220  requires ideal : Ideal(R, I)221  requires killed : I ⊆ ker(f)222  shows compose(quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I)),223    quotientProjection(R.carrier, quotientRelation(R, I)), R.carrier,224    (R.carrier ⧸ quotientRelation(R, I)), S.carrier) = f225proof226  have sourceParts := CommRing.parts with source227  have targetParts := CommRing.parts with target228  have parts := RingHom.parts with hom229  have idealParts := Ideal.parts with ideal230  have engine := IsRingHom.factorization with sourceParts, targetParts, parts,231    idealParts, killed232  rw quotientRelation.value233  exact engine234235theorem RingHom.quotient_unique (I g : Set)236  requires ideal : Ideal(R, I)237  requires killed : I ⊆ ker(f)238  requires candidate : g : (R.carrier ⧸ quotientRelation(R, I)) → S.carrier239  requires factors : ∀ x ∈ R, g(⟦x⟧[R.carrier, quotientRelation(R, I)]) = f(x)240  shows g = quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I))241proof242  have sourceParts := CommRing.parts with source243  have targetParts := CommRing.parts with target244  have parts := RingHom.parts with hom245  have idealParts := Ideal.parts with ideal246  rw quotientRelation.value at candidate247  rw under quotientRelation.value at factors248  rw quotientRelation.value249  exact IsRingHom.factor_unique with sourceParts, targetParts, parts,250    idealParts, killed, candidate, factors251252-- The first isomorphism theorem: a surjective homomorphism identifies the253-- quotient by its kernel with the target.254theorem RingHom.first_isomorphism255  requires onto : SurjectiveBetween(f, R.carrier, S.carrier)256  shows inducedMap(f) : R ⧸ ker(f) ≃+* S257proof258  have sourceParts := CommRing.parts with source259  have targetParts := CommRing.parts with target260  have parts := RingHom.parts with hom261  have engine := idealQuotient.first_isomorphism with sourceParts, targetParts,262    parts, onto263  have kernelIdeal := ringKernel.ideal with source, target, hom264  have quotientComm := quotientRing.comm_ring with source, kernelIdeal265  have shifted : IsRingIso(inducedMap(f),266      Ring.carrier(R ⧸ ker(f)), Ring.add(R ⧸ ker(f)),267      Ring.zero(R ⧸ ker(f)), Ring.neg(R ⧸ ker(f)),268      Ring.mul(R ⧸ ker(f)), Ring.one(R ⧸ ker(f)),269      S.carrier, S.add, S.zero, S.neg, S.mul, S.one)270    rw [quotientRing.carrierOf, quotientRing.addOf, quotientRing.zeroOf,271      quotientRing.negOf, quotientRing.mulOf, quotientRing.oneOf,272      quotientRelation.value]273    exact engine274  exact RingIso.of_projections with (CommRing.to_ring with quotientComm),275    (CommRing.to_ring with target), shifted276277end Descent278