Homomorphisms


(* Definition of homomorphism between algebras. *)
(* Venanzio Capretta, January 1999              *)
(* Coq version 6.2.3                            *)

Require Export Algebras.

Implicit Arguments On.

Section Algebras_Homomorphisms.

Variable sigma : Signature.
Variables A, B : (Algebra sigma).

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

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

Section Homomorphism_Commutes.

(* An homomorphism consist first of all in a family of setoid functions. *)
Variable phi : (i : (Finite n))(S_Fun (As i) (Bs i)).

(* This function must commute with the functions of the signature. *)

Variable i : (Finite m). (* we choose the i-th function. *)

Local fi := (nth_function i).
Local r := (function_type_arity fi).
Local a := (function_type_arg 2!fi).
Local h := (function_type_result fi).

(* Interpretations of the i-th function in the two algebras. *)
Local giA := (functions A i).
Local giB := (functions B i).

(* Let us choose generic arguments for giA. *)
Variable argsA : (Fun_arg_arguments A i).

(* The corresponding arguments for B are obtained by an application of phi. *)
Local argsB : (Fun_arg_arguments B i) :=
  [j : (Finite r)]((phi (a j)) (argsA j)).

Local resA := (giA argsA).
Local resB := (giB argsB).

(* Now phi is an homomorphisms if applying phi to resA yields resB. *)
Definition phi_commutes :=
  resB [=] ((phi h) resA).

End Homomorphism_Commutes.

Definition
Is_homomorphism :=
  [phi : (i : (Finite n))(S_Fun (As i) (Bs i))]
  (i : (Finite m))(args : (Fun_arg_arguments A i))
  (phi_commutes phi args).

(* We can now define the type of homomorphisms. *)
Record
Homomorphism : Set := homomorphism
  { hom_function :> (i : (Finite n))(S_Fun (As i) (Bs i));
    hom_proof : (Is_homomorphism hom_function)
  }.

(* Definition of monomorphisms, epimorphisms and isomorphisms. *)

Definition
is_monomorphism :=
  [phi : Homomorphism]
  (i : (Finite n))(injective (phi i)).

Definition
is_epimorphism :=
  [phi : Homomorphism]
  (i : (Finite n))(surjective (phi i)).

Definition
is_isomorphism :=
  [phi : Homomorphism]
  (i : (Finite n))(bijective (phi i)).

Record
Monomorphism : Set := monomorphism
  { mono_homomorphism :> Homomorphism;
    mono_proof : (is_monomorphism mono_homomorphism)
  }.

Record
Epimorphism : Set := epimorphism
  { epi_homomorphism :> Homomorphism;
    epi_proof : (is_epimorphism epi_homomorphism)
  }.

Record
Isomorphism : Set := isomorphism
  { iso_homomorphism :> Homomorphism;
    iso_proof : (is_isomorphism iso_homomorphism)
  }.

(* A and B are isomorphic if there is an isomorphism. *)
(* This may look silly, but that's what it is.        *)
Definition
Isomorphic := Isomorphism.

End Algebras_Homomorphisms.

(* Definition of Endomorphisms and Automorphisms. *)

Definition
Endomorphism :=
  [sigma : Signature][A : (Algebra sigma)]
  (Homomorphism A A).

Definition
Automorphism :=
  [sigma : Signature][A : (Algebra sigma)]
  (Isomorphism A A).

(* Identity Isomorphisms. *)

Section Identity_Isomorphisms.

Variable sigma : Signature.
Variable A : (Algebra sigma).

Local n := (sorts_num sigma).
Local m := (fun_num sigma).
Local As := (sorts A).

Local id_sf :=
[i : (Finite n)](b_function (s_id_bij (As i))).

Local id_is_bij :=
[i : (Finite n)](b_proof (s_id_bij (As i))).

(* Proof that id_sf is an homomorphism. *)
Section Id_Homomorphism.

Variable i : (Finite m).

Local fi := (nth_function i).
Local r := (function_type_arity fi).
Local a := (function_type_arg 2!fi).
Local h := (function_type_result fi).

Local fiA := (functions A i).

Variable args : (Fun_arg_arguments A i).
Local id_args : (Fun_arg_arguments A i)
                 := [j]((id_sf (a j)) (args j)).
Local fi_args := (fiA args).
Local fi_id_args := (fiA id_args).
Local id_fi_args := ((id_sf h) fi_args).

(* We want to prove that fi_id_args is equal to id_fi_args. *)

Remark id_args_eq :
  (j : (Finite r)) (args j) [=] (id_args j).

Remark id_args_setoid_eq :
  id_args [=] args.

Remark fi_result_eq :
  fi_id_args [=] fi_args.

Lemma
id_sf_commutes_with_functions :
  fi_id_args [=] id_fi_args.

End Id_Homomorphism.

Lemma
id_sf_is_homomorphism : (Is_homomorphism id_sf).

Local id_endo : (Endomorphism A) :=
  (homomorphism id_sf_is_homomorphism).

Definition
id_auto : (Automorphism A) :=
  (isomorphism 4!id_endo id_is_bij).

End Identity_Isomorphisms.

Implicit Arguments Off.

25/02/99, 14:36