import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`: lädt nur den
-- benötigten Teil der Bibliothek und beschleunigt den
-- Buch-Build erheblich (ermittelt mit `#min_imports`).
import Mathlib.Algebra.Field.ZMod
import Mathlib.Algebra.Torsor.Defs
import Mathlib.Data.Finite.Vector
import Mathlib.GroupTheory.PGroup
import Mathlib.GroupTheory.Perm.Cycle.Type

open Verso.Genre Manual
open Verso.Genre.Manual.InlineLean

set_option pp.rawOnError true
set_option verso.docstring.allowMissing true

#doc (Manual) "Das Schlüssellemma und der Satz von Cauchy" =>
%%%
htmlSplit := .never
tag := "cauchy"
file := "cauchy"
%%%

Dieses Kapitel übersetzt den Anfang von Kapitel 18 des Skripts: das
_zentrale Schlüssellemma_ über Fixpunkte von p-Gruppen-Wirkungen und
seine erste Anwendung, den Satz von Cauchy.  Unterwegs werden wir zum
ersten Mal selbst etwas in Lean _definieren_: eine Gruppenwirkung.

# Das zentrale Schlüssellemma

> *Lemma 18.1.1 (Zentrales Schlüssellemma).* Es sei
  $`m \in \mathbb{N}` und es sei $`p` eine Primzahl.  Weiter sei $`G`
  eine Gruppe der Ordnung $`p^m`, die auf einer endlichen Menge $`M`
  operiert.  Weiter sei
  $`M_0 = \{ m \in M : g \cdot m = m \ \forall g \in G \}` die Menge
  der Fixpunkte.  Dann ist $`|M| \equiv |M_0| \pmod{p}`.

Wie sagt Mathlib das alles?

* „eine Gruppe der Ordnung $`p^m`“: Dafür hat Mathlib ein Prädikat
  `IsPGroup p G` („die Ordnung jedes Elements ist eine
  $`p`-Potenz“; für endliche Gruppen ist das nach dem Satz von
  Cauchy unten äquivalent).  Das Lemma `IsPGroup.of_card` übersetzt
  unsere Voraussetzung `Nat.card G = p ^ m` dorthin.

* „die auf einer endlichen Menge $`M` operiert“: Eine Wirkung von
  $`G` auf $`M` ist eine Typklasse, `[MulAction G M]`; die
  Endlichkeit von $`M` ist die Typklasse `[Finite M]`.

* Die Fixpunktmenge heißt `MulAction.fixedPoints G M`, und die
  Kongruenz $`|M| \equiv |M_0| \pmod{p}` schreibt sich
  `Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p]`.

Der Beweis im Skript zerlegt $`M` in Bahnen und zitiert die
Bahnengleichung.  Genau so beweist Mathlib die Aussage
`IsPGroup.card_modEq_card_fixedPoints`.  Wir zitieren hier also
einfach die Bibliothek, so wie das Skript an dieser Stelle Satz 17.2.1
zitiert.

```lean
open Equiv.Perm Equiv.Perm.VectorsProdEqOne
open MulAction Multiplicative

theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*}
    [Group G] (hG : Nat.card G = p ^ m) (M : Type*)
    [Finite M] [MulAction G M] :
    Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p] := by
  have : Fact p.Prime := ⟨hp⟩
  exact (IsPGroup.of_card hG).card_modEq_card_fixedPoints M
```

(Die `open`-Zeilen holen die Namensräume, die wir in diesem Kapitel
brauchen, in den Geltungsbereich; `Equiv.Perm.vectorsProdEqOne` tritt
gleich auf.)

# Der Satz von Cauchy

> *Satz 18.1.2 (Satz von Cauchy).* Wenn die Ordnung einer endlichen
  Gruppe durch $`p` teilbar ist, dann existiert ein Element von
  Ordnung $`p`.

Wir folgen dem Beweis des Skripts Satz für Satz.  Der Beweis
konstruiert eine raffinierte Hilfsmenge mit einer raffinierten
Gruppenwirkung.  Diesmal gibt es also vor dem eigentlichen Satz echte
Arbeit: Wir bauen erst die Menge und die Wirkung.

## Die Menge M

„Betrachte die Menge
$`M = \bigl\{ (a_1, \dots, a_p) \in G \times \dots \times G : a_1 \cdot a_2 \cdots a_p = e \bigr\}`.“

Mathlib kennt diese Menge.  Ein $`p`-Tupel von Gruppenelementen ist
ein `List.Vector G p`, also eine Liste der Länge $`p`.  Und $`M` ist
die Menge `Equiv.Perm.vectorsProdEqOne G p` aller Vektoren, deren
Einträge sich zu 1 multiplizieren.

„Gegeben ein Tupel $`(a_1, \dots, a_p) \in M`, dann stellen wir erst
einmal fest, dass der letzte Eintrag des Tupels durch die ersten
Einträge eindeutig bestimmt ist,
$`a_p = (a_1 \cdots a_{p-1})^{-1}`.  Wir erhalten die folgende
Gleichung: $`|M| = |G^{p-1}| = |G|^{p-1}`.“

Auch das steht schon in Mathlib: Die Bijektion
$`(a_1, \dots, a_{p-1}) \mapsto (a_1, \dots, a_{p-1}, (a_1 \cdots a_{p-1})^{-1})`
heißt `VectorsProdEqOne.vectorEquiv`, und die resultierende
Zählformel ist `VectorsProdEqOne.card`:

```
VectorsProdEqOne.card (G : Type) [Group G] (n : ℕ) [Fintype G] :
    Fintype.card ↑(vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)
```

## Die Wirkung von ℤ/(p)

„Als Nächstes brauchen wir eine schicke Gruppenwirkung, denn wir
wollen das zentrale Schlüssellemma anwenden.  Dazu lassen wir die
zyklische Gruppe $`\mathbb{Z}/(p)` auf $`M` durch zyklisches
Vertauschen wirken.“

Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p` um
$`k` Stellen ist `VectorsProdEqOne.rotate v k`.  Die Fußnote des
Skripts begründet, dass der Shift $`M` auf sich abbildet, „weil in
jeder Gruppe aus $`a \cdot b = e` auch $`b \cdot a = e` gilt“.  In
Mathlib ist das das Lemma
`List.prod_rotate_eq_one_of_prod_eq_one`, das schon in der Definition
von `rotate` steckt.

Damit $`\mathbb{Z}/(p)` _als Gruppe_ wirkt, müssen wir die
Wirkungsaxiome nachprüfen: Der Shift um 0 tut nichts, und der Shift
um $`j + k` ist der Shift um $`k` gefolgt vom Shift um $`j`.  Mathlib
stellt `rotate_zero`, `rotate_rotate` und `rotate_length` bereit (der
Shift um die volle Länge $`p` tut nichts); daraus leiten wir zuerst
ab, dass der Shift nur von der Verschiebung _modulo p_ abhängt.
Genau deshalb wirkt $`\mathbb{Z}/(p)` und nicht bloß
$`\mathbb{N}`.

```lean
theorem rotate_mul {G : Type*} [Group G] {p : ℕ}
    (v : vectorsProdEqOne G p) (q : ℕ) :
    rotate v (p * q) = v := by
  induction q with
  | zero => rw [Nat.mul_zero, rotate_zero]
  | succ q ih =>
      rw [Nat.mul_succ, ← rotate_rotate, ih, rotate_length]

theorem rotate_mod {G : Type*} [Group G] {p : ℕ}
    (v : vectorsProdEqOne G p) (k : ℕ) :
    rotate v (k % p) = rotate v k := by
  calc rotate v (k % p)
      = rotate (rotate v (k % p)) (p * (k / p)) :=
        (rotate_mul _ _).symm
    _ = rotate v (k % p + p * (k / p)) :=
        rotate_rotate _ _ _
    _ = rotate v k := by rw [Nat.mod_add_div]
```

Nun können wir die Wirkung definieren.  Zwei technische Anmerkungen.
Mathlibs `MulAction` erwartet eine multiplikativ geschriebene Gruppe;
$`\mathbb{Z}/(p)` = `ZMod p` ist aber additiv geschrieben.  Der Wrapper
`Multiplicative` wechselt die Notation (dank
`open Multiplicative` oben schreiben sich seine Übergänge kurz
`toAdd` und `ofAdd`).  Die Voraussetzung `[NeZero p]` schließt
`p = 0` aus, wo „Shift um eine Restklasse“ sinnlos wäre.

```lean
instance rotateAction {G : Type*} [Group G] {p : ℕ}
    [NeZero p] :
    MulAction (Multiplicative (ZMod p))
      (vectorsProdEqOne G p) where
  smul k v := rotate v (toAdd k).val
  one_smul v := by
    show rotate v (ZMod.val 0) = v
    rw [ZMod.val_zero, rotate_zero]
  mul_smul j k v := by
    show rotate v ((toAdd j + toAdd k).val) =
      rotate (rotate v (toAdd k).val) (toAdd j).val
    rw [ZMod.val_add, rotate_mod, rotate_rotate,
      Nat.add_comm]
```

## Die Fixpunkte

„Die Fixpunktmenge dieser Wirkung ist
$`M_0 = \{ (a, \dots, a) \in G^p : a^p = e \}`.“

Mit anderen Worten: Ein Tupel ist genau dann ein Fixpunkt, wenn es
konstant ist, seine Liste also für ein $`a` die Liste
`List.replicate p a` = $`(a, \dots, a)` ist.  (Die
Bedingung $`a^p = e` gilt dann automatisch, weil sich die Einträge
eines Tupels in $`M` zu $`e` multiplizieren.)  Der Schlüsselschritt ist das Lemma
`List.rotate_one_eq_self_iff_eq_replicate`: Eine Liste, die der
zyklische Shift um _eine_ Stelle nicht ändert, ist konstant.

```lean
theorem mem_fixedPoints_iff_replicate {G : Type*} [Group G]
    {p : ℕ} [Fact (1 < p)] (v : vectorsProdEqOne G p) :
    v ∈ fixedPoints (Multiplicative (ZMod p))
        (vectorsProdEqOne G p) ↔
      ∃ a : G,
        (v : List.Vector G p).toList
          = List.replicate p a := by
  rw [mem_fixedPoints]
  constructor
  · -- Ein Fixpunkt wird insbesondere von 1 ∈ ℤ/(p) fixiert,
    -- bleibt also unter dem Shift um eine Stelle
    -- unverändert …
    intro hv
    have h1 : rotate v 1 = v := by
      have h := hv (ofAdd (1 : ZMod p))
      rwa [show ofAdd (1 : ZMod p) • v
            = rotate v (1 : ZMod p).val from rfl,
          ZMod.val_one] at h
    -- … und ist daher konstant.
    obtain ⟨a, ha⟩ :=
      List.rotate_one_eq_self_iff_eq_replicate.mp
        (Subtype.ext_iff.mp (Subtype.ext_iff.mp h1))
    refine ⟨a, ha.trans ?_⟩
    congr 1
    exact (v : List.Vector G p).2
  · -- Umgekehrt ändert kein zyklischer Shift ein konstantes
    -- Tupel.
    rintro ⟨a, ha⟩ g
    apply Subtype.ext
    apply Subtype.ext
    show (v : List.Vector G p).toList.rotate (toAdd g).val =
      (v : List.Vector G p).toList
    rw [ha, List.rotate_replicate]
```

## Der Beweis

Jetzt setzen wir die Teile zusammen und folgen dem Skript Zeile für
Zeile.

```lean
theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ}
    (hp : p.Prime) (hdvd : p ∣ Fintype.card G) :
    ∃ a : G, orderOf a = p := by
  -- Die Konsequenzen der Primalität, die die Instanzsuche
  -- braucht:
  have : Fact p.Prime := ⟨hp⟩
  have : NeZero p := ⟨hp.ne_zero⟩
  have : Fact (1 < p) := ⟨hp.one_lt⟩
  -- Abkürzung: M₀ ist die Fixpunktmenge der Wirkung.
  set M₀ := fixedPoints (Multiplicative (ZMod p))
    (vectorsProdEqOne G p)
  -- „Wir erhalten die folgende Gleichung:
  --  |M| = |G^{p-1}| = |G|^{p-1}.“
  have hM : Nat.card (vectorsProdEqOne G p)
      = Fintype.card G ^ (p - 1) := by
    rw [Nat.card_eq_fintype_card, VectorsProdEqOne.card]
  -- Die zyklische Gruppe ℤ/(p) hat Ordnung p = p¹; das
  -- Schlüssellemma, angewandt auf die Rotationswirkung,
  -- liefert |M| ≡ |M₀| (mod p):
  have hZp :
      Nat.card (Multiplicative (ZMod p)) = p ^ 1 := by
    simp [Nat.card_eq_fintype_card]
  have hcong :
      Nat.card (vectorsProdEqOne G p) ≡
        Nat.card M₀ [MOD p] :=
    key_lemma hp hZp (vectorsProdEqOne G p)
  -- „Auf der anderen Seite folgt aus dem zentralen
  --  Schlüssellemma, dass
  --  |M₀| ≡ |M| ≡ |G|^{p-1} ≡ 0 (mod p) ist.“
  have hdvdM0 : p ∣ Nat.card M₀ := by
    have hp1 : p - 1 ≠ 0 := by have := hp.one_lt; omega
    have h0 : (0 : ℕ) ≡ Nat.card M₀ [MOD p] :=
      calc (0 : ℕ)
          ≡ Fintype.card G ^ (p - 1) [MOD p] :=
            (Nat.modEq_zero_iff_dvd.mpr
              (dvd_pow hdvd hp1)).symm
        _ = Nat.card (vectorsProdEqOne G p) := hM.symm
        _ ≡ Nat.card M₀ [MOD p] := hcong
    exact Nat.modEq_zero_iff_dvd.mp h0.symm
  -- „Wegen (e, …, e) ∈ M₀ ist schon einmal klar, dass
  --  M₀ ≠ ∅ ist.“
  let v₀ : vectorsProdEqOne G p :=
    ⟨List.Vector.replicate p 1,
      (List.prod_replicate p 1).trans (one_pow p)⟩
  have hv₀ : v₀ ∈ M₀ :=
    (mem_fixedPoints_iff_replicate v₀).mpr ⟨1, rfl⟩
  -- M₀ ist nichtleer, und |M₀| ist durch p ≥ 2 teilbar,
  -- also ist |M₀| ≥ p > 1 …
  have := Fintype.ofFinite M₀
  have hlt : 1 < Fintype.card M₀ := by
    rw [← Nat.card_eq_fintype_card]
    have hpos : 0 < Nat.card M₀ :=
      Nat.card_pos_iff.mpr ⟨⟨⟨v₀, hv₀⟩⟩, inferInstance⟩
    have := Nat.le_of_dvd hpos hdvdM0
    have := hp.one_lt
    omega
  -- „Also existiert mindestens ein a ≠ e mit a^p = e.“
  obtain ⟨w, hw⟩ :=
    Fintype.exists_ne_of_one_lt_card hlt ⟨v₀, hv₀⟩
  obtain ⟨a, ha⟩ :=
    (mem_fixedPoints_iff_replicate w.1).mp w.2
  -- Das Tupel w liegt in M, sein Produkt ist also e; weil
  -- das Tupel konstant ist, heißt das genau a^p = e:
  have hpow : a ^ p = 1 := by
    have hprod : (w.1 : List.Vector G p).toList.prod = 1 :=
      w.1.2
    rwa [ha, List.prod_replicate] at hprod
  -- Und a ≠ e, denn sonst wäre w das Tupel (e, …, e) = v₀:
  have hne : a ≠ 1 := by
    rintro rfl
    exact hw (Subtype.ext (Subtype.ext (Subtype.ext ha)))
  -- „Nach Satz 17.4.6 hat a dann automatisch die
  --  Ordnung p.“
  exact ⟨a, orderOf_eq_prime hpow hne⟩
```

# Bemerkungen

Mathlibs Fassung des Satzes von Cauchy heißt
`exists_prime_orderOf_dvd_card`; ihr Beweis ist dasselbe Zählargument,
nur etwas anders organisiert.

# Übungsaufgabe

Das ist Satz 18.2.3 im Skript: _Es sei $`p` eine Primzahl und $`G`
eine nichttriviale Gruppe, deren Ordnung eine $`p`-Potenz ist.  Dann
ist das Zentrum von $`G` nicht trivial._  Beweisen Sie das in Lean:
Wenden Sie `key_lemma` auf die Konjugationswirkung von $`G` auf sich
selbst an,
oder finden Sie die Aussage in Mathlib.  Öffnen Sie
`AlgebraInLean/Cauchy.lean` im Übungs-Repository und ersetzen Sie das
`sorry` durch einen Beweis.

```lean
theorem center_nontrivial {p m : ℕ} (hp : p.Prime)
    {G : Type*} [Group G] [Finite G] (hm : m ≠ 0)
    (hG : Nat.card G = p ^ m) :
    Nontrivial (Subgroup.center G) := by
  sorry
```