Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: right_left_cosets.pvs Sprache: PVS

Original von: PVS^©

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