From cc75cdc801de659586939408b02259b6d1ad5f94 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 13 Aug 2026 10:08:19 +0200 Subject: [PATCH] Cleanup and final touches --- AlgebraInLean/Basics.lean | 6 ++-- AlgebraInLean/Cauchy.lean | 23 +++++++------- AlgebraInLean/Degrees.lean | 18 +++++------ AlgebraInLean/Elements.lean | 6 ++-- AlgebraInLean/Frobenius.lean | 15 ++++----- AlgebraInLean/Galois.lean | 14 ++++----- AlgebraInLean/Ideals.lean | 6 ++-- AlgebraInLean/LittleFermat.lean | 10 +++--- AlgebraInLean/Polynomials.lean | 16 +++++----- AlgebraInLean/Quotients.lean | 10 +++--- AlgebraInLean/Reciprocity.lean | 21 +++++++------ AlgebraInLean/Transitivity.lean | 8 ++--- Book.lean | 3 ++ Book/Appendix.lean | 54 +++++++++++++++++++++++++++++++++ Book/Basics.lean | 9 +++--- Book/Cauchy.lean | 26 ++++++++-------- Book/Degrees.lean | 31 ++++++++++--------- Book/Elements.lean | 32 +++++++++---------- Book/Frobenius.lean | 12 ++++---- Book/Galois.lean | 12 ++++---- Book/Ideals.lean | 8 ++--- Book/LittleFermat.lean | 12 ++++---- Book/Polynomials.lean | 16 +++++----- Book/Quotients.lean | 10 +++--- Book/Reciprocity.lean | 20 ++++++------ Book/Transitivity.lean | 18 +++++------ README.md | 5 ++- 27 files changed, 243 insertions(+), 178 deletions(-) create mode 100644 Book/Appendix.lean diff --git a/AlgebraInLean/Basics.lean b/AlgebraInLean/Basics.lean index 8391720..e46f476 100644 --- a/AlgebraInLean/Basics.lean +++ b/AlgebraInLean/Basics.lean @@ -61,8 +61,8 @@ das Inverse `a⁻¹`; die Axiome heißen `mul_assoc`, `one_mul`, Ein Unterschied fällt auf: Das Skript *fordert* die Eindeutigkeit von neutralem Element und Inversen, Mathlib -nicht. Das ist kein Widerspruch — die Eindeutigkeit folgt -aus den übrigen Axiomen. Genau das beweisen wir jetzt, mit +nicht. Das ist kein Widerspruch, denn die Eindeutigkeit +folgt aus den übrigen Axiomen. Genau das beweisen wir jetzt, mit dem Standardargument aus der linearen Algebra: *Es sei e ein weiteres Element, das von links neutral wirkt. @@ -83,7 +83,7 @@ theorem neutral_eindeutig {G : Type*} [Group G] (e : G) Zeigen Sie ebenso die Eindeutigkeit des Inversen: Wenn a·b = 1 ist, dann ist b bereits *das* Inverse a⁻¹. Das Standardargument: b = 1·b = (a⁻¹·a)·b = a⁻¹·(a·b) = a⁻¹·1 -= a⁻¹. Ersetzen Sie das `sorry` durch einen Beweis — die += a⁻¹. Ersetzen Sie das `sorry` durch einen Beweis. Die Taktik `calc` aus dem Beweis oben und die Lemmata `one_mul`, `inv_mul_cancel`, `mul_assoc`, `mul_one` genügen. -/ diff --git a/AlgebraInLean/Cauchy.lean b/AlgebraInLean/Cauchy.lean index a3e6729..8f291aa 100644 --- a/AlgebraInLean/Cauchy.lean +++ b/AlgebraInLean/Cauchy.lean @@ -33,8 +33,8 @@ 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 äquivalent, - nach dem Satz von Cauchy unten!). Das Lemma + 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. @@ -48,7 +48,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 +`IsPGroup.card_modEq_card_fixedPoints`. Wir zitieren hier also einfach die Bibliothek, so wie das Skript an dieser Stelle Satz 17.2.1 zitiert. -/ @@ -69,15 +69,15 @@ 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 +Gruppenwirkung. Diesmal gibt es also vor dem eigentlichen Satz echte Arbeit: Wir bauen erst die Menge und die Wirkung. „Betrachte die Menge M = { (a₁, …, a_p) ∈ G ⨯ ⋯ ⨯ G : a₁·a₂ ⋯ a_p = e }.“ Mathlib kennt diese Menge. Ein p-Tupel von Gruppenelementen -ist ein `List.Vector G p` — eine Liste der Länge p —, und M -ist die Menge `Equiv.Perm.vectorsProdEqOne G p` aller +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₁, …, a_p) ∈ M, dann stellen wir erst @@ -98,8 +98,9 @@ Vertauschen wirken.“ Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p` um k Stellen ist `VectorsProdEqOne.rotate v k`. Die Fußnote -des Skripts — der Shift bildet M auf sich ab, „weil in jeder -Gruppe aus a·b = e auch b·a = e gilt“ — ist das Mathlib-Lemma +des Skripts begründet, dass der Shift M auf sich abbildet, +„weil in jeder Gruppe aus a·b = e auch b·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. @@ -109,7 +110,7 @@ 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 +der Verschiebung *modulo p* abhängt. Genau deshalb wirkt ℤ/(p) und nicht bloß ℕ. -/ @@ -163,7 +164,7 @@ M₀ = { (a, …, a) ∈ 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` — das ist (a, …, a) — ist. (Die +`List.replicate p a` = (a, …, 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 @@ -298,7 +299,7 @@ theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ} 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. + selbst an, oder finden Sie die Aussage in Mathlib. Ersetzen Sie dazu das `sorry` durch einen Beweis. -/ diff --git a/AlgebraInLean/Degrees.lean b/AlgebraInLean/Degrees.lean index d16d333..ff1c3d1 100644 --- a/AlgebraInLean/Degrees.lean +++ b/AlgebraInLean/Degrees.lean @@ -18,7 +18,7 @@ namespace AlgebraInLean ## Das Mathlib-Wörterbuch * Eine Körpererweiterung L/K ist in Mathlib eine - `Algebra K L`-Instanz zwischen zwei Körpern — L wird damit + `Algebra K L`-Instanz zwischen zwei Körpern. Damit wird L insbesondere ein K-Vektorraum, genau wie im Skript. * Eine Kette K ⊆ L ⊆ M besteht aus drei Algebra-Instanzen @@ -29,8 +29,8 @@ namespace AlgebraInLean * 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 + den Wert 0. Wo das Skript in seiner Fußnote mit ∞ + rechnet, rechnet Mathlib also mit 0. „[L:K] ist endlich“ ist die Typklasse `FiniteDimensional K L`. ## Die Gradformel @@ -40,7 +40,7 @@ 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 +„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`). @@ -51,9 +51,9 @@ 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 Behauptung zerfällt in die beiden Beweisschritte „Die Produkte bilden ein Erzeugendensystem“ und „Die -Produkte sind linear unabhängig“ — ist in Mathlib die +Produkte sind linear unabhängig“. In Mathlib ist sie 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 @@ -85,7 +85,7 @@ theorem gradformel (K L M : Type*) [Field K] [Field L] von `Basis.smulTower`: Das „Einsetzen“ im Erzeugendensystem-Schritt und das „Umsortieren“ im Unabhängigkeits-Schritt werden dort durch die - Komposition der Koordinatenabbildungen erledigt — + 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. @@ -101,8 +101,8 @@ 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, +`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`. diff --git a/AlgebraInLean/Elements.lean b/AlgebraInLean/Elements.lean index 08d68f7..1aab85d 100644 --- a/AlgebraInLean/Elements.lean +++ b/AlgebraInLean/Elements.lean @@ -25,7 +25,7 @@ open IntermediateField * Das Minimalpolynom heißt `minpoly K a`; der Grad [a:K] des Skripts ist `(minpoly K a).natDegree`. Für transzendentes a - ist `minpoly K a = 0` — wieder die 0-Konvention für ∞. + ist `minpoly K a = 0`; das ist wieder die 0-Konvention für ∞. * Der Zwischenkörper K(a) heißt `K⟮a⟯`, kurz für `IntermediateField.adjoin K {a}`; die Notation kommt mit @@ -39,8 +39,8 @@ open IntermediateField Satz 3.5.4 des Skripts: „Es sei L/K eine Körpererweiterung und es sei a ∈ L. Dann gilt die Gleichheit [a:K] = [K(a):K].“ -Die Behauptung des Beweises — die Potenzen 1, a, …, a^{m-1} -bilden eine Basis von K(a) — ist in Mathlib die Konstruktion +Der Beweis behauptet, dass die Potenzen 1, a, …, a^{m-1} eine +Basis von K(a) bilden. In Mathlib ist das die Konstruktion `IntermediateField.adjoin.powerBasis`. -/ diff --git a/AlgebraInLean/Frobenius.lean b/AlgebraInLean/Frobenius.lean index e3928d9..52a1be0 100644 --- a/AlgebraInLean/Frobenius.lean +++ b/AlgebraInLean/Frobenius.lean @@ -5,8 +5,9 @@ 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. +(DefSatz_Frobenius-Endomorphismus) Satz für Satz nach Lean. +Es geht um den „Traum jedes Studienanfängers“: +(a+b)^p = a^p + b^p. -/ import Mathlib @@ -101,17 +102,17 @@ theorem frobenius_add {R : Type*} [CommRing R] (p : ℕ) 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 +2. 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 𝔽_p ist die Identität: Für jedes -a ∈ 𝔽_p ist a^p = a. Das ist ein alter Bekannter — der +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. diff --git a/AlgebraInLean/Galois.lean b/AlgebraInLean/Galois.lean index bf7b7ff..f13f307 100644 --- a/AlgebraInLean/Galois.lean +++ b/AlgebraInLean/Galois.lean @@ -5,7 +5,7 @@ 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 +Fixkörper-Konstruktion (DefSatz_Fixkoerper). Die „Hausaufgabe“ des Skripts wird auch hier zur Übungsaufgabe. -/ import Mathlib @@ -21,7 +21,7 @@ namespace AlgebraInLean `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` — +* „L/K ist galoissch“ ist die Typklasse `IsGalois K L`, definiert als „separabel und normal“, genau wie im Skript. @@ -41,7 +41,7 @@ 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 +die Abgeschlossenheit unter der Multiplikation. Der Rest der Hausaufgabe ist, wie im Skript, Ihre Übungsaufgabe. -/ @@ -67,7 +67,7 @@ Mathlib; wir zitieren sie mit ihren Namen. 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 +Die Gradaussage ist `FixedPoints.finrank_eq_card`; das gebündelte Fixkörper-Objekt heißt dort `FixedPoints.subfield G L`. @@ -75,7 +75,7 @@ gebündelte Fixkörper-Objekt heißt dort 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 +und Untergruppen […].* In Mathlib ist das der ordnungsumkehrende Isomorphismus `IsGalois.intermediateFieldEquivSubgroup`; das „ᵒᵈ“ (order dual) im Typ ist genau das „inklusionsumkehrend“ des @@ -94,8 +94,8 @@ example (K L : Type*) [Field K] [Field L] [Algebra 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 +Nachweis, dass Fix G ein Unterkörper ist, also die +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. diff --git a/AlgebraInLean/Ideals.lean b/AlgebraInLean/Ideals.lean index 8d7459f..c81f875 100644 --- a/AlgebraInLean/Ideals.lean +++ b/AlgebraInLean/Ideals.lean @@ -4,8 +4,8 @@ Algebra in Lean — Kapitel 9 des Skripts Diese Datei begleitet das Skript „Algebra und Zahlentheorie“ (Stefan Kebekus, CC-BY 4.0). Sie übersetzt den Satz „ℤ ist -ein Hauptidealring“ (satz:9-1-4) Satz für Satz nach Lean — -der klassische Beweis über Division mit Rest. +ein Hauptidealring“ (satz:9-1-4) Satz für Satz nach Lean. +Es ist der klassische Beweis über Division mit Rest. -/ import Mathlib @@ -51,7 +51,7 @@ 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 behandelt (und den Rest dem Leser überlässt), nehmen wir -gleich beliebige b — die Division mit Rest in Lean +gleich beliebige b; die Division mit Rest in Lean funktioniert für alle ganzen Zahlen. -/ diff --git a/AlgebraInLean/LittleFermat.lean b/AlgebraInLean/LittleFermat.lean index c46d3d2..f9b085c 100644 --- a/AlgebraInLean/LittleFermat.lean +++ b/AlgebraInLean/LittleFermat.lean @@ -4,8 +4,8 @@ Algebra in Lean — Kapitel 17 Diese Datei begleitet das Skript „Algebra und Zahlentheorie“ (Stefan Kebekus, CC-BY 4.0). Sie übersetzt einen Satz des -Skripts — den kleinen Satz von Fermat, `satz:kleinerFermat` in -Kapitel 17 — Satz für Satz nach Lean. Das deutsche Original +Skripts Satz für Satz nach Lean: den kleinen Satz von Fermat +(`satz:kleinerFermat` in Kapitel 17). Das deutsche Original jedes Beweissatzes steht als Kommentar direkt über dem Lean-Code, der ihn umsetzt: So sieht man, wie sich die Standardphrasen eines Vorlesungsbeweises nach Lean/Mathlib @@ -26,7 +26,7 @@ Bevor wir das in Lean formulieren können, müssen wir wissen, wie Mathlib über die beteiligten Objekte spricht. * Der Restklassenring ℤ/(p) heißt `ZMod p`. Die Restklasse - einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)` — + einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)`; Lean fügt den kanonischen Ringmorphismus ℤ → ℤ/(p) automatisch ein („Koerzion“). @@ -41,7 +41,7 @@ wie Mathlib über die beteiligten Objekte spricht. * Das Skript sagt „es sei p eine Primzahl“. In Lean führen wir die Primalität von `p` als Hypothese `hp : p.Prime` mit. - Manche Tatsachen — etwa dass ℤ/(p) ein Körper ist — findet + Manche Tatsachen, etwa dass ℤ/(p) ein Körper ist, findet Leans Automatisierung nur, wenn die Hypothese als *Instanz* registriert ist; genau das leistet die erste Beweiszeile `have : Fact p.Prime := ⟨hp⟩`. @@ -108,7 +108,7 @@ example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a := 2. **Übungsaufgabe** (das ist `bem:kleinerFermat` im Skript). In Anwendungen verwendet man häufig die äquivalente Formulierung a^(p−1) ≡ 1 (mod p) für nicht durch p - teilbare a. Leiten Sie sie aus `little_fermat` ab — oder + teilbare a. Leiten Sie sie aus `little_fermat` ab, oder geben Sie einen direkten Beweis nach den Ideen oben. Ersetzen Sie dazu das `sorry` durch einen Beweis. -/ diff --git a/AlgebraInLean/Polynomials.lean b/AlgebraInLean/Polynomials.lean index 99e675b..2e271de 100644 --- a/AlgebraInLean/Polynomials.lean +++ b/AlgebraInLean/Polynomials.lean @@ -25,7 +25,7 @@ open Polynomial 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 + Achtung: `degree` hat Werte in `WithBot ℕ`; das Nullpolynom bekommt den Grad ⊥ („minus unendlich“, wie im Skript). Daneben gibt es `f.natDegree : ℕ`. @@ -47,7 +47,7 @@ p² ∤ a₀, dann ist f irreduzibel in R[x].* In Mathlib heißt der Satz `Polynomial.irreducible_of_eisenstein_criterion`. Er ist dort über ein Primideal P statt eines Primelements p -formuliert — für uns ist P das Hauptideal (p) aus dem +formuliert. Für uns ist P das Hauptideal (p) aus dem letzten Kapitel, und „p teilt aₖ“ wird zu `f.coeff k ∈ Ideal.span {p}`. Statt „p ∤ aₙ“ (was im Skript aus ggT = 1 folgt) verlangt Mathlib direkt @@ -59,7 +59,7 @@ aus ggT = 1 folgt) verlangt Mathlib direkt eine Primzahl p, aber nicht durch p² teilbar ist.“ Das Skript lässt die Kontrolle der Eisenstein-Bedingungen -als Kopfrechnung weg — in Lean führen wir sie aus und lernen +als Kopfrechnung weg. In Lean führen wir sie aus und lernen dabei die Koeffizienten-API kennen: `coeff_sub`, `coeff_X_pow` und `coeff_C` berechnen die Koeffizienten von xⁿ − r, nämlich aₙ = 1, a₀ = −r und aₖ = 0 sonst. @@ -84,7 +84,7 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ) · rw [hmonic.leadingCoeff, Ideal.mem_span_singleton] exact fun h => hprime.not_isUnit (isUnit_of_dvd_one h) -- „p|a₀, …, p|a_{n−1}“: Unterhalb von Grad n sind die - -- Koeffizienten −r (bei k = 0) und 0 (sonst) — beide + -- Koeffizienten −r (bei k = 0) und 0 (sonst), beide -- durch p teilbar. · intro k hk have hkn : k < n := by @@ -116,16 +116,16 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ) des Kapitels steht in Mathlib (Datei `Mathlib.RingTheory.Polynomial.GaussLemma`). -2. Das zweite Beispiel des Skripts — xⁿ − p ist irreduzibel - und deshalb das Minimalpolynom von ⁿ√p — greifen wir im - Kapitel über Körpererweiterungen wieder auf. +2. Das zweite Beispiel des Skripts greifen wir im Kapitel + über Körpererweiterungen wieder auf: xⁿ − p ist + irreduzibel und deshalb das Minimalpolynom von ⁿ√p. ## Übungsaufgabe Genau dieses zweite Beispiel ist die Übung: „Das Polynom xⁿ − p ∈ ℤ[x] ist für jede Primzahl p irreduzibel.“ Wenden Sie `xn_sub_r_irreduzibel` mit r = p an. Zu zeigen bleibt -p² ∤ p: Aus p = p²·c folgt durch Kürzen 1 = p·c — dann wäre +p² ∤ p: Aus p = p²·c folgt durch Kürzen 1 = p·c; dann wäre p eine Einheit, im Widerspruch zur Primalität. Nützlich sind `mul_left_cancel₀`, `isUnit_of_dvd_one` und `Prime.not_isUnit`. Ersetzen Sie das `sorry` durch einen diff --git a/AlgebraInLean/Quotients.lean b/AlgebraInLean/Quotients.lean index 59ea991..0e07b29 100644 --- a/AlgebraInLean/Quotients.lean +++ b/AlgebraInLean/Quotients.lean @@ -24,7 +24,7 @@ namespace AlgebraInLean Verknüpfung und Inversen abgeschlossen ist, sagen `U.mul_mem` und `U.inv_mem`. -* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein +* Ein Gruppenmorphismus ist ein Term `φ : G →* Q`, ein „Bündel“ aus der Abbildung und den Nachweisen `map_mul : φ (a·b) = φ a · φ b` (daraus folgen `map_one` und `map_inv`). Der Kern heißt `φ.ker`; @@ -64,7 +64,7 @@ Mathlib kennt diese Aussage als Instanz `MonoidHom.normal_ker : φ.ker.Normal`. Das Skript fährt fort: Untergruppen mit dieser Eigenschaft heißen *normale Untergruppen* oder *Normalteiler*, und die Bedingung ist -nicht nur notwendig, sondern auch hinreichend — zu jedem +nicht nur notwendig, sondern auch hinreichend: Zu jedem Normalteiler existiert eine Restklassengruppe. ## Die Restklassengruppe und ihre universelle Eigenschaft @@ -73,8 +73,8 @@ Das Skript definiert die Restklassengruppe in Kapitel 17.3 über ihre universelle Eigenschaft. Mathlib stellt beides bereit: den Quotienten `G ⧸ N` mit der Quotientenabbildung `QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle -Eigenschaft als `QuotientGroup.lift` — gegeben ein -Morphismus `α : G →* H` mit `N ≤ α.ker` erhält man den +Eigenschaft als `QuotientGroup.lift`. Gegeben ein +Morphismus `α : G →* H` mit `N ≤ α.ker`, erhält man den induzierten Morphismus auf dem Quotienten: -/ @@ -126,7 +126,7 @@ theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G) ## Übungsaufgabe Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit -unter der Verknüpfung zu zeigen — prüfen Sie den +unter der Verknüpfung zu zeigen. Prüfen Sie den verschwiegenen Teil selbst nach: U·N ist auch abgeschlossen unter Inversen. Tipp: (u·n)⁻¹ = u⁻¹·(u·n⁻¹·u⁻¹), und der zweite Faktor liegt nach `conj_mem` in N. Ersetzen Sie das diff --git a/AlgebraInLean/Reciprocity.lean b/AlgebraInLean/Reciprocity.lean index 9c8c912..d52a95a 100644 --- a/AlgebraInLean/Reciprocity.lean +++ b/AlgebraInLean/Reciprocity.lean @@ -23,9 +23,9 @@ namespace AlgebraInLean `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 + `decide`: Aussagen über konkrete endliche Objekte sind + *entscheidbar*, etwa „ist 7 ein Quadrat in 𝔽₁₇?“. Lean + darf die Antwort also einfach ausrechnen. Das Ergebnis ist ein vollwertiger Beweis. ## Das Reziprozitätsgesetz @@ -37,11 +37,12 @@ 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`: +In Mathlib heißt der Satz `legendreSym.quadratic_reciprocity`. +Dort stehen die Exponenten als `p / 2`, was für ungerade p +dasselbe ist wie (p−1)/2. Dazu kommen die beiden +Ergänzungssätze. Der erste besagt, dass (−1/p) = 1 genau für +p ≡ 1 (mod 4) gilt; in der Quadrat-Formulierung ist er +`ZMod.exists_sq_eq_neg_one_iff`: -/ example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) : @@ -86,8 +87,8 @@ von Fermat bewiesen haben. 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 +Reziprozität und den Ergänzungssätzen). Lassen Sie dann +Lean Ihre Antwort bestätigen. Ersetzen Sie dazu das `sorry` durch einen Beweis. -/ diff --git a/AlgebraInLean/Transitivity.lean b/AlgebraInLean/Transitivity.lean index 940cb82..0b0bac1 100644 --- a/AlgebraInLean/Transitivity.lean +++ b/AlgebraInLean/Transitivity.lean @@ -19,10 +19,10 @@ Korollar 3.7.1 des Skripts: „Es seien L/K und M/L zwei algebraische Körpererweiterungen. Dann ist auch M/K algebraisch.“ -Der Kern des Skript-Beweises — adjungiere die endlich vielen -Koeffizienten des Minimalpolynoms, schließe auf Endlichkeit und -klettere mit der Gradformel den Turm hinauf — ist in Mathlib -das Lemma `isIntegral_trans`. Das Mathlib-Wörterbuch aus +Der Kern des Skript-Beweises ist in Mathlib das Lemma +`isIntegral_trans`: adjungiere die endlich vielen Koeffizienten +des Minimalpolynoms, schließe auf Endlichkeit und klettere mit +der Gradformel den Turm hinauf. Das Mathlib-Wörterbuch aus `AlgebraInLean/Elements.lean` gilt unverändert weiter. -/ diff --git a/Book.lean b/Book.lean index 0535880..319617d 100644 --- a/Book.lean +++ b/Book.lean @@ -14,6 +14,7 @@ import Book.Cauchy import Book.Frobenius import Book.Galois import Book.Reciprocity +import Book.Appendix open Verso.Genre Manual @@ -87,3 +88,5 @@ oder der ausführlichen Anleitung am Anfang der {include 0 Book.Galois} {include 0 Book.Reciprocity} + +{include 0 Book.Appendix} diff --git a/Book/Appendix.lean b/Book/Appendix.lean new file mode 100644 index 0000000..8aa51e3 --- /dev/null +++ b/Book/Appendix.lean @@ -0,0 +1,54 @@ +import VersoManual +import Manual.Meta + +set_option pp.rawOnError true +set_option verso.docstring.allowMissing true + +open Verso.Genre +open Verso.Genre.Manual.InlineLean + +#doc (Manual) "Anhang: Lizenz und Hinweise" => +%%% +htmlSplit := .never +tag := "anhang" +file := "anhang" +%%% + +Dieser Anhang sagt, unter welchen Bedingungen Sie diese Notizen +weiterverwenden dürfen, und wie sie entstanden sind. + +# Lizenz + +Diese Kursnotizen stehen, genau wie das begleitende Skript _Algebra +und Zahlentheorie_, unter der Lizenz +[Creative Commons Namensnennung 4.0 International (CC BY 4.0)](https://creativecommons.org/licenses/by/4.0/deed.de). + +Sie dürfen das Material also in jedem Format teilen und bearbeiten, +auch kommerziell, solange Sie angemessene Urheber- und Rechteangaben +machen, einen Link auf die Lizenz beifügen und angeben, ob Änderungen +vorgenommen wurden. Der vollständige Lizenztext liegt im Repository +in der Datei `LICENSE`. + +Der zitierte Lean-Code lebt von [Mathlib](https://github.com/leanprover-community/mathlib4), +das seinerseits unter der Apache-Lizenz 2.0 steht. Die Namen der +zitierten Lemmata und Definitionen gehören dorthin, nicht hierher. + +# Zur Entstehung: KI-Einsatz und Originalität + +Diese Notizen sind unter starkem Einsatz von KI-Werkzeugen (großen +Sprachmodellen) entstanden. Das gilt für die Lean-Beweise ebenso wie +für die deutsche Prosa: Beides wurde weitgehend maschinell entworfen +und von mir anschließend geprüft, korrigiert und überarbeitet. + +Ich erhebe daher *keinerlei Anspruch auf Originalität*. Die +Mathematik stammt aus der Vorlesung und ist Standardstoff; die +Beweisideen stammen aus dem Skript; die eigentliche Arbeit im Beweis +leisten die Lemmata aus Mathlib, die hier nur zusammengesetzt und +kommentiert werden. Der Beitrag dieser Notizen liegt allein in der +Auswahl und der Aufbereitung des Materials. + +Ein Trost bleibt: Sämtlicher Lean-Code in diesen Notizen wird beim +Bauen des Buches mitelaboriert. Die gezeigten Beweise sind also vom +Compiler geprüft, ganz gleich, wer oder was sie geschrieben hat. Für +die Prosa gilt das nicht — Fehler darin gehen zu meinen Lasten. +Hinweise darauf nehme ich gerne entgegen. diff --git a/Book/Basics.lean b/Book/Basics.lean index 4fe99ff..422d18d 100644 --- a/Book/Basics.lean +++ b/Book/Basics.lean @@ -64,7 +64,8 @@ die Axiome heißen `mul_assoc`, `one_mul`, `mul_one`, Ein Unterschied fällt auf: Das Skript _fordert_ die Eindeutigkeit von neutralem Element und Inversen, Mathlib nicht. Das ist kein -Widerspruch — die Eindeutigkeit folgt aus den übrigen Axiomen. Genau +Widerspruch, denn die Eindeutigkeit folgt aus den übrigen Axiomen. +Genau das beweisen wir jetzt, mit dem Standardargument aus der linearen Algebra: @@ -74,8 +75,8 @@ Algebra: $`e = e \cdot 1 = 1`. Der Lean-Beweis benutzt die Taktik `calc`, die eine Kette von -Gleichungen Schritt für Schritt abarbeitet — das Lean-Gegenstück zur -Gleichungskette am Ende des Textbeweises: +Gleichungen Schritt für Schritt abarbeitet; sie ist das +Lean-Gegenstück zur Gleichungskette am Ende des Textbeweises: ```lean theorem neutral_eindeutig {G : Type*} [Group G] (e : G) @@ -96,7 +97,7 @@ $$`b = 1 \cdot b = (a^{-1} \cdot a) \cdot b = a^{-1} \cdot (a \cdot b) = a^{-1} Öffnen Sie `AlgebraInLean/Basics.lean` und ersetzen Sie das `sorry` durch einen -Beweis — `calc` und die Lemmata `one_mul`, `inv_mul_cancel`, +Beweis. `calc` und die Lemmata `one_mul`, `inv_mul_cancel`, `mul_assoc`, `mul_one` genügen. ```lean diff --git a/Book/Cauchy.lean b/Book/Cauchy.lean index 0bea4a6..24e78b7 100644 --- a/Book/Cauchy.lean +++ b/Book/Cauchy.lean @@ -40,8 +40,8 @@ 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 äquivalent, nach dem - Satz von Cauchy unten!). Das Lemma `IsPGroup.of_card` übersetzt + $`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 @@ -54,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 +`IsPGroup.card_modEq_card_fixedPoints`. Wir zitieren hier also einfach die Bibliothek, so wie das Skript an dieser Stelle Satz 17.2.1 zitiert. @@ -82,7 +82,7 @@ gleich auf.) 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 +Gruppenwirkung. Diesmal gibt es also vor dem eigentlichen Satz echte Arbeit: Wir bauen erst die Menge und die Wirkung. ## Die Menge M @@ -91,8 +91,8 @@ Arbeit: Wir bauen erst die Menge und die Wirkung. $`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` — eine Liste der Länge $`p` —, und $`M` ist die -Menge `Equiv.Perm.vectorsProdEqOne G p` aller Vektoren, deren +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 @@ -120,9 +120,9 @@ Vertauschen wirken.“ Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p` um $`k` Stellen ist `VectorsProdEqOne.rotate v k`. Die Fußnote des -Skripts — der Shift bildet $`M` auf sich ab, „weil in jeder Gruppe -aus $`a \cdot b = e` auch $`b \cdot a = e` gilt“ — ist das -Mathlib-Lemma +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. @@ -131,8 +131,8 @@ 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ß +ab, dass der Shift nur von der Verschiebung _modulo p_ abhängt. +Genau deshalb wirkt $`\mathbb{Z}/(p)` und nicht bloß $`\mathbb{N}`. ```lean @@ -186,7 +186,7 @@ $`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` — das ist $`(a, \dots, a)` — ist. (Die +`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 @@ -322,7 +322,7 @@ 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 — +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 fd988e2..f26e923 100644 --- a/Book/Degrees.lean +++ b/Book/Degrees.lean @@ -28,7 +28,7 @@ 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 + `Algebra K L`-Instanz zwischen zwei Körpern. Damit wird $`L` insbesondere ein $`K`-Vektorraum, genau wie im Skript. * Eine Kette $`K \subseteq L \subseteq M` besteht aus drei @@ -38,9 +38,9 @@ und Körpererweiterungen als Vektorräume. * Der Grad $`[L:K]` heißt `Module.finrank K L`. Achtung, hier weicht die Konvention vom Skript ab: `finrank` hat Werte in $`\mathbb{N}`, - und unendlichdimensionale Erweiterungen bekommen den Wert 0 — wo + und unendlichdimensionale Erweiterungen bekommen den Wert 0. Wo das Skript in seiner Fußnote mit $`\infty` rechnet, rechnet Mathlib - mit 0. „$`[L:K]` ist endlich“ ist die Typklasse + also mit 0. „$`[L:K]` ist endlich“ ist die Typklasse `FiniteDimensional K L`. # Die Gradformel @@ -63,9 +63,10 @@ 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 +Die Behauptung zerfällt in die beiden Beweisschritte „Die Produkte +bilden ein Erzeugendensystem“ und „Die Produkte sind linear +unabhängig“. In Mathlib ist sie die Konstruktion +`Basis.smulTower`: Aus einer Basis $`\ell` von $`L/K` und einer Basis $`m` von $`M/L` baut sie die Basis $`(\ell_i \cdot m_j)` von $`M/K` (das Lemma `Basis.smulTower_apply` bestätigt, @@ -98,7 +99,7 @@ theorem gradformel (K L M : Type*) [Field K] [Field L] 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 — +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 $`μ_{ij}` aus dem Skript. @@ -112,7 +113,7 @@ Das erste Korollar des Skripts zur Gradformel: $`[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 := …` +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`. @@ -127,9 +128,9 @@ theorem grad_teilt (K L M : Type*) [Field K] [Field L] # Der vollständige Beweis -Der Beweis oben ist ehrlich, aber kurz: Die eigentliche Arbeit — -die Behauptung über die Produkte — haben wir bei `Basis.smulTower` -eingekauft. Zum Abschluss führen wir den Skript-Beweis selbst aus, +Der Beweis oben ist ehrlich, aber kurz: Die eigentliche Arbeit haben +wir bei `Basis.smulTower` eingekauft, nämlich die Behauptung über die +Produkte. Zum Abschluss führen wir den Skript-Beweis selbst aus, Satz für Satz. Die unendlichen Fälle entfallen wie zuvor, weil wir Endlichkeit voraussetzen. @@ -151,7 +152,7 @@ Der erste Schritt des Skripts: liefert $`m = \sum_{i,j} μ_{ij} \cdot (\ell_i \cdot m_j)`. In Lean heißen die Koeffizienten $`λ_j` und $`μ_{ij}` gerade -`m.repr x j` und `ℓ.repr (m.repr x j) i` — das „Schreibe … als +`m.repr x j` und `ℓ.repr (m.repr x j) i`. Das „Schreibe … als Linearkombination“ des Skripts ist das Lemma `Basis.sum_repr`. Das „Einsetzen“ ist eine kleine Rechnung mit dem Distributivgesetz `Finset.sum_smul` und der Turmbedingung `smul_assoc`, @@ -203,7 +204,7 @@ Der zweite Schritt: Das Lemma `Fintype.linearIndependent_iff` übersetzt „linear unabhängig“ in genau die Sprechweise des Skripts: Jede Relation hat -verschwindende Koeffizienten. Wir benutzen es dreimal — einmal in +verschwindende Koeffizienten. Wir benutzen es dreimal: einmal in jede Richtung für die Basen `m` und `ℓ`, und einmal für die zu beweisende Aussage selbst. @@ -252,8 +253,8 @@ Zum Schluss der Zusammenbau, wie im Skript angekündigt: als $`K`-Vektorraum bilden; damit ist dann sofort $`[M:K] = a \cdot b` gezeigt. -Die Konstruktion `Module.Basis.mk` baut aus unseren beiden Lemmata — -linear unabhängig und erzeugend — eine Basis; das „sofort gezeigt“ +Aus unseren beiden Lemmata (linear unabhängig, erzeugend) baut die +Konstruktion `Module.Basis.mk` eine Basis. Das „sofort gezeigt“ ist wieder das Abzählen der Indexmenge `Fin a × Fin b`. ```lean diff --git a/Book/Elements.lean b/Book/Elements.lean index bec85d0..d4c971e 100644 --- a/Book/Elements.lean +++ b/Book/Elements.lean @@ -31,15 +31,15 @@ Kapitel, die Transitivität der Algebraizität. * „$`a` ist algebraisch über $`K`“ heißt `IsAlgebraic K a`. Über Körpern ist das gleichbedeutend damit, dass $`a` Nullstelle - eines _normierten_ Polynoms ist — in Mathlib `IsIntegral K a` - („$`a` ist ganz über $`K`“). Die Umrechnungen heißen + eines _normierten_ Polynoms ist; in Mathlib heißt das + `IsIntegral K a` („$`a` ist ganz über $`K`“). Die Umrechnungen heißen `IsAlgebraic.isIntegral` und `IsIntegral.isAlgebraic`; die meisten Mathlib-Lemmata sind für `IsIntegral` formuliert. * Das Minimalpolynom heißt `minpoly K a`; der Grad $`[a:K]` des Skripts ist sein Grad `(minpoly K a).natDegree`. Für transzendentes $`a` setzt Mathlib `minpoly K a = 0`, und das - Nullpolynom hat `natDegree` 0 — wir treffen also wieder die + Nullpolynom hat `natDegree` 0. Damit treffen wir wieder die 0-Konvention für $`\infty` aus dem letzten Kapitel. * Der Zwischenkörper $`K(a)` heißt `K⟮a⟯`, kurz für @@ -47,9 +47,9 @@ Kapitel, die Transitivität der Algebraizität. durch `open IntermediateField` verfügbar; Vorsicht, `⟮…⟯` sind eigene Unicode-Zeichen, keine gewöhnlichen Klammern. -* „Die Erweiterung $`L/K` ist algebraisch“ — jedes Element von - $`L` ist algebraisch über $`K` — ist die Typklasse - `Algebra.IsAlgebraic K L`. Das elementweise Ausbuchstabieren +* „Die Erweiterung $`L/K` ist algebraisch“ ist die Typklasse + `Algebra.IsAlgebraic K L`; gemeint ist, dass jedes Element von + $`L` algebraisch über $`K` ist. Das elementweise Ausbuchstabieren übernimmt `Algebra.IsAlgebraic.isAlgebraic`. # Satz 3.5.4 @@ -73,14 +73,14 @@ Der Beweis im algebraischen Fall: Ich behaupte, dass $`V = K(a)` ist; damit ist dann $`[K(a):K] = \dim_K V = m` und der Satz ist bewiesen. … -Die Behauptung — mit den beiden Beweisschritten +Die Behauptung zerfällt in die beiden Beweisschritte „Abgeschlossenheit unter Multiplikation“ und „Abgeschlossenheit -unter Inversenbildung“ — ist in Mathlib die Konstruktion +unter Inversenbildung“. In Mathlib ist sie die Konstruktion `IntermediateField.adjoin.powerBasis`: Für ganzes $`a` baut sie aus den Potenzen $`1, a, …, a^{m-1}` eine Basis von `K⟮a⟯`, eine sogenannte _Potenzbasis_. Wie bei der Gradformel bleibt für uns -das Abzählen der Basis — und wie dort holen wir den vollständigen -Beweis am Ende des Kapitels nach. +das Abzählen der Basis; den vollständigen Beweis holen wir wie +dort am Ende des Kapitels nach. ```lean open IntermediateField @@ -99,8 +99,8 @@ theorem grad_element {K L : Type*} [Field K] [Field L] rfl ``` -Den transzendenten Fall — $`[a:K] = ∞ = [K(a):K]` — behandelt -das Skript mit den unendlichen Potenzen $`1, a, a^2, …`; in +Im transzendenten Fall gilt $`[a:K] = ∞ = [K(a):K]`. Das Skript +behandelt ihn mit den unendlichen Potenzen $`1, a, a^2, …`; in Mathlibs 0-Konvention steht auf beiden Seiten schlicht 0. Als fertiges Zitat heißt unser Satz übrigens `IntermediateField.adjoin.finrank`. @@ -132,9 +132,9 @@ theorem einfach_algebraisch {K L : Type*} [Field K] # Der vollständige Beweis -Oben haben wir die eigentliche Arbeit — die Potenzen bilden eine -Basis von $`K(a)` — bei `IntermediateField.adjoin.powerBasis` -eingekauft. Jetzt führen wir den Skript-Beweis Satz für Satz +Oben haben wir die eigentliche Arbeit bei +`IntermediateField.adjoin.powerBasis` eingekauft: dass die Potenzen +eine Basis von $`K(a)` bilden. Jetzt führen wir den Skript-Beweis Satz für Satz selbst aus. Er ist deutlich länger als der vollständige Beweis der Gradformel, denn das Skript zeigt hier wirklich etwas Substantielles: dass ein endlichdimensionaler Untervektorraum, @@ -159,7 +159,7 @@ noncomputable def potenzraum (K : Type*) {L : Type*} fun i : Fin (minpoly K a).natDegree => a ^ (i : ℕ)) ``` -Ein Argument benutzt das Skript zweimal — einmal für $`a`, später +Ein Argument benutzt das Skript zweimal: einmal für $`a`, später noch einmal für ein Element $`y ∈ V`: > Falls nicht, dann gäbe es eine Zahl $`m ∈ ℕ` und Elemente diff --git a/Book/Frobenius.lean b/Book/Frobenius.lean index 89e8a38..d00cbd0 100644 --- a/Book/Frobenius.lean +++ b/Book/Frobenius.lean @@ -21,8 +21,8 @@ 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`. +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 @@ -110,9 +110,9 @@ theorem frobenius_add {R : Type*} [CommRing R] (p : ℕ) 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: +`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`. @@ -120,7 +120,7 @@ $`p^n` Elementen. In Mathlib heißt er `GaloisField p n`. 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 +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. diff --git a/Book/Galois.lean b/Book/Galois.lean index 18cac08..4858ab3 100644 --- a/Book/Galois.lean +++ b/Book/Galois.lean @@ -23,8 +23,8 @@ 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. +Fixkörper-Konstruktion. Deren Beweis ist im Skript eine +„Hausaufgabe“ und bleibt es auch hier. # Das Mathlib-Wörterbuch @@ -32,7 +32,7 @@ ist und es auch hier bleibt. `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 +* „$`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 @@ -51,7 +51,7 @@ Satz und Definition 16.1.1 des Skripts: eine Hausaufgabe. Wir definieren die Menge in Lean und beweisen exemplarisch die -Abgeschlossenheit unter der Multiplikation — der Rest der Hausaufgabe +Abgeschlossenheit unter der Multiplikation. Der Rest der Hausaufgabe ist, wie im Skript, Ihre Übungsaufgabe. ```lean @@ -107,8 +107,8 @@ example (K L : Type*) [Field K] [Field L] [Algebra 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 +dass `Fix G` ein Unterkörper ist, also die 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. diff --git a/Book/Ideals.lean b/Book/Ideals.lean index bf602bc..6294a51 100644 --- a/Book/Ideals.lean +++ b/Book/Ideals.lean @@ -22,9 +22,9 @@ file := "ideale" %%% Dieses Kapitel übersetzt den Satz „ℤ ist ein Hauptidealring“ aus -Kapitel 9 des Skripts — der klassische Beweis über Division mit Rest, -und zugleich unsere erste Begegnung mit dem Wohlordnungsprinzip in -Lean. +Kapitel 9 des Skripts. Es ist der klassische Beweis über Division +mit Rest und zugleich unsere erste Begegnung mit dem +Wohlordnungsprinzip in Lean. # Das Mathlib-Wörterbuch @@ -62,7 +62,7 @@ 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` 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 diff --git a/Book/LittleFermat.lean b/Book/LittleFermat.lean index 1392101..4ab5695 100644 --- a/Book/LittleFermat.lean +++ b/Book/LittleFermat.lean @@ -36,9 +36,9 @@ deutsche Original, Aussage und Beweis: $`\overline{a}^{p-1} = 1 \in \mathbb{F}_p^*`, oder äquivalent $`a^p \equiv a \pmod{p}`. ∎ -Fünf Sätze. Unser Ziel ist ein Lean-Beweis mit genau dieser Struktur — -jeder deutsche Satz kehrt als Kommentar über dem Lean-Code wieder, der -ihn umsetzt. +Fünf Sätze. Unser Ziel ist ein Lean-Beweis mit genau dieser +Struktur: Jeder deutsche Satz kehrt als Kommentar über dem Lean-Code +wieder, der ihn umsetzt. # Das Mathlib-Wörterbuch @@ -46,7 +46,7 @@ Bevor wir den Satz überhaupt formulieren können, müssen wir wissen, wie Mathlib über die beteiligten Objekte spricht. * Der Restklassenring $`\mathbb{Z}/(p)` heißt `ZMod p`. Die - Restklasse einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)` — + Restklasse einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)`; Lean fügt den kanonischen Ringmorphismus $`\mathbb{Z} \to \mathbb{Z}/(p)` automatisch ein (eine _Koerzion_). @@ -60,7 +60,7 @@ Mathlib über die beteiligten Objekte spricht. * Das Skript sagt „es sei $`p` eine Primzahl“. In Lean führen wir die Primalität von `p` als Hypothese `hp : p.Prime` mit. Manche - Tatsachen — etwa dass $`\mathbb{Z}/(p)` ein Körper ist — findet + Tatsachen, etwa dass $`\mathbb{Z}/(p)` ein Körper ist, findet Leans Automatisierung nur, wenn die Hypothese als _Instanz_ registriert ist; genau das leistet die erste Beweiszeile `have : Fact p.Prime := ⟨hp⟩`. @@ -141,7 +141,7 @@ example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a := Das ist die Bemerkung nach dem Satz im Skript: In Anwendungen verwendet man häufig die äquivalente Formulierung $`a^{p-1} \equiv 1 \pmod{p}` für nicht durch $`p` teilbare $`a`. Leiten Sie -sie aus `little_fermat` ab — oder geben Sie einen direkten Beweis nach +sie aus `little_fermat` ab, oder geben Sie einen direkten Beweis nach den Ideen oben. Öffnen Sie `AlgebraInLean/LittleFermat.lean` im Übungs-Repository und ersetzen Sie das `sorry` durch einen Beweis. diff --git a/Book/Polynomials.lean b/Book/Polynomials.lean index cd4dc80..074d6a6 100644 --- a/Book/Polynomials.lean +++ b/Book/Polynomials.lean @@ -31,7 +31,7 @@ Polynom-API kennen. `X ^ 3 - C 2`. * Der k-te Koeffizient ist `f.coeff k`, der Grad `f.degree`. - Achtung: `degree` hat Werte in `WithBot ℕ` — das Nullpolynom + Achtung: `degree` hat Werte in `WithBot ℕ`; das Nullpolynom bekommt den Grad `⊥` („minus unendlich“, wie im Skript). Daneben gibt es `f.natDegree : ℕ`. @@ -55,7 +55,7 @@ Satz 7.2.1 des Skripts: In Mathlib heißt der Satz `Polynomial.irreducible_of_eisenstein_criterion`. Er ist dort über -ein Primideal `P` statt eines Primelements $`p` formuliert — für uns +ein Primideal `P` statt eines Primelements $`p` formuliert. Für uns ist `P` das Hauptideal $`(p)` aus dem letzten Kapitel, und „$`p` teilt $`a_k`“ wird zu `f.coeff k ∈ Ideal.span {p}`. Statt „$`p \nmid a_n`“ (was im Skript aus $`\operatorname{ggT} = 1` folgt) @@ -68,7 +68,7 @@ verlangt Mathlib direkt `f.leadingCoeff ∉ P`. ist. Das Skript lässt die Kontrolle der Eisenstein-Bedingungen als -Kopfrechnung weg — in Lean führen wir sie aus und lernen dabei die +Kopfrechnung weg. In Lean führen wir sie aus und lernen dabei die Koeffizienten-API kennen: `coeff_sub`, `coeff_X_pow` und `coeff_C` berechnen die Koeffizienten von $`x^n - r`, nämlich $`a_n = 1`, $`a_0 = -r` und $`a_k = 0` sonst. @@ -95,7 +95,7 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ) · rw [hmonic.leadingCoeff, Ideal.mem_span_singleton] exact fun h => hprime.not_isUnit (isUnit_of_dvd_one h) -- „p|a₀, …, p|a_{n−1}“: Unterhalb von Grad n sind die - -- Koeffizienten −r (bei k = 0) und 0 (sonst) — beide + -- Koeffizienten −r (bei k = 0) und 0 (sonst), beide -- durch p teilbar. · intro k hk have hkn : k < n := by @@ -125,9 +125,9 @@ 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 in Mathlib (Datei `Mathlib.RingTheory.Polynomial.GaussLemma`). Das -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. +zweite Beispiel des Skripts greifen wir im Kapitel über +Körpererweiterungen wieder auf: $`x^n - p` ist irreduzibel und +deshalb das Minimalpolynom von $`\sqrt[n]{p}`. # Übungsaufgabe @@ -138,7 +138,7 @@ Genau dieses zweite Beispiel ist die Übung: Wenden Sie `xn_sub_r_irreduzibel` mit `r = p` an. Zu zeigen bleibt $`p^2 \nmid p`: Aus $`p = p^2 \cdot c` folgt durch Kürzen -$`1 = p \cdot c` — dann wäre $`p` eine Einheit, im Widerspruch zur +$`1 = p \cdot c`; dann wäre $`p` eine Einheit, im Widerspruch zur Primalität. Nützlich sind `mul_left_cancel₀`, `isUnit_of_dvd_one` und `Prime.not_isUnit`. Öffnen Sie `AlgebraInLean/Polynomials.lean` und ersetzen Sie das diff --git a/Book/Quotients.lean b/Book/Quotients.lean index aa090a9..c9b2e19 100644 --- a/Book/Quotients.lean +++ b/Book/Quotients.lean @@ -33,7 +33,7 @@ $`U \cdot N` für normales $`N` wieder eine Untergruppe ist. Mitgliedschaft schreibt sich `g ∈ U`. Dass `U` unter Verknüpfung und Inversen abgeschlossen ist, sagen `U.mul_mem` und `U.inv_mem`. -* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein „Bündel“ aus +* Ein Gruppenmorphismus ist ein Term `φ : G →* Q`, ein „Bündel“ aus der Abbildung und den Nachweisen `map_mul : φ (a·b) = φ a · φ b` (daraus folgen `map_one` und `map_inv`). Der Kern heißt `φ.ker`; die Mitgliedschaft entpackt @@ -74,7 +74,7 @@ Mathlib kennt diese Aussage als Instanz `MonoidHom.normal_ker : φ.ker.Normal`. Das Skript fährt fort: Untergruppen mit dieser Eigenschaft heißen _normale Untergruppen_ oder _Normalteiler_, und die Bedingung ist nicht nur notwendig, -sondern auch hinreichend — zu jedem Normalteiler existiert eine +sondern auch hinreichend: Zu jedem Normalteiler existiert eine Restklassengruppe. # Die Restklassengruppe und ihre universelle Eigenschaft @@ -83,8 +83,8 @@ Das Skript definiert die Restklassengruppe in Kapitel 17.3 über ihre universelle Eigenschaft. Mathlib stellt beides bereit: den Quotienten `G ⧸ N` mit der Quotientenabbildung `QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle Eigenschaft -als `QuotientGroup.lift` — gegeben ein Morphismus `α : G →* H` mit -`N ≤ α.ker` erhält man den induzierten Morphismus auf dem +als `QuotientGroup.lift`. Gegeben ein Morphismus `α : G →* H` mit +`N ≤ α.ker`, erhält man den induzierten Morphismus auf dem Quotienten: ```lean @@ -139,7 +139,7 @@ theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G) # Übungsaufgabe Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit unter der -Verknüpfung zu zeigen — prüfen Sie den verschwiegenen Teil selbst +Verknüpfung zu zeigen. Prüfen Sie den verschwiegenen Teil selbst nach: $`U \cdot N` ist auch abgeschlossen unter Inversen. Tipp: $`(u \cdot n)^{-1} = u^{-1} \cdot (u \cdot n^{-1} \cdot u^{-1})`, und der zweite Faktor liegt nach `conj_mem` in $`N`. Öffnen Sie `AlgebraInLean/Quotients.lean` und diff --git a/Book/Reciprocity.lean b/Book/Reciprocity.lean index 66f8c6a..8907454 100644 --- a/Book/Reciprocity.lean +++ b/Book/Reciprocity.lean @@ -32,9 +32,9 @@ schließt den Kreis zum Anfang des Kurses. `IsSquare (a : ZMod p)`. * Das Lean-Lernthema dieses Kapitels ist die Taktik `decide`: - Aussagen über konkrete endliche Objekte — „ist 7 ein Quadrat in - $`\mathbb{F}_{17}`?“ — sind _entscheidbar_, und Lean darf die - Antwort einfach ausrechnen. Das Ergebnis ist ein vollwertiger + Aussagen über konkrete endliche Objekte sind _entscheidbar_, etwa + „ist 7 ein Quadrat in $`\mathbb{F}_{17}`?“. Lean darf die Antwort + also einfach ausrechnen. Das Ergebnis ist ein vollwertiger Beweis. # Das Reziprozitätsgesetz @@ -46,12 +46,12 @@ Satz 24.2.1 des Skripts: die Gleichung $`\left(\tfrac{p}{q}\right) \cdot \left(\tfrac{q}{p}\right) = (-1)^{\frac{p-1}{2} \cdot \frac{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 — -$`\left(\tfrac{-1}{p}\right) = 1` genau für -$`p \equiv 1 \pmod{4}` — ist in der -Quadrat-Formulierung `ZMod.exists_sq_eq_neg_one_iff`: +In Mathlib heißt der Satz `legendreSym.quadratic_reciprocity`. Dort +stehen die Exponenten als `p / 2`, was für ungerade $`p` dasselbe ist +wie $`(p-1)/2`. Dazu kommen die beiden Ergänzungssätze. Der erste +besagt, dass $`\left(\tfrac{-1}{p}\right) = 1` genau für +$`p \equiv 1 \pmod{4}` gilt; in der Quadrat-Formulierung ist er +`ZMod.exists_sq_eq_neg_one_iff`: ```lean example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) : @@ -95,7 +95,7 @@ im Kapitel über den kleinen Satz von Fermat gerechnet haben. 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. +Ergänzungssätzen). Lassen Sie dann Lean Ihre Antwort bestätigen. Öffnen Sie `AlgebraInLean/Reciprocity.lean` und ersetzen Sie das `sorry` durch einen Beweis. diff --git a/Book/Transitivity.lean b/Book/Transitivity.lean index f8d6496..b44b15e 100644 --- a/Book/Transitivity.lean +++ b/Book/Transitivity.lean @@ -48,10 +48,10 @@ gilt unverändert weiter. die Erweiterung $`Z(m)/K` algebraisch; insbesondere ist das Element $`m ∈ Z(m)` algebraisch über $`K`. -Genau dieses Argument — adjungiere die endlich vielen -Koeffizienten des Minimalpolynoms, schließe auf Endlichkeit und -klettere mit der Gradformel den Turm hinauf — steckt in Mathlib -im Lemma `isIntegral_trans`. Unser Beweis übersetzt die +Genau dieses Argument steckt in Mathlib im Lemma +`isIntegral_trans`: adjungiere die endlich vielen Koeffizienten +des Minimalpolynoms, schließe auf Endlichkeit und klettere mit +der Gradformel den Turm hinauf. Unser Beweis übersetzt die Rahmensätze des Skripts und zitiert für den Kern dieses Lemma; der letzte Abschnitt des Kapitels führt auch diesen Beweis Satz für Satz aus: @@ -89,7 +89,7 @@ Das Skript warnt an dieser Stelle: keiner Prüfung funktioniert. Lassen Sie das! Die Warnung gilt wortgleich in Lean: Auch Mathlib konstruiert -nirgendwo ein Minimalpolynom von $`m` über $`K` — der Beweis von +nirgendwo ein Minimalpolynom von $`m` über $`K`. Der Beweis von `isIntegral_trans` läuft über die Endlichkeit von Moduln, nicht über explizite Polynome. @@ -100,8 +100,8 @@ nirgendwo ein Minimalpolynom von $`m` über $`K` — der Beweis von Koeffizienten des Minimalpolynoms erzeugte Unteralgebra gebildet (das $`Z` des Skripts), ihre Endlichkeit als Modul gezeigt, und am Ende die Endlichkeit längs des Turms - komponiert — `Module.Finite.trans`, die Gradformel in der - Gestalt „endlich über endlich ist endlich“. + komponiert, und zwar mit `Module.Finite.trans`, der Gradformel + in der Gestalt „endlich über endlich ist endlich“. 2. Als fertiges Zitat ist die Transitivität in Mathlib die Instanz `Algebra.IsAlgebraic.trans K L M` — eine Zeile. @@ -134,7 +134,7 @@ theorem algebraisch_quadrat {K L : Type*} [Field K] # Der vollständige Beweis Zum Schluss der Skript-Beweis der Transitivität, ohne das Zitat -von `isIntegral_trans` — die Kette $`K ⊆ Z ⊆ Z(m) ∋ m` wird +von `isIntegral_trans`: die Kette $`K ⊆ Z ⊆ Z(m) ∋ m` wird wörtlich nachgebaut. Das komplette Skript-Zitat steht oben; im Beweis stehen die Sätze wie immer als Kommentare. Drei Übersetzungsentscheidungen vorweg: @@ -237,7 +237,7 @@ theorem transitivitaet_vollstaendig (K L M : Type*) Zwei Details verdienen einen zweiten Blick. Erstens: `Z⟮x⟯` ist eine Erweiterung von $`Z`, aber die Aussage „$`Z(m)/K` ist -algebraisch“ braucht $`Z(m)` als Erweiterung von $`K` — diesen +algebraisch“ braucht $`Z(m)` als Erweiterung von $`K`. Diesen stillschweigenden Wechsel des Grundkörpers, den das Skript gar nicht erwähnt, macht `restrictScalars K` explizit. Zweitens steckt im Schritt „$`f ∈ Z[x]` hat $`m` als Nullstelle, also ist diff --git a/README.md b/README.md index b6b9d3b..22a67a5 100644 --- a/README.md +++ b/README.md @@ -65,4 +65,7 @@ server as for the lecture notes. ## License -CC-BY 4.0, like the lecture notes. +CC-BY 4.0, like the lecture notes; see `LICENSE`. The book contains an +appendix (`Book/Appendix.lean`) restating the license and disclosing +that these notes were produced with heavy use of AI tools, with no +claim to originality.