Require Export CRings.
Set Automatic Introduction.

Section RingHom_Definition.

Variables R S : CRing.

Section RingHom_Preliminary.

Variable phi : CSetoid_fun R S.

Definition fun_pres_plus := ∀ x y:R, phi (x+y) ≡ (phi x) + (phi y).
Definition fun_pres_mult := ∀ 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.

Section RingHom_Lemmas.

Variables R S : CRing.

Section RingHom_Axioms.

Variable f : RingHom R S.

Lemma rh_strext : ∀ x y:R, (f x) [#] (f y) → x [#] y.
Proof.
 elim f; intuition.
 assert (fun_strext rhmap0); elim rhmap0; intuition.
Qed.

Lemma rh_pres_plus : ∀ x y:R, f (x+y) ≡ (f x) + (f y).
Proof.
 elim f; auto.
Qed.

Lemma rh_pres_mult : ∀ x y:R, f (x×y) ≡ (f x) × (f y).
Proof.
 elim f; auto.
Qed.

Lemma rh_pres_unit : (f (1:R)) ≡ (1:S).
Proof.
 elim f; auto.
Qed.

End RingHom_Axioms.

Hint Resolve rh_strext rh_pres_plus rh_pres_mult rh_pres_unit : algebra.

Section RingHom_Basics.

Variable f : RingHom R S.

Lemma rh_pres_zero : (f (0:R)) ≡ (0:S).
Proof.
 astepr ((f 0)[-](f 0)).
 astepr ((f (0+0))[-](f 0)).
 Step_final ((f 0+f 0)[-]f 0).
Qed.

Lemma rh_pres_inv : ∀ x:R, (f −x) ≡ − (f x).
Proof.
 intro x; apply (cg_cancel_lft S (f x)).
 astepr (0:S).
 astepl (f (x+−x)).
 Step_final (f (0:R)); try apply rh_pres_zero.
Qed.

Lemma rh_pres_minus : ∀ x y:R, f (x−y) ≡ (f x) − (f y).
Proof.
 unfold cg_minus.
 intros x y.
 rewrite → rh_pres_plus.
 rewrite → rh_pres_inv.
 reflexivity.
Qed.

Lemma rh_apzero : ∀ x:R, (f x) [#] 0 → x [#] 0.
Proof.
 intros x X; apply (cg_ap_cancel_rht R x (0:R) x).
 astepr x.
 apply (rh_strext f (x+x) x).
 astepl ((f x)[+](f x)).
 astepr ((0:S) + (f x)).
 apply (op_rht_resp_ap S (f x) (0:S) (f x)).
 assumption.
Qed.

Lemma rh_pres_nring : ∀ n, (f (nring n:R)) ≡ (nring n:S).
Proof.
 induction n.
  apply rh_pres_zero.
 simpl.
 rewrite → rh_pres_plus;auto with ×.
Qed.

End RingHom_Basics.

End RingHom_Lemmas.

Hint Resolve rh_strext rh_pres_plus rh_pres_mult rh_pres_unit : algebra.
Hint Resolve rh_pres_zero rh_pres_minus rh_pres_inv rh_apzero : algebra.
Hint Rewrite rh_pres_zero rh_pres_plus rh_pres_minus rh_pres_inv rh_pres_mult rh_pres_unit : ringHomPush.

Definition RHid R : RingHom R R.
Proof.
 ∃ (id_un_op R).
   intros x y; apply eq_reflexive.
  intros x y; apply eq_reflexive.
 apply eq_reflexive.
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).
Proof.
 intros x y.
 simpl.
 repeat rewrite → rh_pres_plus;reflexivity.
Qed.

Lemma RHcompose2 : fun_pres_mult _ _ (compose_CSetoid_fun _ _ _ psi phi).
Proof.
 intros x y.
 simpl.
 repeat rewrite → rh_pres_mult; reflexivity.
Qed.

Lemma RHcompose3 : fun_pres_unit _ _ (compose_CSetoid_fun _ _ _ psi phi).
Proof.
 unfold fun_pres_unit.
 simpl.
 repeat rewrite → rh_pres_unit; reflexivity.
Qed.

Definition RHcompose : RingHom R T := Build_RingHom _ _ _ RHcompose1 RHcompose2 RHcompose3.

End Compose.