Grace/Cumulus/Algebra/Ring/Homomorphism.g17

Open in Workbench Download source

Imports

HomomorphismCore · Quotient

Declarations

Source

1-- Ring homomorphisms f : R →+* S between bundled rings: maps preserving2-- the operations and constants, the bridges to the form over separate3-- pieces, the preservation laws, identity and composite homomorphisms, the4-- kernel ideal, and isomorphisms f : R ≃+* S; everything 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.Homomorphism11import HomomorphismCore12import Quotient1314-- f : R →+* S: a function between the carriers preserving zero, one,15-- negation, addition, and multiplication. The form is a transparent16-- guard, so a hypothesis f : R →+* S also supplies the rings R and S, their17-- operations, and the binders (a : R) and (b : S). IsRingHom(f, A, add,18-- …, B, plus, …) remains the form over separate pieces, bridged below.19predicate RingHom (f R S : Set) :=20  Ring(R) ∧ Ring(S) ∧ (f : R.carrier → S.carrier) ∧21  f(R[0]) = S[0] ∧ f(R[1]) = S[1] ∧ (∀ x ∈ R, f(-x) = -f(x)) ∧22  (∀ x y ∈ R, f(x + y) = f(x) + f(y)) ∧23  (∀ x y ∈ R, f(x * y) = f(x) * f(y))24predicate RingIso (f R S : Set) :=25  RingHom(f, R, S) ∧ BijectiveBetween(f, R.carrier, S.carrier)2627notation guard "_ : _ →+* _" => RingHom28notation guard "_ : _ ≃+* _" => RingIso2930-- The kernel of f : R →+* S is written ker(f) wherever a hypothesis in31-- scope supplies the homomorphism, and is the set ringKernel(f, R.carrier,32-- S.zero) of the elements sent to zero.33notation function "ker(f)" => ringKernel(f, R, S[0]) via hypothesis RingHom(f, R, S)3435-- Bridges between the bundled homomorphism and the form over separate36-- pieces: the bundled-to-unbundled direction is an instance.37instance RingHom.parts (f R S : Set)38  requires hom : f : R →+* S39  shows IsRingHom(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,40    S.carrier, S.add, S.zero, S.neg, S.mul, S.one)41proof42  obtain ⟨source, target, function, zero, one, neg, add, mul⟩ := hom43  unfold IsRingHom44  exact ⟨function, zero, one, neg, add, mul⟩4546theorem RingHom.of_projections (f R S : Set)47  requires source : Ring(R)48  requires target : Ring(S)49  requires hom : IsRingHom(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,50    S.carrier, S.add, S.zero, S.neg, S.mul, S.one)51  shows f : R →+* S52proof53  obtain ⟨function, zero, one, neg, add, mul⟩ := hom54  unfold Homomorphism.RingHom55  exact ⟨source, target, function, zero, one, neg, add, mul⟩5657theorem RingHom.of_parts (f A add zero neg mul one B plus z minus times unit : Set)58  requires source : IsRing(A, add, zero, neg, mul, one)59  requires target : IsRing(B, plus, z, minus, times, unit)60  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)61  shows f : Ring.mk(A, add, zero, neg, mul, one) →+* Ring.mk(B, plus, z, minus, times, unit)62proof63  have bundledSource := Ring.of_parts with source64  have bundledTarget := Ring.of_parts with target65  have shifted : IsRingHom(f, Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),66      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),67      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),68      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),69      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)),70      Ring.one(Ring.mk(A, add, zero, neg, mul, one)),71      Ring.carrier(Ring.mk(B, plus, z, minus, times, unit)),72      Ring.add(Ring.mk(B, plus, z, minus, times, unit)),73      Ring.zero(Ring.mk(B, plus, z, minus, times, unit)),74      Ring.neg(Ring.mk(B, plus, z, minus, times, unit)),75      Ring.mul(Ring.mk(B, plus, z, minus, times, unit)),76      Ring.one(Ring.mk(B, plus, z, minus, times, unit)))77    ring_projections78  exact RingHom.of_projections with bundledSource, bundledTarget, shifted7980instance RingIso.parts (f R S : Set)81  requires iso : f : R ≃+* S82  shows IsRingIso(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,83    S.carrier, S.add, S.zero, S.neg, S.mul, S.one)84proof85  obtain ⟨hom, bijective⟩ := iso86  have parts := RingHom.parts with hom87  unfold IsRingIso88  exact ⟨parts, bijective⟩8990theorem RingIso.of_projections (f R S : Set)91  requires source : Ring(R)92  requires target : Ring(S)93  requires iso : IsRingIso(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,94    S.carrier, S.add, S.zero, S.neg, S.mul, S.one)95  shows f : R ≃+* S96proof97  obtain ⟨hom, bijective⟩ := iso98  have bundled := RingHom.of_projections with source, target, hom99  unfold Homomorphism.RingIso100  exact ⟨bundled, bijective⟩101102-- The constructor: between commutative rings the three usual laws suffice,103-- zero and negation being preserved as a consequence.104theorem RingHom.mk (f R S : Set)105  requires source : CommRing(R)106  requires target : CommRing(S)107  requires function : f : R.carrier → S.carrier108  requires additive : ∀ x y ∈ R, f(x + y) = f(x) + f(y)109  requires multiplicative : ∀ x y ∈ R, f(x * y) = f(x) * f(y)110  requires unital : f(R[1]) = S[1]111  shows f : R →+* S112proof113  have sourceParts := CommRing.parts with source114  have targetParts := CommRing.parts with target115  have engine := IsRingHom.of_add_mul_one with sourceParts, targetParts,116    function, additive, multiplicative, unital117  exact RingHom.of_projections with (CommRing.to_ring with source),118    (CommRing.to_ring with target), engine119120section HomLaws121variable (f R S : Set)122hypothesis hom : f : R →+* S123124theorem RingHom.source125  shows Ring(R)126proof127  obtain ⟨source, rest⟩ := hom128  exact source129130theorem RingHom.target131  shows Ring(S)132proof133  obtain ⟨source, target, rest⟩ := hom134  exact target135136-- The preservation laws, under their standard names.137instance RingHom.map_mem (a : R)138  shows f(a) ∈ S139proof140  obtain ⟨source, target, function, rest⟩ := hom141  exact FunctionBetween.apply_closed with function, *142143theorem RingHom.map_zero144  shows f(R[0]) = S[0]145proof146  obtain ⟨source, target, function, zero, rest⟩ := hom147  exact zero148149theorem RingHom.map_one150  shows f(R[1]) = S[1]151proof152  obtain ⟨source, target, function, zero, one, rest⟩ := hom153  exact one154155theorem RingHom.map_neg (a : R)156  shows f(-a) = -f(a)157proof158  obtain ⟨source, target, function, zero, one, neg, rest⟩ := hom159  have aIn : a ∈ R by assumption160  exact neg with a, aIn161162theorem RingHom.map_add (a b : R)163  shows f(a + b) = f(a) + f(b)164proof165  obtain ⟨source, target, function, zero, one, neg, add, mul⟩ := hom166  have aIn : a ∈ R by assumption167  have bIn : b ∈ R by assumption168  exact add with a, aIn, b, bIn169170theorem RingHom.map_mul (a b : R)171  shows f(a * b) = f(a) * f(b)172proof173  obtain ⟨source, target, function, zero, one, neg, add, mul⟩ := hom174  have aIn : a ∈ R by assumption175  have bIn : b ∈ R by assumption176  exact mul with a, aIn, b, bIn177178theorem RingHom.map_sub (a b : R)179  shows f(a - b) = f(a) - f(b)180proof181  have source := RingHom.source with hom182  have target := RingHom.target with hom183  have fa : f(a) ∈ S := RingHom.map_mem with *184  have fb : f(b) ∈ S := RingHom.map_mem with *185  have negIn : -b ∈ R := Ring.neg_mem with *186  rw [Ring.sub.value, Ring.sub.value, RingHom.map_add, RingHom.map_neg]187  rfl188189-- The kernel: the elements sent to zero, an ideal of the source when the190-- rings are commutative, and the measure of equal images.191theorem RingHom.mem_kernel_iff (x : R)192  shows x ∈ ker(f) ↔ f(x) = S[0]193proof194  have xIn : x ∈ R by assumption195  constructor196  . intro member197    have data := ringKernel.membership.forward with member198    exact data.right199  . intro vanishes200    exact ringKernel.membership.backward with ⟨xIn, vanishes⟩201202theorem RingHom.kernel_subset203  shows ker(f) ⊆ R204proof205  intros x hx206  have data := ringKernel.membership.forward with hx207  exact data.left208209theorem RingHom.zero_mem_kernel210  shows R[0] ∈ ker(f)211proof212  have source := RingHom.source with hom213  have zeroIn : R[0] ∈ R := Ring.zero_mem with *214  have vanishes := RingHom.map_zero with hom215  exact ringKernel.membership.backward with ⟨zeroIn, vanishes⟩216217theorem RingHom.ext (g : Set)218  requires hom2 : g : R →+* S219  requires same : ∀ x ∈ R, f(x) = g(x)220  shows f = g221proof222  obtain ⟨source, target, function, rest⟩ := hom223  obtain ⟨source2, target2, function2, rest2⟩ := hom2224  exact FunctionBetween.ext with function, function2, same225226end HomLaws227228section CommutativeHomLaws229variable (f R S : Set)230hypothesis source : CommRing(R)231hypothesis target : CommRing(S)232hypothesis hom : f : R →+* S233234theorem ringKernel.ideal235  shows Ideal(R, ker(f))236proof237  have sourceParts := CommRing.parts with source238  have targetParts := CommRing.parts with target239  have parts := RingHom.parts with hom240  have engine := IsRingHom.kernel_ideal with sourceParts, targetParts, parts241  exact Ideal.of_projections with engine242243theorem RingHom.apply_eq_iff (x y : R)244  shows f(x) = f(y) ↔ x - y ∈ ker(f)245proof246  have sourceParts := CommRing.parts with source247  have targetParts := CommRing.parts with target248  have parts := RingHom.parts with hom249  have xIn : x ∈ R by assumption250  have yIn : y ∈ R by assumption251  have criterion := IsRingHom.kernel_congruent with sourceParts, targetParts,252    parts, xIn, yIn253  rw Ring.sub.value254  constructor255  . intro equal256    have same := criterion.backward with equal257    unfold Congruent at same258    exact same259  . intro member260    have same : Congruent(R.add, R.neg, ringKernel(f, R.carrier, S.zero), x, y)261      unfold Congruent262      exact member263    exact criterion.forward with same264265end CommutativeHomLaws266267-- Identity and composite homomorphisms.268theorem RingHom.id (R : Set)269  requires comm : CommRing(R)270  shows identity(R.carrier) : R →+* R271proof272  have parts := CommRing.parts with comm273  have engine := IsRingHom.identity with parts274  exact RingHom.of_projections with (CommRing.to_ring with comm),275    (CommRing.to_ring with comm), engine276277theorem RingHom.comp (f g R S T : Set)278  requires comm : CommRing(R)279  requires first : f : R →+* S280  requires second : g : S →+* T281  shows compose(g, f, R.carrier, S.carrier, T.carrier) : R →+* T282proof283  have parts := CommRing.parts with comm284  have firstParts := RingHom.parts with first285  have secondParts := RingHom.parts with second286  have engine := IsRingHom.compose with parts, firstParts, secondParts287  exact RingHom.of_projections with (RingHom.source with first),288    (RingHom.target with second), engine289290-- An isomorphism is a homomorphism, and its inverse graph is one too.291theorem RingIso.hom_of (f R S : Set)292  requires iso : f : R ≃+* S293  shows f : R →+* S294proof295  obtain ⟨hom, bijective⟩ := iso296  exact hom297298theorem RingIso.bijective_of (f R S : Set)299  requires iso : f : R ≃+* S300  shows BijectiveBetween(f, R.carrier, S.carrier)301proof302  obtain ⟨hom, bijective⟩ := iso303  exact bijective304305theorem RingIso.symm (f R S : Set)306  requires source : CommRing(R)307  requires target : CommRing(S)308  requires iso : f : R ≃+* S309  shows converse(f, R.carrier, S.carrier) : S ≃+* R310proof311  have sourceParts := CommRing.parts with source312  have targetParts := CommRing.parts with target313  have parts := RingIso.parts with iso314  have engine := IsRingIso.inverse with sourceParts, targetParts, parts315  exact RingIso.of_projections with (CommRing.to_ring with target),316    (CommRing.to_ring with source), engine317