CoRN.old.CModule_Homomorphisms
Require Export CModules.
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 := ∀ 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 := ∀ (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.
Implicit Arguments ModHom [R].
Implicit Arguments hommap [R].
Implicit Arguments hom1 [R].
Implicit Arguments hom2 [R].
Implicit Arguments hom3 [R].
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 : ∀ x y:A, (f x) [#] (f y) → x [#] y.
Proof.
elim f; intuition.
assert (fun_strext hommap0); elim hommap0; intuition.
Qed.
Lemma mh_pres_plus : ∀ x y:A, f (x+y) ≡ (f x) + (f y).
Proof.
elim f; auto.
Qed.
Lemma mh_pres_unit : (f (cm_unit A)) ≡ (cm_unit B).
Proof.
elim f; auto.
Qed.
Lemma mh_pres_mult : ∀ (a:R)(x:A), f (rm_mu A a x) ≡ rm_mu B a (f x).
Proof.
elim f; auto.
Qed.
End ModHom_Axioms.
Hint Resolve mh_strext mh_pres_plus mh_pres_unit mh_pres_mult : algebra.
Section ModHom_Basics.
Variable f : ModHom A B.
Lemma mh_pres_zero : (f (0:A)) ≡ (0:B).
Proof.
astepr ((f 0)[-](f 0)).
astepr ((f (0+0))[-](f 0)).
Step_final ((f 0+f 0)[-]f 0).
Qed.
Lemma mh_pres_minus : ∀ x:A, (f −x) ≡ − (f x).
Proof.
intro x; apply (cg_cancel_lft B (f x)).
astepr (0:B).
astepl (f (x[+][--]x)).
Step_final (f (0:A)); try apply mh_pres_zero.
Qed.
Lemma mh_apzero : ∀ x:A, (f x) [#] 0 → x [#] 0.
Proof.
intros x X; apply (cg_ap_cancel_rht A x (0:A) x).
astepr x.
apply (mh_strext f (x+x) x).
astepl ((f x)[+](f x)).
astepr ((0:B) + (f x)).
apply (op_rht_resp_ap B (f x) (0:B) (f x)).
assumption.
Qed.
End ModHom_Basics.
End ModHom_Lemmas.
Implicit Arguments mh_strext [R].
Implicit Arguments mh_pres_plus [R].
Implicit Arguments mh_pres_unit [R].
Implicit Arguments mh_pres_mult [R].
Implicit Arguments mh_pres_zero [R].
Implicit Arguments mh_pres_minus [R].
Implicit Arguments mh_apzero [R].
Hint Resolve mh_strext mh_pres_plus mh_pres_unit mh_pres_mult : algebra.
Hint Resolve mh_pres_zero mh_pres_minus mh_apzero : algebra.