From 4ff2bb5fb2cb7e3136ed2f28c01a34d915af96b3 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 13 Aug 2026 09:47:44 +0200 Subject: [PATCH] Working. --- Book/Cauchy.lean | 17 +++++++++-------- Book/Degrees.lean | 6 +++--- Book/Frobenius.lean | 4 ++-- Book/Ideals.lean | 11 ++++++----- Book/LittleFermat.lean | 3 ++- Book/Polynomials.lean | 11 ++++++----- Book/Reciprocity.lean | 15 ++++++++------- 7 files changed, 36 insertions(+), 31 deletions(-) diff --git a/Book/Cauchy.lean b/Book/Cauchy.lean index 0304675..0bea4a6 100644 --- a/Book/Cauchy.lean +++ b/Book/Cauchy.lean @@ -44,15 +44,15 @@ Wie sagt Mathlib das alles? Satz von Cauchy unten!). 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 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 +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 @@ -318,10 +318,11 @@ 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 — +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. diff --git a/Book/Degrees.lean b/Book/Degrees.lean index 1953fde..fd988e2 100644 --- a/Book/Degrees.lean +++ b/Book/Degrees.lean @@ -99,9 +99,9 @@ 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. +`Basis.smulTower_repr` sagt, dass die $`(i,j)`-Koordinate von `x` +gerade die $`i`-te Koordinate der $`j`-ten Koordinate ist: exakt das +$`μ_{ij}` aus dem Skript. # Übungsaufgabe diff --git a/Book/Frobenius.lean b/Book/Frobenius.lean index fd00804..89e8a38 100644 --- a/Book/Frobenius.lean +++ b/Book/Frobenius.lean @@ -113,8 +113,8 @@ Mathlib bündelt die drei Verträglichkeiten zum Ringmorphismus `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`. +Zu jeder Primzahlpotenz $`p^n` gibt es genau einen Körper mit +$`p^n` Elementen. In Mathlib heißt er `GaloisField p n`. # Übungsaufgabe diff --git a/Book/Ideals.lean b/Book/Ideals.lean index 76e928c..bf602bc 100644 --- a/Book/Ideals.lean +++ b/Book/Ideals.lean @@ -30,12 +30,13 @@ Lean. * Ein Ideal in einem kommutativen Ring `R` ist ein Term `I : Ideal R`. Die beiden Bedingungen aus der Ideal-Definition des - Skripts heißen `I.add_mem` (für alle `a, b ∈ I` ist `a+b ∈ I`) und + Skripts heißen `I.add_mem` (für alle $`a, b \in I` ist + $`a+b \in I`) und `I.mul_mem_left` (für alle $`r \in R` und $`a \in I` ist $`r \cdot a \in I`); außerdem ist `I.zero_mem : 0 ∈ I`. * Das von einer Menge `s` erzeugte Ideal ist `Ideal.span s`; ein - _Hauptideal_ `(a)` ist also `Ideal.span {a}`. Die Beobachtung + _Hauptideal_ $`(a)` ist also `Ideal.span {a}`. Die Beobachtung „Hauptideale und Teilbarkeit“ des Skripts ist das Lemma `Ideal.mem_span_singleton : b ∈ span {a} ↔ a ∣ b`. @@ -59,9 +60,9 @@ Satz 9.3.7 des Skripts, mit Beweis: Zwei Anmerkungen zur Übersetzung. Das „kleinste positive Element“ liefert das Wohlordnungsprinzip, in Mathlib -`Int.exists_least_of_bdd`. Und wo das Skript nur positive `b` +`Int.exists_least_of_bdd`. Und wo das Skript nur positive $`b` behandelt (und den Rest dem Leser überlässt), nehmen wir gleich -beliebige `b` — die Division mit Rest in Lean funktioniert für alle +beliebige $`b` — die Division mit Rest in Lean funktioniert für alle ganzen Zahlen. ```lean @@ -125,7 +126,7 @@ theorem int_hauptidealring (I : Ideal ℤ) : In Mathlib ist `IsPrincipalIdealRing ℤ` eine Instanz: ℤ ist ein euklidischer Ring, und `EuclideanDomain.to_principal_ideal_domain` führt genau unser Argument für beliebige euklidische Ringe. Damit -ist auch der zweite Satz des Skript-Abschnitts abgedeckt: `K[x]` ist +ist auch der zweite Satz des Skript-Abschnitts abgedeckt: $`K[x]` ist euklidisch (Division mit Rest, wobei der Grad die Rolle des Betrags übernimmt), also ein Hauptidealring. Auch der Hilbertsche Basissatz aus diesem Kapitel steht in Mathlib: `Polynomial.isNoetherianRing`. diff --git a/Book/LittleFermat.lean b/Book/LittleFermat.lean index fa169dc..1392101 100644 --- a/Book/LittleFermat.lean +++ b/Book/LittleFermat.lean @@ -117,7 +117,8 @@ Man beachte, wie treu die Übersetzung ist. Die Fallunterscheidung „Falls … ist die Sache klar / Ansonsten …“ wird zu `by_cases`; das Zitat des Satzes von Lagrange wird zum Bibliothekslemma `Subgroup.card_subgroup_dvd_card`; und die Formulierung „die Ordnung -von `ā`, also die Größe der von `ā` erzeugten Untergruppe“ ist genau +von $`\overline{a}`, also die Größe der von $`\overline{a}` +erzeugten Untergruppe“ ist genau das Umschreiben mit `Nat.card_zpowers`, das `orderOf u` mit der Mächtigkeit der von `u` erzeugten Untergruppe `Subgroup.zpowers u` identifiziert. diff --git a/Book/Polynomials.lean b/Book/Polynomials.lean index 049f07a..cd4dc80 100644 --- a/Book/Polynomials.lean +++ b/Book/Polynomials.lean @@ -27,14 +27,15 @@ Polynom-API kennen. * Der Polynomring über `R` heißt `Polynomial R`, mit der Notation `R[X]`. Die Variable ist `X`, das konstante Polynom zu `a : R` ist - `C a`; ein Polynom wie `x³−2` schreibt sich also `X ^ 3 - C 2`. + `C a`; ein Polynom wie $`x^3 - 2` schreibt sich also + `X ^ 3 - C 2`. * Der k-te Koeffizient ist `f.coeff k`, der Grad `f.degree`. Achtung: `degree` hat Werte in `WithBot ℕ` — das Nullpolynom bekommt den Grad `⊥` („minus unendlich“, wie im Skript). Daneben gibt es `f.natDegree : ℕ`. -* „f ist normiert“ (Leitkoeffizient 1) ist `f.Monic`; „f ist +* „$`f` ist normiert“ (Leitkoeffizient 1) ist `f.Monic`; „$`f` ist irreduzibel“ ist `Irreducible f`; die Bedingung „ggT der Koeffizienten ist 1“ aus dem Eisenstein-Kriterium heißt `f.IsPrimitive` (kein Nichteinheits-Teiler in `R`). @@ -122,10 +123,10 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ) Mathlibs Beweis des Eisenstein-Kriteriums folgt derselben Idee wie das Erklärvideo 9-1 des Skripts: Reduktion der Koeffizienten modulo -`p`. Auch das Gauß-Kriterium aus dem ersten Teil des Kapitels steht +$`p`. Auch das Gauß-Kriterium aus dem ersten Teil des Kapitels steht in Mathlib (Datei `Mathlib.RingTheory.Polynomial.GaussLemma`). Das -zweite Beispiel des Skripts — `xⁿ − p` ist irreduzibel und deshalb -das Minimalpolynom von `ⁿ√p` — greifen wir im Kapitel über +zweite Beispiel des Skripts — $`x^n - p` ist irreduzibel und deshalb +das Minimalpolynom von $`\sqrt[n]{p}` — greifen wir im Kapitel über Körpererweiterungen wieder auf. # Übungsaufgabe diff --git a/Book/Reciprocity.lean b/Book/Reciprocity.lean index dfef092..66f8c6a 100644 --- a/Book/Reciprocity.lean +++ b/Book/Reciprocity.lean @@ -28,13 +28,14 @@ schließt den Kreis zum Anfang des Kurses. `legendreSym p a : ℤ`; es setzt eine `Fact (Nat.Prime p)`-Instanz voraus. -* „`a` ist ein quadratischer Rest modulo `p`“ ist einfach +* „$`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. + $`\mathbb{F}_{17}`?“ — sind _entscheidbar_, und Lean darf die + Antwort einfach ausrechnen. Das Ergebnis ist ein vollwertiger + Beweis. # Das Reziprozitätsgesetz @@ -81,14 +82,14 @@ 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. +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. +hinter dem Legendre-Symbol beruht darauf, dass $`\mathbb{F}_p^*` +zyklisch von Ordnung $`p-1` ist — dieselbe Beobachtung, mit der wir +im Kapitel über den kleinen Satz von Fermat gerechnet haben. # Übungsaufgabe