|
cosets[T:Type+,*:[T,T->T],one:T]: THEORY
%------------------------------------------------------------------------------
% Left and Right Cosets
%
% Author: Rick Butler, NASA Langley
% Adapted from work done by David Lester, Manchester
%
% Version 1.0 12/12/07
%
% This theory defines convenient notation:
%
% a*H -- left coset
% H*a -- right coset
%
%------------------------------------------------------------------------------
BEGIN
%------------------------------------------------------------------------
% The imported type T with * and one must be a group.
% From this foundation other groups are created. These are just subgroups of the
% underlying imported type.
%------------------------------------------------------------------------
ASSUMING IMPORTING group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING group[T,*,one]
S,R: VAR set[T]
H,G: VAR group
a,b,x,y,z: VAR T
m: VAR nat
% Herstein Lemma 2.4.3
congruent_mod(G:group,H:subgroup(G))(a,b:T):bool
= member(a*inv(b),H)
congruence_is_equivalence: LEMMA
subgroup?(H,G) IMPLIES equivalence?[T](congruent_mod(G,H))
% ---------- Special Coset Notation ------------
;
*(a: T, H: set[T]): set[T] = {t:T | EXISTS (h:(H)): t = a*h} ; %% left
*(H: set[T], a: T): set[T] = {t:T | EXISTS (h:(H)): t = h*a} ; %% right
left_coset_subset : LEMMA FORALL (H: subgroup(G)),(a:(G)): subset?(a*H,G)
right_coset_subset: LEMMA FORALL (H: subgroup(G)),(a:(G)): subset?(H*a,G)
left_coset_one : LEMMA one*S = S
right_coset_one : LEMMA S*one = S
left_coset_assoc : LEMMA a*(b*S) = (a*b)*S
right_coset_assoc : LEMMA (S*a)*b = S*(a*b)
lr_coset_assoc : LEMMA (a*S)*b = a*(S*b)
subset_left_coset : LEMMA subset?(S, R) IMPLIES subset?(a*S, a*R)
subset_right_coset: LEMMA subset?(S, R) IMPLIES subset?(S*a, R*a)
% ------------- Cosets ------------------------
% Herstein Lemma 2.4.4
right_coset(G:group,H:subgroup(G))(a:(G)): { s: set[T] | subset?(s,G)}
%% was set[(G)]
= H*a
% = image((LAMBDA (h:(H)): h*a),(H))
right_coset_image: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
right_coset(G,H)(a) = image((LAMBDA (h:(H)): h*a),(H))
right_coset_is: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
right_coset(G,H)(a) = {x: T | congruent_mod(G,H)(a,x)}
right_coset_def : LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
right_coset(G,H)(a) = H*a
% Herstein Lemma 2.4.5
nonempty_right_coset: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
nonempty?(right_coset(G,H)(a))
right_coset_correspondence: LEMMA FORALL (A,B:set[T]):
subgroup?(H,G) AND member(a,G) AND member(b,G) AND
A = right_coset(G,H)(a) AND B = right_coset(G,H)(b) IMPLIES
EXISTS (f:[(A)->(B)]): bijective?(f)
% left stuff
left_coset(G:group,H:subgroup(G))(a:(G)): { s: set[T] | subset?(s,G)}
%% was set[(G)]
= a*H
% = image((LAMBDA (h:(H)): a*h),(H))
left_coset_image : LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
left_coset(G,H)(a) = image((LAMBDA (h:(H)): a*h),(H))
left_coset_def : LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
left_coset(G,H)(a) = a*H
% ---- Define Types ----
left_cosets(G:group,H:subgroup(G)): TYPE = {s: set[T] |
EXISTS (a: (G)): s = a*H}
right_cosets(G:group,H:subgroup(G)): TYPE = {s: set[T] |
EXISTS (a: (G)): s = H*a}
% --- retrieve a generator -- not unique
lc_gen(G:group, H: subgroup(G),lc: left_cosets(G,H)): {a: T | G(a) AND lc = a*H} =
choose({a: T | G(a) AND lc = a*H})
lc_gen_def: LEMMA subgroup?(H,G) AND G(a) IMPLIES
lc_gen(G,H,a*H)*H = a*H
rc_gen(G:group, H: subgroup(G), rc: right_cosets(G,H)): {a: T | G(a) AND rc = H*a} =
choose({a: T | G(a) AND rc = H*a})
rc_gen_def: LEMMA subgroup?(H,G) AND G(a) IMPLIES
H*rc_gen(G,H,H*a) = H*a
lc_eq : LEMMA subgroup?(H,G) AND a*H = b*H
IMPLIES (EXISTS (h: (H)): a = b*h)
lc_is_eq : LEMMA subgroup?(H,G) AND (EXISTS (h: (H)): a = b*h)
IMPLIES a*H = b*H
rc_eq : LEMMA subgroup?(H,G) AND H*a = H*b
IMPLIES (EXISTS (h: (H)): a = h*b)
rc_is_eq : LEMMA subgroup?(H,G) AND (EXISTS (h: (H)): a = h*b)
IMPLIES H*a = H*b
END cosets
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
