First Homomorphism Theorem

(* The first homomorphism theorem. See Meinke, Tucker Theorem 3.4.18. *)
(* Venanzio Capretta, January 1999                                    *)
(* Coq version 6.2.3                                                  *)

Require Export Homomorphisms.
Require Export Kernels.

Implicit Arguments On.

Section First_Homomorphism_Theorem.

Variable sigma : Signature.
Variable A, B : (Algebra sigma).
Variable phi : (Epimorphism A B).

Local n := (sorts_num sigma).
Local m := (fun_num sigma).

Local As := (sorts A).
Local Bs := (sorts B).

Local A_quot := (ker_quot phi).
Local nat_hom := (natural phi).

Local quots := (sorts A_quot).

Local psi : (s:(Finite n))(quots s) -> (Bs s) := [s](phi s).

Remark psi_well_defined :
  (s:(Finite n))(fun_well_defined (psi 1!s)).

Local psi_setoid : (s:(Finite n))(S_Fun (quots s) (Bs s)) :=
  [s](setoid_function (psi_well_defined 1!s)).

(* psi commutes with the functions of the algebra. *)

Lemma psi_is_homomorphism : (Is_homomorphism 2!A_quot 3!B psi_setoid).

Local psi_homo : (Homomorphism A_quot B) :=
  (homomorphism psi_is_homomorphism).

Remark psi_injective :
  (s:(Finite n))(injective (psi_homo s)).

Remark psi_surjective :
  (s:(Finite n))(surjective (psi_homo s)).

Remark psi_bijective :
  (s:(Finite n))(bijective (psi_homo s)).

Remark psi_is_iso : (is_isomorphism psi_homo).

Definition ker_quot_iso : (Isomorphism A_quot B) :=
  (isomorphism psi_is_iso).

Theorem first_homomorphism_theorem :
  (s:(Finite n))(x:(As s))
  ((phi s) x) [=] ((ker_quot_iso s) ((nat_hom s) x)).

End First_Homomorphism_Theorem.

Implicit Arguments Off.

25/02/99, 14:36