Quellcode-Bibliothek homomorphisms.pvs
Sprache: unbekannt
|
|
homomorphisms[T1: TYPE,
*: [T1,T1 -> T1],
one1: T1,
T2: TYPE,
o: [T2,T2 -> T2],
one2: T2]: THEORY
%-----------------------------------------------------------------------------
% Experimental theory
%
% Author: Rick Butler
%
%-----------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING group_def
T1_is_group: ASSUMPTION group?[T1,*,one1](fullset[T1])
T2_is_group: ASSUMPTION group?[T2,o,one2](fullset[T2])
ENDASSUMING
IMPORTING group[T1,*,one1], group[T2,o,one2]
homomorphism?(G1: group[T1,*,one1],
G2: group[T2,o,one2],
phi: [(G1) -> (G2)]): bool =
(FORALL (a,b: (G1)): phi(a*b) = phi(a) o phi(b))
isomorphism?(G1: group[T1,*,one1],
G2: group[T2,o,one2],
phi: [(G1) -> (G2)]): bool = bijective?(phi) AND
homomorphism?(G1,G2,phi)
homomorphic?(G1: group[T1,*,one1],
G2: group[T2,o,one2]): bool =
EXISTS (phi: [(G1) -> (G2)]): homomorphism?(G1,G2,phi)
isomorphic?(G1: group[T1,*,one1],
G2: group[T2,o,one2]): bool =
EXISTS (phi: [(G1) -> (G2)]): isomorphism?(G1,G2,phi)
G: VAR group[T1,*,one1]
GP: VAR group[T2,o,one2]
homomorphism(G,GP): TYPE = {phi:[(G) -> (GP)] | homomorphism?(G,GP,phi)}
isomorphism (G,GP): TYPE = {phi:[(G) -> (GP)] | isomorphism?(G,GP,phi)}
homo_one: LEMMA FORALL (phi: homomorphism(G,GP)): phi(one1) = one2
kernel(G: group[T1,*,one1],
GP: group[T2,o,one2])(phi: homomorphism(G,GP)): subgroup[T1,*,one1](G) =
{a: T1 | G(a) AND phi(a) = one2}
END homomorphisms
[ 0.15Quellennavigators
Projekt
]
|
2026-03-28
|
