Kernels

(* Definition of the kernel of an homomorphism. *)
(* Venanzio Capretta, January 1999              *)
(* Coq version 6.2.3                            *)

Require Export Homomorphisms.
Require Export Congruences.

Implicit Arguments On.

Section Kernels.

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

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

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

Local ker_rel : (s : (Finite n))(relation (As s)) :=
  [s,a1,a2] ((phi s) a1) [=] ((phi s) a2).

Remark ker_well_defined :
  (s:(Finite n))(Relation_well_defined (ker_rel 1!s)).

Local ker_setoid : (s : (Finite n))(Setoid_relation (As s)) :=
  [s](setoid_relation (ker_well_defined 1!s)).

Remark ker_reflexive : (s : (Finite n))(reflexive (As s) (ker_rel 1!s)).

Remark ker_symmetric : (s : (Finite n))(symmetric (As s) (ker_rel 1!s)).

Remark ker_transitive : (s : (Finite n))(transitive (As s) (ker_rel 1!s)).

Remark ker_equivalence : (s : (Finite n))(Equiv (ker_rel 1!s)).

Section Kernel_Substitutivity.

(* We prove the substitutivity property for the kernel. *)

Variable i : (Finite m).

Local h := (nth_arity i).
Local a := (nth_arg 2!i).
Local r := (nth_result i).

Local fiA := (functions A i).
Local fiB := (functions B i).

Variables args1A, args2A : (Fun_arg_arguments A i).
Variable argsAeq : (j : (Finite h))((ker_setoid (a j)) (args1A j) (args2A j)).

Local args1B : (Fun_arg_arguments B i) := [j]((phi (a j)) (args1A j)).
Local args2B : (Fun_arg_arguments B i) := [j]((phi (a j)) (args2A j)).

Remark argsBeq : (j : (Finite h)) (args1B j) [=] (args2B j).

Remark argseq : args1B [=] args2B.

Remark phi_eq : (fiB args1B) [=] (fiB args2B).

Remark phi_comm1 : (fiB args1B) [=] ((phi r) (fiA args1A)).

Remark phi_comm2 : (fiB args2B) [=] ((phi r) (fiA args2A)).

Lemma ker_subst : ((ker_setoid r) (fiA args1A) (fiA args2A)).

End Kernel_Substitutivity.

Remark ker_substitutivity : (is_Congruence ker_setoid).

Definition kernel : (Congruence A) :=
  (congruence 3!ker_setoid ker_equivalence ker_substitutivity).

Definition ker_quot : (Algebra sigma) := (quotient kernel).

Local kers := (sorts ker_quot).

(* Natural map from A to the quotient A/kernel. *)

Local nat_fun : (s : (Finite n))(As s) -> (kers s) := [s,a]a.

Remark nat_fun_well_defined :
  (s : (Finite n))(fun_well_defined (nat_fun 1!s)).

Local nat_s_fun : (s : (Finite n))(S_Fun (As s) (kers s)) :=
  [s](setoid_function (nat_fun_well_defined 1!s)).

(* We prove now that nat_s_fun is an homomorphism. *)

Section Nat_Homomorphism.

Variable i : (Finite m).

Local h := (nth_arity i).
Local a := (nth_arg 2!i).
Local r := (nth_result i).

Local fiA := (functions A i).
Local fik := (functions ker_quot i).

Variable args : (Fun_arg_arguments A i).

Local argsk : (Fun_arg_arguments ker_quot i) :=
  [j]((nat_s_fun (a j)) (args j)).

Remark args_eq : (s_eq 1!(Fun_arg_arguments A i) argsk args).

Local resA := (fiA args).
Local resk := (fik argsk).

Remark resAk_eq : (s_eq 1!(sorts A r) resk resA).

Local resA' := ((nat_s_fun r) resA).

Remark nat_commutes_A : (s_eq 1!(sorts A r) resk resA').

Lemma nat_commutes : resk [=] resA'.

End Nat_Homomorphism.

Remark nat_is_homomorphism : (Is_homomorphism 2!A 3!ker_quot nat_s_fun).

Definition natural : (Homomorphism A ker_quot) :=
  (homomorphism nat_is_homomorphism).

End Kernels.

Implicit Arguments Off.

25/02/99, 14:36