import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
-- `#min_imports`, ergänzt um die Taktik `ring`.
import Mathlib.Algebra.Field.ZMod
import Mathlib.Data.Nat.Choose.Dvd
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Tactic.Ring

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

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

#doc (Manual) "Endliche Körper und der Frobenius" =>
%%%
htmlSplit := .never
tag := "frobenius"
file := "frobenius"
%%%

Dieses Kapitel übersetzt den Satz über den Frobenius-Endomorphismus
aus Kapitel 14 des Skripts Satz für Satz nach Lean.  Es geht um den
„Traum jedes Studienanfängers“: $`(a+b)^p = a^p + b^p`.

# Das Mathlib-Wörterbuch

* „$`R` hat Charakteristik $`p`“ ist die Typklasse `CharP R p`.
  Das entscheidende Lemma ist `CharP.cast_eq_zero`: Das Bild von
  $`p` in $`R` ist Null.

* Binomialkoeffizienten heißen `Nat.choose`; die binomische Formel
  ist `add_pow`, eine Summe über `Finset.range`.  Endliche Summen und
  ihre Umformungen sind das Lean-Lernthema dieses Kapitels.

# Der Frobenius-Endomorphismus

Satz und Definition 14.2.2 des Skripts:

> *Satz und Definition 14.2.2 (Frobenius-Endomorphismus).* Es sei
  $`p` eine Primzahl und es sei $`R` ein kommutativer Ring mit Eins
  der Charakteristik $`p`.  Dann ist die Abbildung
  $`F : R \to R`, $`a \mapsto a^p` ein Ringmorphismus.

> _Beweis._ Die Verträglichkeit mit der Multiplikation ist klar,
  weil $`R` kommutativ ist: $`(a \cdot b)^p = a^p \cdot b^p`.
  Ebenso ist $`F(1) = 1`.  Interessant ist nur die Verträglichkeit
  mit der Addition.  …  Die binomische Formel gilt in jedem
  kommutativen Ring, also ist
  $`(a+b)^p = \sum_{k=0}^{p} \binom{p}{k} \cdot a^k \cdot b^{p-k}`.
  Für alle Indizes $`0 < k < p` ist der Binomialkoeffizient
  $`\binom{p}{k}` ein Vielfaches von $`p` ….  Weil $`R` die
  Charakteristik $`p` hat, ist $`p = 0` in $`R`, und alle diese
  Summanden verschwinden.  Übrig bleiben nur die Summanden für
  $`k = 0` und $`k = p`.

```lean
theorem frobenius_mul {R : Type*} [CommRing R] (p : ℕ)
    (a b : R) : (a * b) ^ p = a ^ p * b ^ p :=
  mul_pow a b p

theorem frobenius_add {R : Type*} [CommRing R] (p : ℕ)
    [Fact p.Prime] [CharP R p] (a b : R) :
    (a + b) ^ p = a ^ p + b ^ p := by
  have hp : p.Prime := Fact.out
  -- „Die binomische Formel gilt in jedem kommutativen
  --  Ring, also ist
  --  (a+b)^p = ∑ₖ (p über k)·a^k·b^{p−k}.“
  rw [add_pow]
  -- „Für alle Indizes 0 < k < p ist der
  --  Binomialkoeffizient (p über k) ein Vielfaches von p
  --  ….  Weil R die Charakteristik p hat, ist p = 0 in
  --  R, und alle diese Summanden verschwinden.“
  have hmid : ∀ k ∈ Finset.Ioo 0 p,
      a ^ k * b ^ (p - k) * (p.choose k : R) = 0 := by
    intro k hk
    obtain ⟨hk0, hkp⟩ := Finset.mem_Ioo.mp hk
    obtain ⟨c, hc⟩ :=
      hp.dvd_choose_self (by omega) hkp
    rw [hc]
    push_cast
    rw [CharP.cast_eq_zero R p]
    ring
  -- „Übrig bleiben nur die Summanden für k = 0 und k = p.“
  have hsplit : Finset.range (p + 1)
      = {0, p} ∪ Finset.Ioo 0 p := by
    ext k
    simp only [Finset.mem_range, Finset.mem_union,
      Finset.mem_insert, Finset.mem_singleton,
      Finset.mem_Ioo]
    omega
  have hdisj : Disjoint ({0, p} : Finset ℕ)
      (Finset.Ioo 0 p) := by
    rw [Finset.disjoint_left]
    intro k hk hk'
    simp only [Finset.mem_insert,
      Finset.mem_singleton] at hk
    simp only [Finset.mem_Ioo] at hk'
    omega
  rw [hsplit, Finset.sum_union hdisj,
    Finset.sum_pair (Ne.symm hp.ne_zero),
    Finset.sum_eq_zero hmid, add_zero]
  -- „(a+b)^p = (p über 0)·a⁰·b^p + (p über p)·a^p·b⁰
  --          = a^p + b^p.“
  simp [Nat.choose_zero_right, Nat.choose_self, add_comm]
```

# Bemerkungen

Mathlib bündelt die drei Verträglichkeiten zum Ringmorphismus
`frobenius R p : R →+* R`; die Additivität heißt dort
`add_pow_char`.  Das Skript beobachtet, dass der Frobenius über einem
Integritätsring injektiv und über einem endlichen Körper sogar
bijektiv ist.  Das führt zur Klassifikation endlicher Körper:
Zu jeder Primzahlpotenz $`p^n` gibt es genau einen Körper mit
$`p^n` Elementen.  In Mathlib heißt er `GaloisField p n`.

# Übungsaufgabe

Der Frobenius des Körpers $`\mathbb{F}_p` ist die Identität: Für
jedes $`a \in \mathbb{F}_p` ist $`a^p = a`.  Das ist ein alter
Bekannter: der kleine
Satz von Fermat aus unserem dritten Kapitel!  In Mathlib heißt er
`ZMod.pow_card`.  Öffnen Sie `AlgebraInLean/Frobenius.lean` und
ersetzen Sie das `sorry` durch einen Beweis.

```lean
theorem frobenius_zmod (p : ℕ) [Fact p.Prime]
    (a : ZMod p) : a ^ p = a := by
  sorry
```