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