Module Homomorphisms
Definition of Module Homomorphisms
Let R be a ring, let A and B be R-Modules and phi : A -> B.Section ModHom_Definition.
Variable R : CRing.
Variables A B : RModule R.
Section ModHom_Preliminary.
Variable phi : CSetoid_fun A B.
Definition fun_pres_plus := forall x y:A, phi (x [+] y) [=] (phi x) [+] (phi y).
Definition fun_pres_unit := (phi (cm_unit A)) [=] (cm_unit B).
Definition fun_pres_mult := forall (a:R)(x:A), phi (rm_mu A a x) [=] rm_mu B a (phi x).
End ModHom_Preliminary.
Record ModHom : Type :=
{hommap :> CSetoid_fun A B;
hom1 : fun_pres_plus hommap;
hom2 : fun_pres_unit hommap;
hom3 : fun_pres_mult hommap}.
End ModHom_Definition.
Lemmas on Module Homomorphisms
Let R be a ring, A and B R-Modules and f a module homomorphism from A to B.Axioms on Module Homomorphisms
Section ModHom_Lemmas.
Variable R : CRing.
Variables A B : RModule R.
Section ModHom_Axioms.
Variable f : ModHom A B.
Lemma mh_strext : forall x y:A, (f x) [#] (f y) -> x [#] y.
Lemma mh_pres_plus : forall x y:A, f (x[+]y) [=] (f x) [+] (f y).
Lemma mh_pres_unit : (f (cm_unit A)) [=] (cm_unit B).
Lemma mh_pres_mult : forall (a:R)(x:A), f (rm_mu A a x) [=] rm_mu B a (f x).
End ModHom_Axioms.
Section ModHom_Basics.
Variable f : ModHom A B.
Lemma mh_pres_zero : (f (0:A)) [=] (0:B).
Lemma mh_pres_minus : forall x:A, (f [--]x) [=] [--] (f x).
Lemma mh_apzero : forall x:A, (f x) [#] 0 -> x [#] 0.
End ModHom_Basics.
End ModHom_Lemmas.