|
factor_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%-----------------------------------------------------------------------------
% Experimental theory working towards factor groups
%
% Author: Rick Butler
%
%-----------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING normal_subgroups[T,*,one]
AUTO_REWRITE+ member
H,G: VAR group[T,*,one]
a,b,h: VAR T
p0: LEMMA FORALL (G: group, H: normal_subgroup(G), A,B: left_cosets(G, H)):
nonempty?[set[T]]({S: set[T] | EXISTS (a, b: (G)):
A = a*H AND B = b*H AND S = (a * b)*H })
prep: LEMMA FORALL (a1,a2,b1,b2: (G)): FORALL (H: normal_subgroup(G)):
a1*H = a2*H AND b1*H = b2*H IMPLIES (a1*b1)*H = (a2*b2)*H
mult_prep: LEMMA FORALL (G: group, H: normal_subgroup(G), A,B: left_cosets(G, H)):
singleton?[set[T]] ({S: set[T] | EXISTS (a, b: (G)):
A = a*H AND B = b*H AND S = (a * b)*H })
AUTO_REWRITE+ left_coset
mult(G:group,H:normal_subgroup(G))(A,B: left_cosets(G,H)): left_cosets(G,H) =
lc_gen(G,H,A)*lc_gen(G,H,B)*H
mult_lem : LEMMA FORALL (G: group, H: normal_subgroup(G), a,b: (G)):
mult(G,H)(a*H,b*H) = (a*b)*H
mult_in : LEMMA FORALL (G: group, H: normal_subgroup(G)),(A,B: left_cosets(G,H)):
mult(G, H)(A,B)(a) IMPLIES G(a)
mult_is_coset: LEMMA FORALL (G: group, H: normal_subgroup(G)),(A,B: left_cosets(G,H)):
EXISTS (a: (G)): mult(G, H)(A,B) = a*H
N_is_identity: LEMMA FORALL (G: group, N: normal_subgroup(G)), (A: left_cosets(G,N)):
mult(G,N)(N,A) = A AND mult(G,N)(A,N) = A
IMPORTING group
left_cosets_group: THEOREM FORALL (G: group, N: normal_subgroup(G)):
group?[left_cosets(G, N), mult(G, N), N](fullset[left_cosets(G, N)])
; %% ----- define G/N as set of all left_cosets
/(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N]
= fullset[left_cosets(G, N)]
over(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N]
= fullset[left_cosets(G, N)]
factor_type(G:group,N:normal_subgroup(G)): TYPE+ = left_cosets(G,N)
END factor_groups
¤ Dauer der Verarbeitung: 0.0 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.
|
