Grace/Cumulus/Algebra/Ring/HomomorphismCore.g17

Open in Workbench Download source

Imports

QuotientCore · Relation.QuotientMap

Declarations

Source

1-- Unital ring homomorphisms over separate pieces and their kernels: the2-- engine under Homomorphism, entirely in ZF3-- 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.HomomorphismCore9import QuotientCore10import Relation.QuotientMap1112-- IsRingHom(f, A, add, …, B, plus, …) is the homomorphism over separate13-- pieces; the bundled f : R →+* S is defined in Homomorphism and bridged14-- to this form. Preservation data is separate from source and target ring laws.15-- Zero and negation laws are included to make the interface directly usable.16predicate IsRingHom (f A add zero neg mul one B plus z minus times unit : Set) :=17  FunctionBetween(f, A, B) ∧ f(zero) = z ∧ f(one) = unit ∧18  (∀ x ∈ A, f(neg(x)) = minus(f(x))) ∧19  (∀ x ∈ A, ∀ y ∈ A, f(call2(add, x, y)) = plus(f(x), f(y))) ∧20  (∀ x ∈ A, ∀ y ∈ A, f(call2(mul, x, y)) = times(f(x), f(y)))2122notation scoped IsRingHom(f, R, S) => IsRingHom(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S.carrier, S.add, S.zero, S.neg, S.mul, S.one)2324predicate IsRingIso (f A add zero neg mul one B plus z minus times unit : Set) :=25  IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit) ∧26  BijectiveBetween(f, A, B)2728notation scoped IsRingIso(f, R, S) => IsRingIso(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S.carrier, S.add, S.zero, S.neg, S.mul, S.one)2930theorem IsRingHom.function (f A add zero neg mul one B plus z minus times unit : Set)31  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)32  shows f : A → B33proof34  exact hom.left3536theorem IsRingHom.zero (f A add zero neg mul one B plus z minus times unit : Set)37  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)38  shows f(zero) = z39proof40  exact hom.right.left4142theorem IsRingHom.one (f A add zero neg mul one B plus z minus times unit : Set)43  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)44  shows f(one) = unit45proof46  exact hom.right.right.left4748theorem IsRingHom.neg (f A add zero neg mul one B plus z minus times unit x : Set)49  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)50  requires hx : x ∈ A51  shows f(neg(x)) = minus(f(x))52proof53  exact hom.right.right.right.left with x, hx5455theorem IsRingHom.add (f A add zero neg mul one B plus z minus times unit x y : Set)56  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)57  requires hx : x ∈ A58  requires hy : y ∈ A59  shows f(call2(add, x, y)) = plus(f(x), f(y))60proof61  exact hom.right.right.right.right.left with x, hx, y, hy6263theorem IsRingHom.mul (f A add zero neg mul one B plus z minus times unit x y : Set)64  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)65  requires hx : x ∈ A66  requires hy : y ∈ A67  shows f(call2(mul, x, y)) = times(f(x), f(y))68proof69  exact hom.right.right.right.right.right with x, hx, y, hy7071theorem IsRingHom.closed (f A add zero neg mul one B plus z minus times unit x : Set)72  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)73  requires hx : x ∈ A74  shows f(x) ∈ B75proof76  have function := IsRingHom.function with hom77  exact FunctionBetween.apply_closed with *7879def ringKernel (f A z : Set) : Set := {x ∈ A | f(x) = z}8081theorem IsRingHom.kernel_ideal (f A add zero neg mul one B plus z minus times unit : Set)82  requires source : IsCommRing(A, add, zero, neg, mul, one)83  requires target : IsCommRing(B, plus, z, minus, times, unit)84  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)85  shows IsIdeal(A, add, zero, neg, mul, ringKernel(f, A, z))86proof87  have sourceRing := IsCommRing.ring with source88  have targetRing := IsCommRing.ring with target89  have zeroIn := IsRing.zero_in_carrier at A, add, zero, neg, mul, one with *90  have zeroValue := IsRingHom.zero with hom91  unfold IsIdeal92  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩93  . settle with Subset, ringKernel.membership94  . apply ringKernel.membership.backward at f, A, z, zero95    refine ⟨zeroIn, zeroValue⟩96  . intros x hx y hy97    obtain ⟨xIn, xValue⟩ := ringKernel.membership.forward with hx98    obtain ⟨yIn, yValue⟩ := ringKernel.membership.forward with hy99    have sumIn := IsRing.add_closed at A, add, zero, neg, mul, one, x, y with *100    have preserved := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *101    apply ringKernel.membership.backward102    refine ⟨sumIn, ?_⟩103    rw [preserved, xValue, yValue]104    ring105  . intros x hx106    obtain ⟨xIn, xValue⟩ := ringKernel.membership.forward with hx107    have negIn := IsRing.neg_closed at A, add, zero, neg, mul, one, x with *108    have preserved := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *109    apply ringKernel.membership.backward110    refine ⟨negIn, ?_⟩111    rw [preserved, xValue]112    ring113  . intros a ha x hx114    obtain ⟨xIn, xValue⟩ := ringKernel.membership.forward with hx115    have aValueIn := IsRingHom.closed with ha116    have leftIn := IsRing.mul_closed at A, add, zero, neg, mul, one, a, x with *117    have rightIn := IsRing.mul_closed at A, add, zero, neg, mul, one, x,118      a with *119    have leftValue := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, a, x with *120    have rightValue := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, a with *121    constructor122    . apply ringKernel.membership.backward at f, A, z, call2(mul, a, x)123      refine ⟨leftIn, ?_⟩124      rw [leftValue, xValue]125      ring126    . apply ringKernel.membership.backward at f, A, z, call2(mul, x, a)127      refine ⟨rightIn, ?_⟩128      rw [rightValue, xValue]129      ring130131theorem IsRingHom.sub (f A add zero neg mul one B plus z minus times unit x y : Set)132  requires source : IsCommRing(A, add, zero, neg, mul, one)133  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)134  requires hx : x ∈ A135  requires hy : y ∈ A136  shows f(call2(add, x, neg(y))) = plus(f(x), minus(f(y)))137proof138  have ring := IsCommRing.ring with source139  have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, y with *140  have sum := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, neg(y) with *141  have inverse := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *142  cc143144theorem IsRingHom.kernel_congruent (f A add zero neg mul one B plus z minus times unit x y : Set)145  requires source : IsCommRing(A, add, zero, neg, mul, one)146  requires target : IsCommRing(B, plus, z, minus, times, unit)147  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)148  requires hx : x ∈ A149  requires hy : y ∈ A150  shows Congruent(add, neg, ringKernel(f, A, z), x, y) ↔ f(x) = f(y)151proof152  have ring := IsCommRing.ring with source153  have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, y with *154  have difference := IsRing.add_closed at A, add, zero, neg, mul, one, x, neg(y) with *155  have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *156  have fy := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *157  have mapped := IsRingHom.sub at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *158  constructor159  . intro member160    unfold Congruent at member161    have value := ringKernel.membership.forward with member162    have equation : plus(f(x), minus(f(y))) = z by cc163    linear_combination equation164  . intro equal165    unfold Congruent166    apply ringKernel.membership.backward167    refine ⟨difference, ?_⟩168    rw [mapped, equal]169    ring170171theorem IsRingHom.respects_ideal (f A add zero neg mul one B plus z minus times unit I : Set)172  requires source : IsCommRing(A, add, zero, neg, mul, one)173  requires target : IsCommRing(B, plus, z, minus, times, unit)174  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)175  requires killed : I ⊆ ringKernel(f, A, z)176  shows Respects(f, A, idealRelation(A, add, neg, I))177proof178  intros x hx y hy related179  have congruent := idealRelation.relates.forward with *180  have member := killed with call2(add, x, neg(y)), congruent181  have kernelCongruent : Congruent(add, neg, ringKernel(f, A, z), x, y) by exact member182  exact IsRingHom.kernel_congruent.forward with *183184-- Users supply the three usual laws; zero and negation are derived.185theorem IsRingHom.of_add_mul_one (f A add zero neg mul one B plus z minus times unit : Set)186  requires source : IsCommRing(A, add, zero, neg, mul, one)187  requires target : IsCommRing(B, plus, z, minus, times, unit)188  requires function : f : A → B189  requires additive : ∀ x ∈ A, ∀ y ∈ A, f(call2(add, x, y)) = plus(f(x), f(y))190  requires multiplicative : ∀ x ∈ A, ∀ y ∈ A, f(call2(mul, x, y)) = times(f(x), f(y))191  requires unital : f(one) = unit192  shows IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times,193    unit)194proof195  have ring := IsCommRing.ring with source196  have zeroIn := IsRing.zero_in_carrier with ring197  have fZeroIn := FunctionBetween.apply_closed with *198  have zeroSum : call2(add, zero, zero) = zero by ring199  have mappedZero := additive with zero, zeroIn, zero, zeroIn200  rw zeroSum at mappedZero201  have zeroValue : f(zero) = z by linear_combination -mappedZero202  unfold IsRingHom203  refine ⟨function, ⟨zeroValue, ⟨unital, ⟨?_, ⟨additive, multiplicative⟩⟩⟩⟩⟩204  intros x hx205  have negIn := IsRing.neg_closed with hx206  have fxIn := FunctionBetween.apply_closed with hx207  have fnIn := FunctionBetween.apply_closed at f, A, B, neg(x) with *208  have inverse := IsRing.add_inverse_left with hx209  have mapped := additive with neg(x), negIn, x, hx210  rw [inverse, zeroValue] at mapped211  linear_combination -mapped212213theorem IsRingHom.identity (A add zero neg mul one : Set)214  requires source : IsCommRing(A, add, zero, neg, mul, one)215  shows IsRingHom(identity(A), A, add, zero, neg, mul, one, A, add, zero, neg, mul, one)216proof217  have function := identity.function at A218  have ring := IsCommRing.ring with source219  have zeroIn := IsRing.zero_in_carrier with ring220  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, Identity]221  have zeroValue := identity.apply at zero, A with *222  have oneValue := identity.apply at one, A with *223  unfold IsRingHom224  refine ⟨function, ⟨zeroValue, ⟨oneValue, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩225  . intros x hx226    have negative := IsRing.neg_closed with hx227    have input := identity.apply with hx228    have output := identity.apply at neg(x), A with *229    cc230  . intros x hx y hy231    have closed := IsRing.add_closed with hx, hy232    have vx := identity.apply with hx233    have vy := identity.apply with hy234    have output := identity.apply at call2(add, x, y), A with *235    cc236  . intros x hx y hy237    have closed := IsRing.mul_closed with hx, hy238    have vx := identity.apply with hx239    have vy := identity.apply with hy240    have output := identity.apply at call2(mul, x, y), A with *241    cc242243theorem IsRingHom.compose (f g A add zero neg mul one B plus z minus times unit C sum o inverse product e : Set)244  requires source : IsCommRing(A, add, zero, neg, mul, one)245  requires first : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)246  requires second : IsRingHom(g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e)247  shows IsRingHom(compose(g, f, A, B, C), A, add, zero, neg, mul, one, C, sum, o, inverse, product, e)248proof249  have ff := IsRingHom.function with first250  have gf := IsRingHom.function with second251  have function := compose.function at g, f, A, B, C with *252  have ring := IsCommRing.ring with source253  have zeroIn := IsRing.zero_in_carrier at A, add, zero, neg, mul, one with *254  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, Identity]255  have fZero := IsRingHom.zero with first256  have gZero := IsRingHom.zero with second257  have fOne := IsRingHom.one with first258  have gOne := IsRingHom.one with second259  have zeroValue := compose.apply at g, f, A, B, C, zero with *260  have oneValue := compose.apply at g, f, A, B, C, one with *261  unfold IsRingHom262  refine ⟨function, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩263  . cc264  . cc265  . intros x hx266    have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *267    have closed := IsRing.neg_closed at A, add, zero, neg, mul, one, x with *268    have fNeg := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *269    have gNeg := IsRingHom.neg at g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e, f(x) with *270    have input := compose.apply at g, f, A, B, C, x with *271    have output := compose.apply at g, f, A, B, C, neg(x) with *272    cc273  . intros x hx y hy274    have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *275    have fy := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *276    have closed := IsRing.add_closed at A, add, zero, neg, mul, one, x, y with *277    have fOp := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *278    have gOp := IsRingHom.add at g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e, f(x), f(y) with *279    have vx := compose.apply at g, f, A, B, C, x with *280    have vy := compose.apply at g, f, A, B, C, y with *281    have output := compose.apply at g, f, A, B, C, call2(add, x, y) with *282    cc283  . intros x hx y hy284    have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *285    have fy := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *286    have closed := IsRing.mul_closed at A, add, zero, neg, mul, one, x, y with *287    have fOp := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *288    have gOp := IsRingHom.mul at g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e, f(x), f(y) with *289    have vx := compose.apply at g, f, A, B, C, x with *290    have vy := compose.apply at g, f, A, B, C, y with *291    have output := compose.apply at g, f, A, B, C, call2(mul, x, y) with *292    cc293294theorem IsRingIso.hom (f A add zero neg mul one B plus z minus times unit : Set)295  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)296  shows IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times,297    unit)298proof299  simp [IsRingIso]300301theorem IsRingIso.bijective (f A add zero neg mul one B plus z minus times unit : Set)302  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)303  shows BijectiveBetween(f, A, B)304proof305  simp [IsRingIso]306307-- Isomorphisms are reversible; the inverse graph is the relational converse.308theorem IsRingIso.inverse (f A add zero neg mul one B plus z minus times unit : Set)309  requires source : IsCommRing(A, add, zero, neg, mul, one)310  requires target : IsCommRing(B, plus, z, minus, times, unit)311  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)312  shows IsRingIso(converse(f, A, B), B, plus, z, minus, times, unit, A, add, zero, neg, mul, one)313proof314  have hom := IsRingIso.hom with iso315  have bijective := IsRingIso.bijective with iso316  have inverse := converse.function_of_bijective with bijective317  have inverseBijective := converse.bijective with bijective318  have ring := IsCommRing.ring with source319  have inverseHom : IsRingHom(converse(f, A, B), B, plus, z, minus, times, unit, A, add, zero, neg, mul, one)320    apply IsRingHom.of_add_mul_one with target, source, inverse321    . intros x hx y hy322      have px := FunctionBetween.apply_closed with inverse, hx323      have py := FunctionBetween.apply_closed with inverse, hy324      have fx := Bijective.apply_inverse with bijective, hx325      have fy := Bijective.apply_inverse with bijective, hy326      have closed := IsRing.add_closed at A, add, zero, neg, mul, one, converse(f, A, B)(x), converse(f, A, B)(y) with *327      have mapped := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, converse(f, A, B)(x), converse(f, A, B)(y) with *328      have recovered := Bijective.inverse_apply with bijective, closed329      cc330    . intros x hx y hy331      have px := FunctionBetween.apply_closed with inverse, hx332      have py := FunctionBetween.apply_closed with inverse, hy333      have fx := Bijective.apply_inverse with bijective, hx334      have fy := Bijective.apply_inverse with bijective, hy335      have closed := IsRing.mul_closed at A, add, zero, neg, mul, one, converse(f, A, B)(x), converse(f, A, B)(y) with *336      have mapped := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, converse(f, A, B)(x), converse(f, A, B)(y) with *337      have recovered := Bijective.inverse_apply with bijective, closed338      cc339    . have oneIn : one ∈ A340        simp [IsCommRing, IsRing, IsMonoid, Identity]341      have mapped := IsRingHom.one with hom342      have recovered := Bijective.inverse_apply with bijective, oneIn343      cc344  unfold IsRingIso345  refine ⟨inverseHom, inverseBijective⟩346