Working…

AlgebraInLean.lean

@@ -3,5 +3,9 @@ import AlgebraInLean.Basics
 import AlgebraInLean.Quotients
 import AlgebraInLean.Ideals
 import AlgebraInLean.Polynomials
+import AlgebraInLean.Degrees
 import AlgebraInLean.LittleFermat
 import AlgebraInLean.Cauchy
+import AlgebraInLean.Frobenius
+import AlgebraInLean.Galois
+import AlgebraInLean.Reciprocity

AlgebraInLean/Cauchy.lean

@@ -23,7 +23,7 @@ open Multiplicative
 
 ## Das zentrale Schlüssellemma
 
-**Lemma (Zentrales Schlüssellemma).**  *Es sei m ∈ ℕ und es
+**Lemma 18.1.1 (Zentrales Schlüssellemma).**  *Es sei m ∈ ℕ 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₀ = { m ∈ M : ∀ g ∈ G: g·m = m } die Menge der Fixpunkte.
@@ -50,7 +50,7 @@ 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.6 zitiert.
+Stelle Satz 17.2.1 zitiert.
 -/
 
 theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*}
@@ -63,7 +63,7 @@ theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*}
 /-!
 ## Der Satz von Cauchy
 
-**Satz (Satz von Cauchy).**  *Wenn die Ordnung einer endlichen
+**Satz 18.1.2 (Satz von Cauchy).**  *Wenn die Ordnung einer endlichen
 Gruppe durch p teilbar ist, dann existiert ein Element von
 Ordnung p.*
 
@@ -282,7 +282,7 @@ theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ}
   have hne : a ≠ 1 := by
     rintro rfl
     exact hw (Subtype.ext (Subtype.ext (Subtype.ext ha)))
-  -- „Nach Satz 17.4.11 hat a dann automatisch die
+  -- „Nach Satz 17.4.6 hat a dann automatisch die
   --  Ordnung p.“
   exact ⟨a, orderOf_eq_prime hpow hne⟩
 

AlgebraInLean/Degrees.lean

@@ -0,0 +1,117 @@
+/-
+Algebra in Lean — Kapitel 3 des Skripts
+=======================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie übersetzt die Gradformel
+(satz:3-6-1) nach Lean — unsere erste Begegnung mit linearer
+Algebra: Basen, Dimensionen und Körpererweiterungen als
+Vektorräume.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+/-!
+# Körpererweiterungen und die Gradformel
+
+## Das Mathlib-Wörterbuch
+
+* Eine Körpererweiterung L/K ist in Mathlib eine
+  `Algebra K L`-Instanz zwischen zwei Körpern — L wird damit
+  insbesondere ein K-Vektorraum, genau wie im Skript.
+
+* Eine Kette K ⊆ L ⊆ M besteht aus drei Algebra-Instanzen
+  und der Verträglichkeitsbedingung `IsScalarTower K L M`
+  („erst nach L, dann nach M einbetten ist dasselbe wie
+  direkt nach M“).
+
+* Der Grad [L:K] heißt `Module.finrank K L`.  Achtung, hier
+  weicht die Konvention vom Skript ab: `finrank` hat Werte
+  in ℕ, und unendlichdimensionale Erweiterungen bekommen
+  den Wert 0 — wo das Skript in seiner Fußnote mit ∞
+  rechnet, rechnet Mathlib mit 0.  „[L:K] ist endlich“ ist
+  die Typklasse `FiniteDimensional K L`.
+
+## Die Gradformel
+
+Satz 3.6.1 des Skripts, mit Beweis:
+
+„Es sei K ⊆ L ⊆ M eine Kette von Körpererweiterungen.  Dann
+gilt die Gleichung [M:K] = [M:L]·[L:K].“
+
+„Wir kümmern uns zuerst um die unendlichen Fälle …“ — diese
+Fälle entfallen in unserer Fassung, weil wir Endlichkeit
+voraussetzen; in Mathlibs 0-Konvention gilt die Formel
+sogar uneingeschränkt (`Module.finrank_mul_finrank`).
+
+„Es seien jetzt also a := [L:K] und b := [M:L] beide
+endlich.  Wähle Basen ℓ₁, …, ℓ_a von L als K-Vektorraum und
+m₁, …, m_b von M als L-Vektorraum.  Ich behaupte, dass die
+a·b Produkte (ℓᵢ·mⱼ) eine Basis von M als K-Vektorraum
+bilden; damit ist dann sofort [M:K] = a·b gezeigt.“
+
+Die Behauptung — mit den beiden Beweisschritten
+„Die Produkte bilden ein Erzeugendensystem“ und „Die
+Produkte sind linear unabhängig“ — ist in Mathlib die
+Konstruktion `Basis.smulTower`: Aus einer Basis ℓ von L/K
+und einer Basis m von M/L baut sie die Basis (ℓᵢ • mⱼ) von
+M/K (das Lemma `Basis.smulTower_apply` bestätigt, dass die
+Basiselemente wirklich die Produkte sind).  Der Rest ist
+Abzählen der Indexmenge.
+-/
+
+theorem gradformel (K L M : Type*) [Field K] [Field L]
+    [Field M] [Algebra K L] [Algebra L M] [Algebra K M]
+    [IsScalarTower K L M]
+    [FiniteDimensional K L] [FiniteDimensional L M] :
+    Module.finrank K M
+      = Module.finrank L M * Module.finrank K L := by
+  -- „Wähle Basen ℓ₁, …, ℓ_a von L als K-Vektorraum und
+  --  m₁, …, m_b von M als L-Vektorraum.“
+  let ℓ := Module.finBasis K L
+  let m := Module.finBasis L M
+  -- „Ich behaupte, dass die a·b Produkte (ℓᵢ·mⱼ) eine
+  --  Basis von M als K-Vektorraum bilden …“
+  let basis := ℓ.smulTower m
+  -- „… damit ist dann sofort [M:K] = a·b gezeigt.“
+  rw [Module.finrank_eq_card_basis basis, Fintype.card_prod,
+    Fintype.card_fin, Fintype.card_fin, mul_comm]
+
+/-!
+## Bemerkungen
+
+1. Die beiden Beweisschritte des Skripts stecken im Beweis
+   von `Basis.smulTower`: Das „Einsetzen“ im
+   Erzeugendensystem-Schritt und das „Umsortieren“ im
+   Unabhängigkeits-Schritt werden dort durch die
+   Komposition der Koordinatenabbildungen erledigt —
+   `smulTower_repr` sagt, dass die (i,j)-Koordinate von x
+   gerade die i-te Koordinate der j-ten Koordinate ist:
+   exakt das μᵢⱼ aus dem Skript.
+
+2. Ohne Endlichkeitsvoraussetzungen heißt die Formel in
+   Mathlib `Module.finrank_mul_finrank`; die unendlichen
+   Fälle des Skripts verschwinden dort in der
+   0-Konvention.
+
+## Übungsaufgabe
+
+Das erste Korollar des Skripts zur Gradformel: „Es sei
+K ⊆ L ⊆ M eine Kette von Körpererweiterungen.  Wenn [M:K]
+endlich ist, dann ist [L:K] endlich, und sogar ein Teiler
+von [M:K].“  Der erste Teil ist `Module.Finite.left` (und
+`Module.Finite.right` liefert die Endlichkeit von [M:L]) —
+beide müssen mit `have := …` in den Kontext geholt werden,
+damit die Instanzsuche sie sieht.  Der Teiler-Teil ist die
+Übung: Ersetzen Sie das `sorry` durch einen Beweis mit
+`gradformel`.
+-/
+
+theorem grad_teilt (K L M : Type*) [Field K] [Field L]
+    [Field M] [Algebra K L] [Algebra L M] [Algebra K M]
+    [IsScalarTower K L M] [FiniteDimensional K M] :
+    Module.finrank K L ∣ Module.finrank K M := by
+  sorry
+
+end AlgebraInLean

AlgebraInLean/Frobenius.lean

@@ -0,0 +1,124 @@
+/-
+Algebra in Lean — Kapitel 14 des Skripts
+========================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie übersetzt den Satz über
+den Frobenius-Endomorphismus
+(DefSatz_Frobenius-Endomorphismus) Satz für Satz nach Lean —
+den „Traum jedes Studienanfängers“: (a+b)^p = a^p + b^p.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+/-!
+# Endliche Körper und der Frobenius
+
+## 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 → R,
+a ↦ a^p ein Ringmorphismus.*
+
+„Die Verträglichkeit mit der Multiplikation ist klar, weil
+R kommutativ ist: (a·b)^p = a^p·b^p.  Ebenso ist F(1) = 1.“
+-/
+
+theorem frobenius_mul {R : Type*} [CommRing R] (p : ℕ)
+    (a b : R) : (a * b) ^ p = a ^ p * b ^ p :=
+  mul_pow a b p
+
+/-!
+„Interessant ist nur die Verträglichkeit mit der Addition.“
+Wir übersetzen den Beweis aus Erklärvideo 14-1 Satz für
+Satz.
+-/
+
+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
+
+1. Mathlib bündelt die drei Verträglichkeiten zum
+   Ringmorphismus `frobenius R p : R →+* R`; die
+   Additivität heißt dort `add_pow_char`.
+
+2. Die Beobachtung des Skripts — über einem Integritätsring
+   ist der Frobenius injektiv, über einem endlichen Körper
+   sogar bijektiv — 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 𝔽_p ist die Identität: Für jedes
+a ∈ 𝔽_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`.  Ersetzen Sie das `sorry`
+durch einen Beweis.
+-/
+
+theorem frobenius_zmod (p : ℕ) [Fact p.Prime]
+    (a : ZMod p) : a ^ p = a := by
+  sorry
+
+end AlgebraInLean

AlgebraInLean/Galois.lean

@@ -0,0 +1,115 @@
+/-
+Algebra in Lean — Kapitel 15 und 16 des Skripts
+===============================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie zeigt, wie Mathlib die
+Begriffe der Galoistheorie darstellt, übersetzt die
+Fixkörper-Konstruktion (DefSatz_Fixkoerper) — und die
+„Hausaufgabe“ des Skripts wird auch hier zur Übungsaufgabe.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+/-!
+# Galois-Theorie
+
+## Das Mathlib-Wörterbuch
+
+* Die Galoisgruppe einer Körpererweiterung L/K ist der Typ
+  `L ≃ₐ[K] L` der K-Algebren-Automorphismen; Mathlib stellt
+  dafür sogar die Notation `Gal(L/K)` bereit.
+
+* „L/K ist galoissch“ ist die Typklasse `IsGalois K L` —
+  definiert als „separabel und normal“, genau wie im
+  Skript.
+
+* Ein Zwischenkörper ist ein Term `Z : IntermediateField K L`;
+  der Fixkörper einer Untergruppe `H : Subgroup Gal(L/K)`
+  heißt `IntermediateField.fixedField H`.
+
+## Der Fixkörper
+
+Satz und Definition 16.1.1 des Skripts:
+
+**Satz und Definition 16.1.1 (Invariante Elemente, Fixkörper).**
+*Sei L ein Körper und G eine Menge von Automorphismen
+L → L.  Dann ist die Menge
+Fix G = { a ∈ L : σ(a) = a für alle σ ∈ G } ein Unterkörper
+von L.  Der Beweis des folgenden Satzes ist eine
+Hausaufgabe.*
+
+Wir definieren die Menge in Lean und beweisen exemplarisch
+die Abgeschlossenheit unter der Multiplikation — der Rest
+der Hausaufgabe ist, wie im Skript, Ihre Übungsaufgabe.
+-/
+
+def Fix {L : Type*} [Field L] (G : Set (L ≃+* L)) :
+    Set L :=
+  {a | ∀ σ ∈ G, σ a = a}
+
+theorem mul_mem_fix {L : Type*} [Field L]
+    {G : Set (L ≃+* L)} {a b : L}
+    (ha : a ∈ Fix G) (hb : b ∈ Fix G) :
+    a * b ∈ Fix G := by
+  -- Automorphismen respektieren die Multiplikation:
+  intro σ hσ
+  rw [map_mul, ha σ hσ, hb σ hσ]
+
+/-!
+## Der Satz von Artin und der Hauptsatz
+
+Auch die großen Sätze dieses Teils der Vorlesung stehen in
+Mathlib; wir zitieren sie mit ihren Namen.
+
+**Satz von Emil Artin (Satz 16.1.2).**  *Es sei G eine endliche
+Untergruppe der Automorphismengruppe eines Körpers L und es
+sei K := Fix G.  Dann ist L/K eine Galoiserweiterung mit
+Galoisgruppe Gal(L/K) = G.  Insbesondere ist [L:K] = |G|.*
+— Die Gradaussage ist `FixedPoints.finrank_eq_card`; das
+gebündelte Fixkörper-Objekt heißt dort
+`FixedPoints.subfield G L`.
+
+**Hauptsatz der Galoistheorie (Satz 16.3.2).**  *Es sei L/K eine
+Galoiserweiterung mit Galoisgruppe G.  Dann sind die
+Abbildungen Z ↦ Gal(L/Z) und H ↦ Fix H zueinander inverse,
+inklusionsumkehrende Bijektionen zwischen Zwischenkörpern
+und Untergruppen […].*  — In Mathlib ist das der
+ordnungsumkehrende Isomorphismus
+`IsGalois.intermediateFieldEquivSubgroup`; das „ᵒᵈ“
+(order dual) im Typ ist genau das „inklusionsumkehrend“ des
+Skripts.
+
+Die Gradaussage |Gal(L/K)| = [L:K] für Galoiserweiterungen
+heißt `IsGalois.card_aut_eq_finrank`:
+-/
+
+example (K L : Type*) [Field K] [Field L] [Algebra K L]
+    [FiniteDimensional K L] [IsGalois K L] :
+    Nat.card (L ≃ₐ[K] L) = Module.finrank K L :=
+  IsGalois.card_aut_eq_finrank K L
+
+/-!
+## Übungsaufgabe
+
+Die „Hausaufgabe“ des Skripts: Vervollständigen Sie den
+Nachweis, dass Fix G ein Unterkörper ist — Abgeschlossenheit
+unter Addition und unter Inversen.  Für die Addition ist
+`map_add` das Gegenstück zu `map_mul`; für das Inverse
+respektieren Körperautomorphismen auch die Division:
+`map_inv₀`.  Ersetzen Sie die beiden `sorry` durch Beweise.
+-/
+
+theorem add_mem_fix {L : Type*} [Field L]
+    {G : Set (L ≃+* L)} {a b : L}
+    (ha : a ∈ Fix G) (hb : b ∈ Fix G) :
+    a + b ∈ Fix G := by
+  sorry
+
+theorem inv_mem_fix {L : Type*} [Field L]
+    {G : Set (L ≃+* L)} {a : L} (ha : a ∈ Fix G) :
+    a⁻¹ ∈ Fix G := by
+  sorry
+
+end AlgebraInLean

AlgebraInLean/LittleFermat.lean

@@ -18,7 +18,7 @@ namespace AlgebraInLean
 /-!
 # Der kleine Satz von Fermat
 
-**Satz (Kleiner Satz von Fermat).**  *Es sei p ∈ ℕ eine
+**Satz 17.5.1 (Kleiner Satz von Fermat).**  *Es sei p ∈ ℕ eine
 Primzahl und es sei a ∈ ℤ irgendeine Zahl.  Dann ist
 a^p ≡ a (mod p).*
 
@@ -69,7 +69,7 @@ theorem little_fermat (p : ℕ) (hp : p.Prime) (a : ℤ) :
     -- „… welche p−1 Elemente hat.“
     have card_units : Nat.card (ZMod p)ˣ = p - 1 := by
       rw [Nat.card_eq_fintype_card, ZMod.card_units p]
-    -- „Nach Satz 17.3.6 («Satz von Lagrange») ist die
+    -- „Nach Satz 17.2.4 («Satz von Lagrange») ist die
     --  Ordnung von ā, also die Größe der von ā erzeugten
     --  Untergruppe, ein Teiler von |𝔽_p^*| = p−1.“
     have lagrange :

AlgebraInLean/Polynomials.lean

@@ -36,9 +36,9 @@ open Polynomial
 
 ## Das Eisenstein-Kriterium
 
-Der Satz aus Kapitel 7 des Skripts:
+Satz 7.2.1 des Skripts:
 
-**Satz (Eisenstein-Kriterium).**  *Es sei R ein faktorieller
+**Satz 7.2.1 (Eisenstein-Kriterium).**  *Es sei R ein faktorieller
 Ring und es sei f = a₀ + a₁·x + … + aₙ·xⁿ ∈ R[x] ein Polynom
 vom Grad n > 0.  Weiter sei ggT(a₀, …, aₙ) = 1.  Wenn es ein
 Primelement p ∈ R gibt mit p|a₀, p|a₁, …, p|a_{n−1} und

AlgebraInLean/Quotients.lean

@@ -87,7 +87,7 @@ example {G H : Type*} [Group G] [Group H] (N : Subgroup G)
 /-!
 ## Die Beobachtung: U·N ist eine Untergruppe
 
-Beobachtung aus Kapitel 17.3 des Skripts: „Es sei G eine
+Beobachtung 17.3.5 des Skripts: „Es sei G eine
 Gruppe und es sei N ⊂ G eine normale Untergruppe.  Weiter
 sei U ⊂ G irgendeine Untergruppe.  Dann ist
 U·N = {u·n : u ∈ U, n ∈ N} wieder eine Untergruppe.  Zum

AlgebraInLean/Reciprocity.lean

@@ -0,0 +1,99 @@
+/-
+Algebra in Lean — Kapitel 24 des Skripts
+========================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie übersetzt das
+Rechenbeispiel zum quadratischen Reziprozitätsgesetz nach
+Lean — und schließt den Kreis zum Anfang des Kurses.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+/-!
+# Quadratische Reziprozität
+
+## Das Mathlib-Wörterbuch
+
+* Das Legendre-Symbol (a/p) heißt `legendreSym p a : ℤ`;
+  es setzt eine `Fact (Nat.Prime p)`-Instanz voraus.
+
+* „a ist ein quadratischer Rest modulo p“ ist einfach
+  `IsSquare (a : ZMod p)`.
+
+* Das Lean-Lernthema dieses Kapitels ist die Taktik
+  `decide`: Aussagen über konkrete endliche Objekte —
+  „ist 7 ein Quadrat in 𝔽₁₇?“ — sind *entscheidbar*, und
+  Lean darf die Antwort einfach ausrechnen.  Das Ergebnis
+  ist ein vollwertiger Beweis.
+
+## Das Reziprozitätsgesetz
+
+Satz 24.2.1 des Skripts:
+
+**Satz 24.2.1 (Quadratisches Reziprozitätsgesetz).**  *Es seien p
+und q zwei unterschiedliche, ungerade Primzahlen.  Dann
+gilt die Gleichung
+(p/q)·(q/p) = (−1)^((p−1)/2 · (q−1)/2).*
+
+In Mathlib: `legendreSym.quadratic_reciprocity` — dort mit
+den Exponenten `p / 2` geschrieben, was für ungerade p
+dasselbe ist wie (p−1)/2.  Dazu die beiden Ergänzungssätze:
+Der erste — (−1/p) = 1 genau für p ≡ 1 (mod 4) — ist in der
+Quadrat-Formulierung `ZMod.exists_sq_eq_neg_one_iff`:
+-/
+
+example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
+    IsSquare (-1 : ZMod p) :=
+  ZMod.exists_sq_eq_neg_one_iff.mpr hp
+
+/-!
+## Das Rechenbeispiel
+
+„Ist 7 ein quadratischer Rest modulo 17?
+(7/17) = (17/7)·(−1)^{8·3} = (3/7)
+       = (7/3)·(−1)^{3·1} = −(1/3) = −1.
+Also ist die Antwort: Nein!“
+
+So rechnet man von Hand — und in der Klausur.  In Lean
+können wir dieselbe Frage der Taktik `decide` übergeben,
+die das Legendre-Symbol direkt auswertet:
+-/
+
+instance : Fact (Nat.Prime 17) := ⟨by norm_num⟩
+
+example : legendreSym 17 7 = -1 := by decide
+
+example : ¬ IsSquare (7 : ZMod 17) := by decide
+
+/-!
+Das ist kein Widerspruch zum Skript, sondern
+Arbeitsteilung: Das Reziprozitätsgesetz macht die Rechnung
+für *Menschen* effizient (und funktioniert auch bei
+riesigen Primzahlen); `decide` probiert stumpf alle
+Restklassen durch — für kleine p völlig in Ordnung.
+
+## Rückblick
+
+Damit endet der Kurs, wo er angefangen hat: Das
+Euler-Kriterium hinter dem Legendre-Symbol beruht darauf,
+dass 𝔽_p^* zyklisch von Ordnung p−1 ist — dieselbe
+Beobachtung, mit der wir in Kapitel drei den kleinen Satz
+von Fermat bewiesen haben.
+
+## Übungsaufgabe
+
+Ist 3 ein quadratischer Rest modulo 41?  Rechnen Sie erst
+von Hand nach dem Muster des Skript-Beispiels (mit
+Reziprozität und den Ergänzungssätzen) — und lassen Sie
+dann Lean Ihre Antwort bestätigen.  Ersetzen Sie dazu das
+`sorry` durch einen Beweis.
+-/
+
+instance : Fact (Nat.Prime 41) := ⟨by norm_num⟩
+
+theorem legendre_41_3 : legendreSym 41 3 = -1 := by
+  sorry
+
+end AlgebraInLean

Book.lean

@@ -6,8 +6,12 @@ import Book.Basics
 import Book.Quotients
 import Book.Ideals
 import Book.Polynomials
+import Book.Degrees
 import Book.LittleFermat
 import Book.Cauchy
+import Book.Frobenius
+import Book.Galois
+import Book.Reciprocity
 
 open Verso.Genre Manual
 
@@ -66,6 +70,14 @@ oder der ausführlichen Anleitung am Anfang der
 
 {include 0 Book.Polynomials}
 
+{include 0 Book.Degrees}
+
 {include 0 Book.LittleFermat}
 
 {include 0 Book.Cauchy}
+
+{include 0 Book.Frobenius}
+
+{include 0 Book.Galois}
+
+{include 0 Book.Reciprocity}

Book/Basics.lean

@@ -17,6 +17,7 @@ set_option verso.docstring.allowMissing true
 %%%
 htmlSplit := .never
 tag := "erste-schritte"
+file := "erste-schritte"
 %%%
 
 Ein Beweis in Lean beginnt mit `by` und besteht aus _Taktiken_.

Book/Cauchy.lean

@@ -19,6 +19,7 @@ set_option verso.docstring.allowMissing true
 %%%
 htmlSplit := .never
 tag := "cauchy"
+file := "cauchy"
 %%%
 
 Dieses Kapitel übersetzt den Anfang von Kapitel 18 des Skripts: das
@@ -28,7 +29,7 @@ ersten Mal selbst etwas in Lean _definieren_: eine Gruppenwirkung.
 
 # Das zentrale Schlüssellemma
 
-> *Lemma (Zentrales Schlüssellemma).* Es sei `m ∈ ℕ` und es sei `p`
+> *Lemma 18.1.1 (Zentrales Schlüssellemma).* Es sei `m ∈ ℕ` 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₀ = { m ∈ M : ∀ g ∈ G: g·m = m }` die Menge der Fixpunkte.  Dann
@@ -53,7 +54,7 @@ Wie sagt Mathlib das alles?
 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.6
+einfach die Bibliothek, so wie das Skript an dieser Stelle Satz 17.2.1
 zitiert.
 
 ```lean
@@ -74,7 +75,7 @@ gleich auf.)
 
 # Der Satz von Cauchy
 
-> *Satz (Satz von Cauchy).* Wenn die Ordnung einer endlichen Gruppe
+> *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
@@ -298,7 +299,7 @@ theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ}
   have hne : a ≠ 1 := by
     rintro rfl
     exact hw (Subtype.ext (Subtype.ext (Subtype.ext ha)))
-  -- „Nach Satz 17.4.11 hat a dann automatisch die
+  -- „Nach Satz 17.4.6 hat a dann automatisch die
   --  Ordnung p.“
   exact ⟨a, orderOf_eq_prime hpow hne⟩
 ```

Book/Degrees.lean

@@ -0,0 +1,120 @@
+import VersoManual
+import Manual.Meta
+-- Minimal-Imports statt `import Mathlib`, ermittelt mit
+-- `#min_imports`.
+import Mathlib.LinearAlgebra.FreeModule.PID
+import Mathlib.RingTheory.Flat.TorsionFree
+import Mathlib.RingTheory.Henselian
+import Mathlib.RingTheory.RegularLocalRing.Defs
+import Mathlib.RingTheory.SimpleRing.Principal
+
+open Verso.Genre
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+#doc (Manual) "Körpererweiterungen und die Gradformel" =>
+%%%
+htmlSplit := .never
+tag := "gradformel"
+file := "gradformel"
+%%%
+
+Dieses Kapitel übersetzt die Gradformel aus Kapitel 3 des Skripts nach
+Lean — unsere erste Begegnung mit linearer Algebra: Basen, Dimensionen
+und Körpererweiterungen als Vektorräume.
+
+# Das Mathlib-Wörterbuch
+
+* Eine Körpererweiterung `L/K` ist in Mathlib eine
+  `Algebra K L`-Instanz zwischen zwei Körpern — `L` wird damit
+  insbesondere ein K-Vektorraum, genau wie im Skript.
+
+* Eine Kette `K ⊆ L ⊆ M` besteht aus drei Algebra-Instanzen und der
+  Verträglichkeitsbedingung `IsScalarTower K L M` („erst nach `L`,
+  dann nach `M` einbetten ist dasselbe wie direkt nach `M`“).
+
+* Der Grad `[L:K]` heißt `Module.finrank K L`.  Achtung, hier weicht
+  die Konvention vom Skript ab: `finrank` hat Werte in `ℕ`, und
+  unendlichdimensionale Erweiterungen bekommen den Wert 0 — wo das
+  Skript in seiner Fußnote mit `∞` rechnet, rechnet Mathlib mit 0.
+  „`[L:K]` ist endlich“ ist die Typklasse `FiniteDimensional K L`.
+
+# Die Gradformel
+
+Satz 3.6.1 des Skripts, mit Beweis:
+
+> *Satz 3.6.1 (Gradformel).* Es sei `K ⊆ L ⊆ M` eine Kette von
+> Körpererweiterungen.  Dann gilt die Gleichung
+> `[M:K] = [M:L]·[L:K]`.
+>
+> _Beweis._ Wir kümmern uns zuerst um die unendlichen Fälle. …  Es
+> seien jetzt also `a := [L:K]` und `b := [M:L]` beide endlich.  Wähle
+> Basen `ℓ₁, …, ℓ_a` von `L` als K-Vektorraum und `m₁, …, m_b` von `M`
+> als L-Vektorraum.  Ich behaupte, dass die `a·b` Produkte `(ℓᵢ·mⱼ)`
+> eine Basis von `M` als K-Vektorraum bilden; damit ist dann sofort
+> `[M:K] = a·b` gezeigt.
+
+Die unendlichen Fälle entfallen in unserer Fassung, weil wir
+Endlichkeit voraussetzen; in Mathlibs 0-Konvention gilt die Formel
+sogar uneingeschränkt (`Module.finrank_mul_finrank`).
+
+Die Behauptung — mit den beiden Beweisschritten „Die Produkte bilden
+ein Erzeugendensystem“ und „Die Produkte sind linear unabhängig“ —
+ist in Mathlib die Konstruktion `Basis.smulTower`: Aus einer Basis
+`ℓ` von `L/K` und einer Basis `m` von `M/L` baut sie die Basis
+`(ℓᵢ • mⱼ)` von `M/K` (das Lemma `Basis.smulTower_apply` bestätigt,
+dass die Basiselemente wirklich die Produkte sind).  Der Rest ist
+Abzählen der Indexmenge.
+
+```lean
+theorem gradformel (K L M : Type*) [Field K] [Field L]
+    [Field M] [Algebra K L] [Algebra L M] [Algebra K M]
+    [IsScalarTower K L M]
+    [FiniteDimensional K L] [FiniteDimensional L M] :
+    Module.finrank K M
+      = Module.finrank L M * Module.finrank K L := by
+  -- „Wähle Basen ℓ₁, …, ℓ_a von L als K-Vektorraum und
+  --  m₁, …, m_b von M als L-Vektorraum.“
+  let ℓ := Module.finBasis K L
+  let m := Module.finBasis L M
+  -- „Ich behaupte, dass die a·b Produkte (ℓᵢ·mⱼ) eine
+  --  Basis von M als K-Vektorraum bilden …“
+  let basis := ℓ.smulTower m
+  -- „… damit ist dann sofort [M:K] = a·b gezeigt.“
+  rw [Module.finrank_eq_card_basis basis, Fintype.card_prod,
+    Fintype.card_fin, Fintype.card_fin, mul_comm]
+```
+
+# Bemerkungen
+
+Die beiden Beweisschritte des Skripts stecken im Beweis von
+`Basis.smulTower`: Das „Einsetzen“ im Erzeugendensystem-Schritt und
+das „Umsortieren“ im Unabhängigkeits-Schritt werden dort durch die
+Komposition der Koordinatenabbildungen erledigt —
+`Basis.smulTower_repr` sagt, dass die (i,j)-Koordinate von `x` gerade
+die i-te Koordinate der j-ten Koordinate ist: exakt das `μᵢⱼ` aus dem
+Skript.
+
+# Übungsaufgabe
+
+Das erste Korollar des Skripts zur Gradformel:
+
+> Es sei `K ⊆ L ⊆ M` eine Kette von Körpererweiterungen.  Wenn
+> `[M:K]` endlich ist, dann ist `[L:K]` endlich, und sogar ein Teiler
+> von `[M:K]`.
+
+Der erste Teil ist `Module.Finite.left` (und `Module.Finite.right`
+liefert die Endlichkeit von `[M:L]`) — beide müssen mit `have := …`
+in den Kontext geholt werden, damit die Instanzsuche sie sieht.  Der
+Teiler-Teil ist die Übung: Öffnen Sie `AlgebraInLean/Degrees.lean`
+und ersetzen Sie das `sorry` durch einen Beweis mit `gradformel`.
+
+```lean
+theorem grad_teilt (K L M : Type*) [Field K] [Field L]
+    [Field M] [Algebra K L] [Algebra L M] [Algebra K M]
+    [IsScalarTower K L M] [FiniteDimensional K M] :
+    Module.finrank K L ∣ Module.finrank K M := by
+  sorry
+```

Book/Frobenius.lean

@@ -0,0 +1,128 @@
+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 — 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 → R`, `a ↦ a^p`
+> ein Ringmorphismus.
+>
+> _Beweis._ Die Verträglichkeit mit der Multiplikation ist klar, weil
+> `R` kommutativ ist: `(a·b)^p = a^p·b^p`.  Ebenso ist `F(1) = 1`.
+> Interessant ist nur die Verträglichkeit mit der Addition.  …  Die
+> binomische Formel gilt in jedem kommutativen Ring ….  Für alle
+> Indizes `0 < k < p` ist der Binomialkoeffizient 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`.  Die Beobachtung des Skripts — über einem
+Integritätsring ist der Frobenius injektiv, über einem endlichen
+Körper sogar bijektiv — 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 `𝔽_p` ist die Identität: Für jedes
+`a ∈ 𝔽_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
+```

Book/Galois.lean

@@ -0,0 +1,120 @@
+import VersoManual
+import Manual.Meta
+-- Minimal-Imports statt `import Mathlib`: ermittelt mit
+-- `#min_imports`, ergänzt um die Galois-Theorie (die das
+-- Werkzeug wieder übersehen hat).
+import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.GroupWithZero.Units.Basic
+import Mathlib.Algebra.Ring.Equiv
+import Mathlib.FieldTheory.Galois.Basic
+
+open Verso.Genre
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+#doc (Manual) "Galois-Theorie" =>
+%%%
+htmlSplit := .never
+tag := "galois"
+file := "galois"
+%%%
+
+Dieses Kapitel zeigt, wie Mathlib die Begriffe der Galoistheorie aus
+den Kapiteln 15 und 16 des Skripts darstellt, und übersetzt die
+Fixkörper-Konstruktion — deren Beweis im Skript eine „Hausaufgabe“
+ist und es auch hier bleibt.
+
+# Das Mathlib-Wörterbuch
+
+* Die Galoisgruppe einer Körpererweiterung `L/K` ist der Typ
+  `L ≃ₐ[K] L` der K-Algebren-Automorphismen; Mathlib stellt dafür
+  sogar die Notation `Gal(L/K)` bereit.
+
+* „`L/K` ist galoissch“ ist die Typklasse `IsGalois K L` — definiert
+  als „separabel und normal“, genau wie im Skript.
+
+* Ein Zwischenkörper ist ein Term `Z : IntermediateField K L`; der
+  Fixkörper einer Untergruppe `H : Subgroup Gal(L/K)` heißt
+  `IntermediateField.fixedField H`.
+
+# Der Fixkörper
+
+Satz und Definition 16.1.1 des Skripts:
+
+> *Satz und Definition 16.1.1 (Invariante Elemente, Fixkörper).* Sei `L` ein
+> Körper und `G` eine Menge von Automorphismen `L → L`.  Dann ist die
+> Menge `Fix G = { a ∈ L : σ(a) = a für alle σ ∈ G }` ein Unterkörper
+> von `L`.  …  Der Beweis des folgenden Satzes ist eine Hausaufgabe.
+
+Wir definieren die Menge in Lean und beweisen exemplarisch die
+Abgeschlossenheit unter der Multiplikation — der Rest der Hausaufgabe
+ist, wie im Skript, Ihre Übungsaufgabe.
+
+```lean
+def Fix {L : Type*} [Field L] (G : Set (L ≃+* L)) :
+    Set L :=
+  {a | ∀ σ ∈ G, σ a = a}
+
+theorem mul_mem_fix {L : Type*} [Field L]
+    {G : Set (L ≃+* L)} {a b : L}
+    (ha : a ∈ Fix G) (hb : b ∈ Fix G) :
+    a * b ∈ Fix G := by
+  -- Automorphismen respektieren die Multiplikation:
+  intro σ hσ
+  rw [map_mul, ha σ hσ, hb σ hσ]
+```
+
+# Der Satz von Artin und der Hauptsatz
+
+Auch die großen Sätze dieses Teils der Vorlesung stehen in Mathlib;
+wir zitieren sie mit ihren Namen.
+
+> *Satz von Emil Artin (Satz 16.1.2).* Es sei `G` eine endliche Untergruppe der
+> Automorphismengruppe eines Körpers `L` und es sei `K := Fix G`.
+> Dann ist `L/K` eine Galoiserweiterung mit Galoisgruppe
+> `Gal(L/K) = G`.  Insbesondere ist `[L:K] = |G|`.
+
+Die Gradaussage ist `FixedPoints.finrank_eq_card`; das gebündelte
+Fixkörper-Objekt heißt dort `FixedPoints.subfield G L`.
+
+> *Hauptsatz der Galoistheorie (Satz 16.3.2).* Es sei `L/K` eine Galoiserweiterung
+> mit Galoisgruppe `G`.  Dann sind die Abbildungen `Z ↦ Gal(L/Z)` und
+> `H ↦ Fix H` zueinander inverse, inklusionsumkehrende Bijektionen
+> zwischen Zwischenkörpern und Untergruppen. …
+
+In Mathlib ist das der ordnungsumkehrende Isomorphismus
+`IsGalois.intermediateFieldEquivSubgroup`; das „ᵒᵈ“ (_order dual_)
+in seinem Typ ist genau das „inklusionsumkehrend“ des Skripts.  Die
+Gradaussage `|Gal(L/K)| = [L:K]` für Galoiserweiterungen heißt
+`IsGalois.card_aut_eq_finrank`:
+
+```lean
+example (K L : Type*) [Field K] [Field L] [Algebra K L]
+    [FiniteDimensional K L] [IsGalois K L] :
+    Nat.card (L ≃ₐ[K] L) = Module.finrank K L :=
+  IsGalois.card_aut_eq_finrank K L
+```
+
+# Übungsaufgabe
+
+Die „Hausaufgabe“ des Skripts: Vervollständigen Sie den Nachweis,
+dass `Fix G` ein Unterkörper ist — Abgeschlossenheit unter Addition
+und unter Inversen.  Für die Addition ist `map_add` das Gegenstück zu
+`map_mul`; für das Inverse respektieren Körperautomorphismen auch die
+Division: `map_inv₀`.  Öffnen Sie `AlgebraInLean/Galois.lean` und
+ersetzen Sie die beiden `sorry` durch Beweise.
+
+```lean
+theorem add_mem_fix {L : Type*} [Field L]
+    {G : Set (L ≃+* L)} {a b : L}
+    (ha : a ∈ Fix G) (hb : b ∈ Fix G) :
+    a + b ∈ Fix G := by
+  sorry
+
+theorem inv_mem_fix {L : Type*} [Field L]
+    {G : Set (L ≃+* L)} {a : L} (ha : a ∈ Fix G) :
+    a⁻¹ ∈ Fix G := by
+  sorry
+```

Book/Ideals.lean

@@ -18,6 +18,7 @@ set_option verso.docstring.allowMissing true
 %%%
 htmlSplit := .never
 tag := "ideale"
+file := "ideale"
 %%%
 
 Dieses Kapitel übersetzt den Satz „ℤ ist ein Hauptidealring“ aus
@@ -43,7 +44,7 @@ Lean.
 
 # ℤ ist ein Hauptidealring
 
-Der Satz aus Kapitel 9 des Skripts, mit Beweis:
+Satz 9.3.7 des Skripts, mit Beweis:
 
 > Es sei `I ⊂ ℤ` ein Ideal und `I ≠ {0}`.  Dann gibt es ein
 > `x ∈ I∖{0}`.  Beachte, dass dann auch `−x = (−1)·x` in `I` ist.

Book/LittleFermat.lean

@@ -15,12 +15,13 @@ set_option verso.docstring.allowMissing true
 %%%
 htmlSplit := .never
 tag := "little-fermat"
+file := "little-fermat"
 %%%
 
-Unser erster Beweis übersetzt Satz 17.5.2 des Skripts.  Hier das
+Unser erster Beweis übersetzt Satz 17.5.1 des Skripts.  Hier das
 deutsche Original, Aussage und Beweis:
 
-> *Satz (Kleiner Satz von Fermat).* Es sei `p ∈ ℕ` eine Primzahl und es
+> *Satz 17.5.1 (Kleiner Satz von Fermat).* Es sei `p ∈ ℕ` eine Primzahl und es
 > sei `a ∈ ℤ` irgendeine Zahl.  Dann ist `a^p ≡ a (mod p)`.
 >
 > _Beweis._ Falls `a` ein Vielfaches von `p` ist, ist die Sache klar.
@@ -85,7 +86,7 @@ theorem little_fermat (p : ℕ) (hp : p.Prime) (a : ℤ) :
     -- „… welche p−1 Elemente hat.“
     have card_units : Nat.card (ZMod p)ˣ = p - 1 := by
       rw [Nat.card_eq_fintype_card, ZMod.card_units p]
-    -- „Nach Satz 17.3.6 («Satz von Lagrange») ist die
+    -- „Nach Satz 17.2.4 («Satz von Lagrange») ist die
     --  Ordnung von ā, also die Größe der von ā erzeugten
     --  Untergruppe, ein Teiler von |𝔽_p^*| = p−1.“
     have lagrange :

Book/Polynomials.lean

@@ -15,6 +15,7 @@ set_option verso.docstring.allowMissing true
 %%%
 htmlSplit := .never
 tag := "polynome"
+file := "polynome"
 %%%
 
 Dieses Kapitel übersetzt die beiden Beispiele nach dem
@@ -40,9 +41,9 @@ Polynom-API kennen.
 
 # Das Eisenstein-Kriterium
 
-Der Satz aus Kapitel 7 des Skripts:
+Satz 7.2.1 des Skripts:
 
-> *Satz (Eisenstein-Kriterium).* Es sei `R` ein faktorieller Ring und
+> *Satz 7.2.1 (Eisenstein-Kriterium).* Es sei `R` ein faktorieller Ring und
 > es sei `f = a₀ + a₁·x + … + aₙ·xⁿ ∈ R[x]` ein Polynom vom Grad
 > `n > 0`.  Weiter sei `ggT(a₀, …, aₙ) = 1`.  Wenn es ein Primelement
 > `p ∈ R` gibt mit `p|a₀`, `p|a₁`, …, `p|a_{n−1}` und `p² ∤ a₀`, dann

Book/Quotients.lean

@@ -18,6 +18,7 @@ set_option verso.docstring.allowMissing true
 %%%
 htmlSplit := .never
 tag := "quotients"
+file := "quotients"
 %%%
 
 Dieses Kapitel übersetzt zwei Beweise rund um normale Untergruppen
@@ -95,7 +96,7 @@ example {G H : Type*} [Group G] [Group H] (N : Subgroup G)
 
 # Die Beobachtung: U·N ist eine Untergruppe
 
-Beobachtung aus Kapitel 17.3 des Skripts:
+Beobachtung 17.3.5 des Skripts:
 
 > Es sei `G` eine Gruppe und es sei `N ⊂ G` eine normale
 > Untergruppe.  Weiter sei `U ⊂ G` irgendeine Untergruppe.  Dann ist

Book/Reciprocity.lean

@@ -0,0 +1,103 @@
+import VersoManual
+import Manual.Meta
+-- Minimal-Imports statt `import Mathlib`, ermittelt mit
+-- `#min_imports`.
+import Mathlib.NumberTheory.LegendreSymbol.Basic
+import Mathlib.Tactic.NormNum.Prime
+
+open Verso.Genre
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+#doc (Manual) "Quadratische Reziprozität" =>
+%%%
+htmlSplit := .never
+tag := "reziprozitaet"
+file := "reziprozitaet"
+%%%
+
+Das letzte Kapitel übersetzt das Rechenbeispiel zum quadratischen
+Reziprozitätsgesetz aus Kapitel 24 des Skripts nach Lean — und
+schließt den Kreis zum Anfang des Kurses.
+
+# Das Mathlib-Wörterbuch
+
+* Das Legendre-Symbol `(a/p)` heißt `legendreSym p a : ℤ`; es setzt
+  eine `Fact (Nat.Prime p)`-Instanz voraus.
+
+* „`a` ist ein quadratischer Rest modulo `p`“ ist einfach
+  `IsSquare (a : ZMod p)`.
+
+* Das Lean-Lernthema dieses Kapitels ist die Taktik `decide`:
+  Aussagen über konkrete endliche Objekte — „ist 7 ein Quadrat in
+  `𝔽₁₇`?“ — sind _entscheidbar_, und Lean darf die Antwort einfach
+  ausrechnen.  Das Ergebnis ist ein vollwertiger Beweis.
+
+# Das Reziprozitätsgesetz
+
+Satz 24.2.1 des Skripts:
+
+> *Satz 24.2.1 (Quadratisches Reziprozitätsgesetz).* Es seien `p` und `q`
+> zwei unterschiedliche, ungerade Primzahlen.  Dann gilt die
+> Gleichung `(p/q)·(q/p) = (−1)^((p−1)/2 · (q−1)/2)`.
+
+In Mathlib: `legendreSym.quadratic_reciprocity` — dort mit den
+Exponenten `p / 2` geschrieben, was für ungerade `p` dasselbe ist wie
+`(p−1)/2`.  Dazu die beiden Ergänzungssätze: Der erste —
+`(−1/p) = 1` genau für `p ≡ 1 (mod 4)` — ist in der
+Quadrat-Formulierung `ZMod.exists_sq_eq_neg_one_iff`:
+
+```lean
+example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
+    IsSquare (-1 : ZMod p) :=
+  ZMod.exists_sq_eq_neg_one_iff.mpr hp
+```
+
+# Das Rechenbeispiel
+
+Aus dem Skript:
+
+> Ist 7 ein quadratischer Rest modulo 17?
+> `(7/17) = (17/7)·(−1)^{8·3} = (3/7) = (7/3)·(−1)^{3·1} = −(1/3)
+> = −1`.  Also ist die Antwort: „Nein!“
+
+So rechnet man von Hand — und in der Klausur.  In Lean können wir
+dieselbe Frage der Taktik `decide` übergeben, die das Legendre-Symbol
+direkt auswertet:
+
+```lean
+instance : Fact (Nat.Prime 17) := ⟨by norm_num⟩
+
+example : legendreSym 17 7 = -1 := by decide
+
+example : ¬ IsSquare (7 : ZMod 17) := by decide
+```
+
+Das ist kein Widerspruch zum Skript, sondern Arbeitsteilung: Das
+Reziprozitätsgesetz macht die Rechnung für _Menschen_ effizient (und
+funktioniert auch bei riesigen Primzahlen); `decide` probiert stumpf
+alle Restklassen durch — für kleine `p` völlig in Ordnung.
+
+# Rückblick
+
+Damit endet der Kurs, wo er angefangen hat: Das Euler-Kriterium
+hinter dem Legendre-Symbol beruht darauf, dass `𝔽_p^*` zyklisch von
+Ordnung `p−1` ist — dieselbe Beobachtung, mit der wir im Kapitel über
+den kleinen Satz von Fermat gerechnet haben.
+
+# Übungsaufgabe
+
+Ist 3 ein quadratischer Rest modulo 41?  Rechnen Sie erst von Hand
+nach dem Muster des Skript-Beispiels (mit Reziprozität und den
+Ergänzungssätzen) — und lassen Sie dann Lean Ihre Antwort bestätigen.
+Öffnen Sie `AlgebraInLean/Reciprocity.lean` und ersetzen Sie das
+`sorry` durch einen Beweis.
+
+```lean
+instance : Fact (Nat.Prime 41) := ⟨by norm_num⟩
+
+theorem legendre_41_3 : legendreSym 41 3 = -1 := by
+  sorry
+```

README.md

@@ -36,8 +36,12 @@ Lean/Mathlib.
 | `AlgebraInLean/Quotients.lean` | Kapitel 2, 17 | Kernels, normal subgroups, quotient groups |
 | `AlgebraInLean/Ideals.lean` | Kapitel 9 | Ideals; ℤ is a principal ideal ring |
 | `AlgebraInLean/Polynomials.lean` | Kapitel 7 | Polynomials; Eisenstein's criterion applied |
+| `AlgebraInLean/Degrees.lean` | Kapitel 3 | Field extensions; the tower law |
 | `AlgebraInLean/LittleFermat.lean` | Kapitel 17 | Fermat's little theorem via Lagrange |
 | `AlgebraInLean/Cauchy.lean` | Kapitel 18 | The key lemma on fixed points and Cauchy's theorem |
+| `AlgebraInLean/Frobenius.lean` | Kapitel 14 | Finite fields; the Frobenius endomorphism |
+| `AlgebraInLean/Galois.lean` | Kapitel 15, 16 | Galois theory; fixed fields |
+| `AlgebraInLean/Reciprocity.lean` | Kapitel 24 | Quadratic reciprocity; computing Legendre symbols |
 
 ## The rendered course notes