Grace/Cumulus/Algebra/Ring/Image.g17

Open in Workbench Download source

Imports

FirstIsomorphism · Subring

Declarations

Source

1-- Image subrings and the general 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.Image8import FirstIsomorphism9import Subring1011theorem IsRingHom.image_subring (f A add zero neg mul one B plus z minus times unit : Set)12  requires source : IsCommRing(A, add, zero, neg, mul, one)13  requires target : IsCommRing(B, plus, z, minus, times, unit)14  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)15  shows IsSubring(B, plus, z, minus, times, unit, functionImage(f, A, B))16proof17  have function := IsRingHom.function with hom18  have ring := IsCommRing.ring with source19  have zeroIn := IsRing.zero_in_carrier with ring20  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsMonoid, Identity]21  have zeroValue := IsRingHom.zero with hom22  have oneValue := IsRingHom.one with hom23  have zeroImage := functionImage.value at f, A, B, zero with *24  have oneImage := functionImage.value at f, A, B, one with *25  have subset := functionImage.subset at f, A, B26  unfold IsSubring27  refine ⟨subset, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩28  . cc29  . cc30    intros y hy31    obtain ⟨yIn, x, hx, shape⟩ := functionImage.membership.forward with hy32    have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, x with *33    have mapped := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *34    have output := functionImage.value at f, A, B, neg(x) with *35    cc36    intros y hy w hw37    obtain ⟨yIn, a, ha, sy⟩ := functionImage.membership.forward with hy38    obtain ⟨wIn, b, hb, sw⟩ := functionImage.membership.forward with hw39    have closed := IsRing.add_closed at A, add, zero, neg, mul, one, a, b with *40    have mapped := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, a, b with *41    have output := functionImage.value at f, A, B, call2(add, a, b) with *42    cc43    intros y hy w hw44    obtain ⟨yIn, c, hc, sy⟩ := functionImage.membership.forward with hy45    obtain ⟨wIn, d, hd, sw⟩ := functionImage.membership.forward with hw46    have closed := IsRing.mul_closed at A, add, zero, neg, mul, one, c, d with *47    have mapped := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, c, d with *48    have output := functionImage.value at f, A, B, call2(mul, c, d) with *49    cc5051theorem IsRingHom.image_comm_ring (f A add zero neg mul one B plus z minus times unit : Set)52  requires source : IsCommRing(A, add, zero, neg, mul, one)53  requires target : IsCommRing(B, plus, z, minus, times, unit)54  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)55  shows IsCommRing(functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)56proof57  have subring := IsRingHom.image_subring with source, target, hom58  exact IsSubring.comm_ring with target, subring5960theorem IsRingHom.corestrict (f A add zero neg mul one B plus z minus times unit : Set)61  requires source : IsCommRing(A, add, zero, neg, mul, one)62  requires target : IsCommRing(B, plus, z, minus, times, unit)63  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)64  shows IsRingHom(f, A, add, zero, neg, mul, one, functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)65proof66  have function := IsRingHom.function with hom67  have corestricted := functionImage.corestrict with *68  have imageRing := IsRingHom.image_comm_ring with source, target, hom69  have subring := IsRingHom.image_subring with source, target, hom70  have subset := functionImage.subset at f, A, B71  have addClosed := IsSubring.add_closed with *72  have mulClosed := IsSubring.mul_closed with *73  have addition : IsMagma(B, plus) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]74  have multiplication : IsMagma(B, times) by simp [IsCommRing, IsRing, IsMonoid, IsSemigroup]75  apply IsRingHom.of_add_mul_one with source, imageRing, corestricted76  . intros x hx y hy77    have fx := functionImage.value with function, hx78    have fy := functionImage.value with function, hx79    have mapped := IsRingHom.add with hx, hy80    have restricted := restrictBinary.value at B, functionImage(f, A, B), plus, f(x), f(y) with *81    cc82  . intros x hx y hy83    have fx := functionImage.value with function, hx84    have fy := functionImage.value with function, hx85    have mapped := IsRingHom.mul with hx, hy86    have restricted := restrictBinary.value at B, functionImage(f, A, B), times, f(x), f(y) with *87    cc88  . exact IsRingHom.one with hom8990-- No surjectivity hypothesis: the target is the image subring.91theorem IsRingHom.first_isomorphism_image (f A add zero neg mul one B plus z minus times unit : Set)92  requires source : IsCommRing(A, add, zero, neg, mul, one)93  requires target : IsCommRing(B, plus, z, minus, times, unit)94  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)95  shows IsRingIso(quotientMap(f, A, functionImage(f, A, B), idealRelation(A, add, neg, ringKernel(f, A, z))), (A ⧸ idealRelation(A, add, neg, ringKernel(f, A, z))),96    quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), add), ⟦zero⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],97    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))],98    functionImage(f, A, B), restrict(plus, functionImage(f, A, B) × functionImage(f, A, B)), z, restrict(minus, functionImage(f, A, B)), restrict(times, functionImage(f, A, B) × functionImage(f, A, B)), unit)99proof100  have function := IsRingHom.function with hom101  have imageRing := IsRingHom.image_comm_ring with source, target, hom102  have corestricted := IsRingHom.corestrict with source, target, hom103  have onto := functionImage.surjective with *104  exact idealQuotient.first_isomorphism with source, imageRing, corestricted, onto105106-- Every homomorphism factors as a surjection followed by an inclusion.107theorem IsRingHom.image_factorization (f A add zero neg mul one B plus z minus times unit : Set)108  requires source : IsCommRing(A, add, zero, neg, mul, one)109  requires target : IsCommRing(B, plus, z, minus, times, unit)110  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)111  shows compose(identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B) = f112proof113  have function := IsRingHom.function with hom114  have corestricted := functionImage.corestrict with function115  have subring := IsRingHom.image_subring with source, target, hom116  have inclusion := IsSubring.inclusion_function with subring117  have composed := compose.function at identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B with *118  apply FunctionBetween.ext with composed, function119  intros x hx120  have fx := functionImage.value with function, hx121  have value := compose.apply at identity(functionImage(f, A, B)), f, A, functionImage(f, A, B), B, x with *122  have included := identity.apply with fx123  cc124