Quelle right_left_cosets.pvs Sprache: 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

quality87%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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:

sprechenden Kalenders