%%-------------------** 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