Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: group_action.pvs Sprache: PVS

Original von: PVS^©

%%-------------------** Group Action and Class Equation **-------------------
%%
%% Author          : André Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%---------------------------------------------------------------------------

group_action[T: TYPE, *: [T,T -> T], one: T, T1: TYPE]: THEORY

BEGIN

     ASSUMING IMPORTING algebra@group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING algebra@group[T,*,one],
             algebra@factor_groups[T,*,one],
             lagrange_index[T,*,one],
             class_equation_scaf[set[T1],T1],
             groups_scaf

    G, H, K: VAR group[T,*,one]
       X, Y: VAR set[T1]
          p: VAR posnat
          n: VAR nat
     F(G,X): TYPE = [(G), (X) -> (X)]

%%%%% Definitions %%%%

   group_action?(G, X)(f:F(G,X)): bool = FORALL (g1, g2:(G), x: (X)):
                             f(one, x) = x AND f(g1 * g2, x) = f(g1, f(g2, x))

   stabilizer(G,X)(f: F(G,X), x: (X)): {S: set[T] | subset?(S,G)} = {g:(G) | f(g,x) = x}

   orbit(G,X)(f: F(G,X), x: (X)): {Y: set[T1] | subset?(Y,X)} = {y:(X) | EXISTS (g:(G)): y = f(g, x)}

   orbits(G,X)(f: F(G,X)): setofsets[T1] = {Y: set[T1] | EXISTS (x:(X)): Y = orbit(G,X)(f,x)}


   Fix(G,X)(f: F(G,X)): {Y: set[T1] | subset?(Y,X)} = {x:(X) | FORALL (g:(G)): f(g, x) = x}

   orbits_nFix(G,X)(f: F(G,X)): setofsets[T1] = {Y: (orbits(G,X)(f)) |
                                     EXISTS (x: {x:(X) | NOT member(x, Fix(G,X)(f))}): Y = orbit(G,X)(f,x)}

%%%%% Properties and results %%%%

   stabilizer_is_subgroup: LEMMA FORALL (x:(X), f:F(G,X)):
                              group_action?(G, X)(f) IMPLIES subgroup?(stabilizer(G,X)(f, x), G)

   singleton_iff_Fix: LEMMA FORALL (x:(X), f:F(G,X)):
                         group_action?(G, X)(f)
                            IMPLIES
                              (orbit(G,X)(f,x) = singleton(x) IFF member(x, Fix(G,X)(f)))

   empty_iff_eq_Fix: LEMMA FORALL (f:F(G,X)):
                              group_action?(G, X)(f)
                                 IMPLIES
                                    (empty?(orbits_nFix(G,X)(f)) IFF X = Fix(G,X)(f))

   orbits_nFix_disj_Fix: LEMMA FORALL (f:F(G,X)):
                            group_action?(G, X)(f)
                               IMPLIES disjoint?(Fix(G,X)(f),Union(orbits_nFix(G,X)(f)))

   orbits_is_union: LEMMA FORALL (f:F(G,X)):
                       group_action?(G, X)(f)
                          IMPLIES Union(orbits(G,X)(f)) = union(Fix(G,X)(f), Union(orbits_nFix(G,X)(f)))

   orbit_nonempty: LEMMA FORALL (x:(X), f:F(G,X)):
                      group_action?(G, X)(f) IMPLIES nonempty?(orbit(G,X)(f,x))

   orbits_nonempty: LEMMA FORALL (f:F(G,X)): nonempty?(X) AND group_action?(G, X)(f)
                             IMPLIES nonempty?(orbits(G,X)(f))

   set_orbits_is: LEMMA FORALL (f:F(G,X)): group_action?(G, X)(f)
                          IMPLIES Union(orbits(G,X)(f)) = X

   orbit_is_finite: LEMMA FORALL (x:(X), f:F(G,X)):
                            is_finite(X) AND group_action?(G, X)(f)
                               IMPLIES
                                  is_finite(orbit(G,X)(f,x))

   orbits_disjoint: LEMMA FORALL (f:F(G,X), A,B: (orbits(G,X)(f))):
                             group_action?(G, X)(f)
                                IMPLIES
                                   A = B OR disjoint?(A,B)

   orbits_partition: LEMMA  FORALL (f:F(G,X)):
                              is_finite(X) AND group_action?(G, X)(f)
                                IMPLIES
                                   finite_partition?(orbits(G,X)(f))

   orbits_nFix_partition: LEMMA FORALL (f:F(G,X)):
                                   is_finite(X) AND group_action?(G, X)(f)
                                      IMPLIES
                                         finite_partition?(orbits_nFix(G,X)(f))

   orbits_eq_index_aux: LEMMA
      FORALL (x:(X), f:F(G,X)): group_action?(G, X)(f)
        IMPLIES
          EXISTS (f:[(left_cosets(G,stabilizer(G,X)(f, x))) -> (orbit(G,X)(f,x))]): bijective?(f)

   orbits_eq_index: LEMMA FORALL (G:finite_group, x:(X), f:F(G,X)):
                         is_finite(X) AND group_action?(G, X)(f)
                            IMPLIES
                              index(G, stabilizer(G,X)(f, x)) = card(orbit(G,X)(f,x))

%%%%% Class Equation %%%%%%%%%%%%%%%%%%%%%%%%

%                 ----
%  sigma(X, f) =  \     f(x)
%                 /
%                 ----
%              member(x,X)

   counting_formula: LEMMA FORALL (f:F(G,X)):
                             finite_group?(G) AND is_finite(X) AND
                             nonempty?(X)     AND group_action?(G, X)(f)
                                IMPLIES
                                  card(X) = sigma_set.sigma(orbits(G,X)(f), card)

   class_equation: LEMMA FORALL (f:F(G,X)):
                            finite_group?(G) AND is_finite(X) AND
                            nonempty?(X)     AND group_action?(G, X)(f)
                               IMPLIES
                                  card(X) = card(Fix(G,X)(f)) + sigma_set.sigma(orbits_nFix(G,X)(f), card)

   Fix_congruence: LEMMA FORALL (f:F(G,X)):
                            finite_group?(G) AND order(G) = p^n AND
                            is_finite(X)     AND nonempty?(X)   AND
                            prime?(p)        AND group_action?(G, X)(f)
                              IMPLIES
                                 divides(p, card(X) - card(Fix(G,X)(f)))

END group_action

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.