|
%%-------------------** Right, left cosets and some properties **-------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------------------------------
right_left_cosets[T:Type,*:[T,T->T],one:T]: THEORY
BEGIN
ASSUMING IMPORTING algebra@group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING algebra@lagrange[T,*,one],
algebra@factor_groups,
finite_sets@finite_sets_eq[T,T],
finite_sets@finite_sets_card_eq
G,H, N: VAR group
a, b: VAR T
left_cosets(G:group, H:subgroup(G)): setofsets[T] = {s: set[T] | EXISTS (a: (G)): s = a*H}
right_cosets(G:group, H:subgroup(G)): setofsets[T] = {s: set[T] | EXISTS (a: (G)): s = H*a}
%%%%%%%%%
nonempty_left_coset: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
nonempty?(left_coset(G,H)(a))
left_coset_finite: LEMMA
FORALL (G:finite_group): subgroup?(H,G) AND member(a,G) IMPLIES
is_finite(left_coset(G,H)(a))
left_coset_correspondence: LEMMA
FORALL (A:set[T]): subgroup?(H,G) AND member(a,G) AND A = left_coset(G,H)(a)
IMPLIES
EXISTS (f:[(H)->(A)]): bijective?(f)
left_coset_correspondence_inv: LEMMA
subgroup?(H,G) AND member(a,G)
IMPLIES
EXISTS (f:[(H)->(a*H*inv(a))]): bijective?(f)
finite_left_coset_correspondence: LEMMA
FORALL (G:finite_group): subgroup?(H,G) AND member(a,G) AND member(b,G)
IMPLIES
card(left_coset(G,H)(a)) = card(left_coset(G,H)(b))
set_left_cosets_full: LEMMA FORALL (H: subgroup(G)): Union(left_cosets(G,H)) = G
left_cosets_disjoint: LEMMA FORALL (H: subgroup(G), A,B: left_cosets(G, H)):
A = B OR disjoint?(A,B)
left_cosets_partition: LEMMA FORALL (G:finite_group, H: subgroup(G)):
finite_partition?[T](left_cosets(G, H))
set_right_cosets_full_1: LEMMA FORALL (H: subgroup(G)): Union(right_cosets(G,H)) = G
right_left_correspondence: LEMMA
subgroup?(H,G) IMPLIES
EXISTS (f:[(right_cosets(G, H)) -> (left_cosets(G,H))]): bijective?(f)
finite_right_left_correspondence: LEMMA
FORALL (G:finite_group): subgroup?(H,G)
IMPLIES
card[set[T]](right_cosets(G,H)) = card[set[T]](left_cosets(G,H))
%% index of H in G is the number of left (right) cosets of H in G %%
index(G:finite_group, H:subgroup(G)): nat = card[set[T]](left_cosets(G, H))
index_gt1: LEMMA FORALL (G:finite_group, H:subgroup(G)): index(G,H) >= 1
;%% define G/N as set of all left cosets of N in G
/(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N] = left_cosets(G, N)
;%% order of G/N
card_factor: LEMMA finite_group?(G) AND normal_subgroup?(N, G)
IMPLIES card[set[T]](G/N) = index(G,N)
END right_left_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.
|
