|
%%-------------------** Normalizer, Centralizer and Class Equation **-------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%--------------------------------------------------------------------------------------
normalizer_centralizer[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@normal_subgroups[T,*,one],
group_action[T,*,one,T]
G, H: VAR group
a, x: VAR T
%%%%% Definitions %%%%%
normalizer(G:group, H:subgroup(G)): {S: set[T] | subset?(S,G)} = { x: (G) | inv(x) * H * x = H}
centralizer(G)(a): {S: set[T] | subset?(S,G)} = { x: (G) | x * a = a * x}
a_by_c(G:group, H:subgroup(G))(h:(H), x:(G)): (G) = h * x * inv(h)
CL(G)(x): {X: set[T] | subset?(X,G)} = { y: (G) | EXISTS (g: (G)): y = g * x * inv(g)}
CLs(G): setofsets[T] = {X: set[T] | EXISTS (x: (G)): X = CL(G)(x)}
CLs_nc(G): setofsets[T] = {X: (CLs(G)) | EXISTS (x: {x:(G) |
NOT member(x, center(G))}): X = CL(G)(x)}
%%%%% Properties and results %%%%%
normalizer_is_subgroup: LEMMA subgroup?(H,G) IMPLIES subgroup?(normalizer(G,H), G)
subset_of_normalizer: LEMMA subgroup?(H,G) IMPLIES subset?(H, normalizer(G,H))
normal_in_normalizer: LEMMA subgroup?(H,G) IMPLIES
normal_subgroup?(H, normalizer(G,H))
centralizer_is_subgroup: LEMMA subgroup?(centralizer(G)(a), G)
singleton_iff_center: LEMMA FORALL (x:(G)): CL(G)(x) = singleton(x) IFF member(x, center(G))
a_by_c_is_action: LEMMA subgroup?(H,G) IMPLIES group_action?(H,G)(a_by_c(G,H))
Fix_is_center: LEMMA Fix(G,G)(a_by_c(G,G)) = center(G)
stabilizer_is_centralizer: LEMMA FORALL (x:(G)): stabilizer(G,G)(a_by_c(G,G), x) = centralizer(G)(x)
orbit_is_CL: LEMMA FORALL (x:(G)): orbit(G,G)(a_by_c(G,G), x) = CL(G)(x)
orbits_is_CLs: LEMMA orbits(G,G)(a_by_c(G,G)) = CLs(G)
orbits_nFix_is_CLs_nc: LEMMA orbits_nFix(G,G)(a_by_c(G,G)) = CLs_nc(G)
CLs_eq_index: LEMMA FORALL (G:finite_group, x:(G)): index(G, centralizer(G)(x)) = card(CL(G)(x))
%%%%% Class Equation %%%%%%%%%%%%%%%%%%%%%%%%
% ----
% sigma(X, f) = \ f(x)
% /
% ----
% member(x,X)
class_equation_2: LEMMA FORALL (G:finite_group):
order(G) = card(center(G)) + sigma_set.sigma(CLs_nc(G), card)
END normalizer_centralizer
¤ Dauer der Verarbeitung: 0.15 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.
|
