Homomorphism Theorems
The homomorphism theorem for modules
Let R be a ring, A and B R-Modules, and sigma a module homomorphism from A to B.Cs is a comodule
We define Cs, a comodule and prove that it really is a comodule.Section Theorem_on_Modules.
Variable R : CRing.
Section Cs_CoModule.
Variables A B : RModule R.
Variable sigma : ModHom A B.
Definition cspred (x:A) : CProp := (sigma x) [#] 0.
Definition cswdpred : (wd_pred A).
Defined.
Lemma cs_is_comod : is_comod A cswdpred.
Definition cs_as_comod := Build_comod R A cswdpred cs_is_comod.
End Cs_CoModule.
Variables A B : RModule R.
Variable sigma : ModHom A B.
Now we can `divide' A by ~Cs.
We now define the functions of which we want to prove the existence.
Definition tau (x:A) := (x:AdivCs).
Definition tau_is_fun := Build_CSetoid_fun A AdivCs tau tau_strext.
Lemma tau_surj : surjective tau_is_fun.
Definition sigst (x:AdivCs) := (sigma x).
Definition sigst_is_fun := Build_CSetoid_fun AdivCs B sigst sigst_strext.
Lemma sigst_inj : injective sigst_is_fun.
And now we have reached a goal: we can easily formulate and prove
the homomorphism theorem for modules.
Lemma ModHomTheorem : {tau : CSetoid_fun A AdivCs | surjective tau}
and {sigst : CSetoid_fun AdivCs B | injective sigst}.
End Theorem_on_Modules.
The homomorphism theorem for rings
Let R and S be rings and sigma a ring homomorphism from R to S.CsR is a coideal
We define CsR, a coideal and prove that it really is a coideal.Section Theorem_on_Rings.
Section Cs_CoIdeal.
Variables R S : CRing.
Variable sigma : RingHom R S.
Definition cspredR (x:R) : CProp := (sigma x) [#] 0.
Definition cswdpredR : (wd_pred R).
Defined.
Lemma cs_is_coideal : is_coideal cswdpredR.
Definition cs_as_coideal := Build_coideal R cswdpredR cs_is_coideal.
End Cs_CoIdeal.
Variables R S : CRing.
Variable sigma : RingHom R S.
Now we can `divide' R by ~CsR.
We now define the functions of which we want to prove the existence.
Definition Rtau (x:R) := (x:RdivCsR).
Lemma Rtau_strext : fun_strext Rtau.
Definition Rtau_is_fun := Build_CSetoid_fun R RdivCsR Rtau Rtau_strext.
Lemma Rtau_surj : surjective Rtau_is_fun.
Definition Rsigst (x:RdivCsR) := (sigma x).
Lemma Rsigst_strext : fun_strext Rsigst.
Definition Rsigst_is_fun := Build_CSetoid_fun RdivCsR S Rsigst Rsigst_strext.
Lemma Rsigst_inj : injective Rsigst_is_fun.
And now we have reached a goal: we can easily formulate and prove
the homomorphism theorem for rings.
Lemma RingHomTheorem : {Rtau : CSetoid_fun R RdivCsR | surjective Rtau}
and {Rsigst : CSetoid_fun RdivCsR S | injective Rsigst}.
End Theorem_on_Rings.