Ein Gruppenkriterium basierend auf der Verknüpfungstabelle einer algebraischen Struktur

In dieser Arbeit beschreiben wir ein einfaches Kriterium, mit dessen Hilfe entschieden werden kann, ob eine gegebene Menge mit einer dazugehörigen Verknüpfung eine Gruppe bildet oder nicht. Dieser Test bezieht sich auf die Struktur der Verknüpfungstabelle der Abbildung auf der Menge. Wir werden zeigen, dass in einer Gruppe jede Zeile und jede Spalte der Verknüpfungstabelle eine Permutation der Gruppenelemente sein muss.

Formalisierung in der Theorema Sprache

Needs["Theorema`"]

Notwendige mathematische Begriffe

𝒯[∘,A][a, b] := 
      a∘b

𝒵[a, ∘,A][
        b] := 𝒯[∘,A][a, 
        b]

𝒮[b, ∘,A][
        a] := 𝒯[∘,A][a, 
        b]

Definition["Verknüpfungstabelle, Zeile",any[∘,A,a,b],
({{(Subscript[𝒯, A, ∘])[a, b]:=}, {(Subscript[𝒵, a, A, ∘])[b]:=}})]

\(ist–Permutation[f, 
        A] : \(\(⇔\)\(\ \)\(f : \(\(A\(⟶\&\(\(bij\)\(.\)\)\)A\)\(\ \ \ \)\(.\)\)\)\)\)

Definition[\("Permutation", 
      any[A, f], 
ist–Permutation[f, 
          A] :  ⇔ \) ]

Formulierung des Satzes

\(\(∀ \+\(\(∘\)\(\(,\)\(A\)\)\)\)\+\(ist–endliche–Gruppe[\(∘\)\(\(,\)\(A\)\)]\)\(∀ \+\(a ∈ A\)ist–Permutation[𝒵\_\(a, \(\(∘\)\(\(,\)\(A\)\)\)\), A]\) ∧ 
      ist–Permutation[𝒮\_\(a, \(\(∘\)\(\(,\)\(A\)\)\)\), A]\)

Theorem["Verknüpfungstabelle", 
      any[A, ∘], with[], 
 ]

Computer–unterstützter Beweis: nicht erfolgreich

\(Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver]\)

Lemma["Kürzungsregel", 
      any[A, ∘], with[], 
]

\(Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Lemma["Kürzungsregel"], 
          Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver, 
      ProverOptions -> {AllowIntroduceQuantifiers -> 
            True}]\)

Computer–unterstützter Beweis: erfolgreich

Theorem["Verknüpfungstabelle",
]

\(Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver]\)

Lemma["Kürzungsregel",
]

\(Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Lemma["Kürzungsregel"], 
          Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver, SearchDepth -> 40]\)

\(Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Lemma["Kürzungsregel"], 
          Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver, 
      ProverOptions -> {GRWTarget -> {"goal", "kb"}}, 
      SearchDepth -> 40]\)

Lemma["Lösung",
]

Lemma["Abgeschlossenheit",
]

Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Lemma["Lösung"], 
          Lemma["Abgeschlossenheit"], 
          Lemma["Kürzungsregel"], 
          Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver, 
      built–in -> Built–in["Connectives"][And], 
      ProverOptions -> {EarlyRewriting -> True, 
          RWInsideQuantifiers -> True}, 
      SearchDepth -> 40]

Prove[Theorem["Verknüpfungstabelle"], 
      using -> ⟨Lemma["Lösung"], 
          Lemma["Abgeschlossenheit"], 
          Lemma["Kürzungsregel"], 
          Definition["Verknüpfungstabelle, Zeile"], 
          Definition["Permutation"]⟩, 
      by -> SetTheoryPCSProver, 
      built–in -> Built–in["Connectives"][And], 
      ProverOptions -> {RWInsideQuantifiers -> True}, 
      SearchDepth -> 40]

Transform[%, 
      TransformerOptions -> {branches -> Proved, 
          steps -> Useful}]