Section RingHom_Definition.
Variables R S : CRing.
Section RingHom_Preliminary.
Variable phi : CSetoid_fun R S.
Definition fun_pres_plus := forall x y:R, phi (x[+]y) [=] (phi x) [+] (phi y).
Definition fun_pres_mult := forall x y:R, phi (x[*]y) [=] (phi x) [*] (phi y).
Definition fun_pres_unit := (phi (1:R)) [=] (1:S).
End RingHom_Preliminary.
Record RingHom : Type :=
{rhmap :> CSetoid_fun R S;
rh1 : fun_pres_plus rhmap;
rh2 : fun_pres_mult rhmap;
rh3 : fun_pres_unit rhmap}.
End RingHom_Definition.
Lemmas on Ring Homomorphisms
Let R and S be rings and f a ring homomorphism from R to S.Axioms on Ring Homomorphisms
Section RingHom_Lemmas.
Variables R S : CRing.
Section RingHom_Axioms.
Variable f : RingHom R S.
Lemma rh_strext : forall x y:R, (f x) [#] (f y) -> x [#] y.
Lemma rh_pres_plus : forall x y:R, f (x[+]y) [=] (f x) [+] (f y).
Lemma rh_pres_mult : forall x y:R, f (x[*]y) [=] (f x) [*] (f y).
Lemma rh_pres_unit : (f (1:R)) [=] (1:S).
End RingHom_Axioms.
Section RingHom_Basics.
Variable f : RingHom R S.
Lemma rh_pres_zero : (f (0:R)) [=] (0:S).
Lemma rh_pres_inv : forall x:R, (f [--]x) [=] [--] (f x).
Lemma rh_pres_minus : forall x y:R, f (x[-]y) [=] (f x) [-] (f y).
Lemma rh_apzero : forall x:R, (f x) [#] 0 -> x [#] 0.
Lemma rh_pres_nring : forall n, (f (nring n:R)) [=] (nring n:S).
End RingHom_Basics.
End RingHom_Lemmas.
Definition RHid R : RingHom R R.
Defined.
Section Compose.
Variable R S T : CRing.
Variable phi : RingHom S T.
Variable psi : RingHom R S.
Lemma RHcompose1 : fun_pres_plus _ _ (compose_CSetoid_fun _ _ _ psi phi).
Lemma RHcompose2 : fun_pres_mult _ _ (compose_CSetoid_fun _ _ _ psi phi).
Lemma RHcompose3 : fun_pres_unit _ _ (compose_CSetoid_fun _ _ _ psi phi).
Definition RHcompose : RingHom R T := Build_RingHom _ _ _ RHcompose1 RHcompose2 RHcompose3.
End Compose.