From 06f12adfa90e3bffbac9cf4e51229b404f623d2b Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 12 Aug 2026 17:05:26 +0200 Subject: [PATCH] Adding material --- AlgebraInLean.lean | 1 + AlgebraInLean/Elements.lean | 112 +++++++++++++++++++ Book.lean | 3 + Book/Degrees.lean | 26 ++--- Book/Elements.lean | 209 ++++++++++++++++++++++++++++++++++++ 5 files changed, 339 insertions(+), 12 deletions(-) create mode 100644 AlgebraInLean/Elements.lean create mode 100644 Book/Elements.lean diff --git a/AlgebraInLean.lean b/AlgebraInLean.lean index f0c6583..2f0f575 100644 --- a/AlgebraInLean.lean +++ b/AlgebraInLean.lean @@ -4,6 +4,7 @@ import AlgebraInLean.Quotients import AlgebraInLean.Ideals import AlgebraInLean.Polynomials import AlgebraInLean.Degrees +import AlgebraInLean.Elements import AlgebraInLean.LittleFermat import AlgebraInLean.Cauchy import AlgebraInLean.Frobenius diff --git a/AlgebraInLean/Elements.lean b/AlgebraInLean/Elements.lean new file mode 100644 index 0000000..fd7522f --- /dev/null +++ b/AlgebraInLean/Elements.lean @@ -0,0 +1,112 @@ +/- +Algebra in Lean — Kapitel 3 des Skripts +======================================= + +Diese Datei begleitet das Skript „Algebra und Zahlentheorie“ +(Stefan Kebekus, CC-BY 4.0). Sie übersetzt den Satz über den +Grad eines Elements (satz:3-5-4) und die Transitivität der +Algebraizität (kor:TdA) nach Lean. +-/ +import Mathlib + +namespace AlgebraInLean + +open IntermediateField + +/-! +# Algebraische Elemente und Transitivität + +## Das Mathlib-Wörterbuch + +* „a ist algebraisch über K“ heißt `IsAlgebraic K a`. Über + Körpern gleichbedeutend: a ist Nullstelle eines normierten + Polynoms, in Mathlib `IsIntegral K a` („a ist ganz über K“). + Umrechnungen: `IsAlgebraic.isIntegral` und + `IsIntegral.isAlgebraic`. + +* 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 ∞. + +* Der Zwischenkörper K(a) heißt `K⟮a⟯`, kurz für + `IntermediateField.adjoin K {a}`; die Notation kommt mit + `open IntermediateField`. + +* „L/K ist algebraisch“ ist die Typklasse + `Algebra.IsAlgebraic K L`. + +## Der Grad eines Elements + +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 +`IntermediateField.adjoin.powerBasis`. +-/ + +theorem grad_element {K L : Type*} [Field K] [Field L] + [Algebra K L] {a : L} (ha : IsIntegral K a) : + Module.finrank K K⟮a⟯ = (minpoly K a).natDegree := by + -- „Betrachte deshalb den m-dimensionalen Untervektorraum + -- V := ⟨1, a, a², …, a^{m-1}⟩ ⊆ K(a). Ich behaupte, + -- dass V = K(a) ist …“ — die Potenzbasis von K⟮a⟯: + let pb := IntermediateField.adjoin.powerBasis ha + -- „… damit ist dann [K(a):K] = dim_K V = m und der Satz + -- ist bewiesen.“ + rw [Module.finrank_eq_card_basis pb.basis, + Fintype.card_fin] + rfl + +/-! +## Die Transitivität der Algebraizität + +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`. +-/ + +theorem transitivitaet (K L M : Type*) [Field K] [Field L] + [Field M] [Algebra K L] [Algebra L M] [Algebra K M] + [IsScalarTower K L M] + [Algebra.IsAlgebraic K L] [Algebra.IsAlgebraic L M] : + Algebra.IsAlgebraic K M := by + constructor + -- „Es sei ein Element m ∈ M gegeben.“ + intro m + -- „Wir wissen, dass m algebraisch über L ist“ — über + -- Körpern gleichbedeutend: m ist ganz über L. + have hm : IsIntegral L m := + (Algebra.IsAlgebraic.isAlgebraic m).isIntegral + -- Ebenso ist die algebraische Erweiterung L/K ganz. + have : Algebra.IsIntegral K L := + Algebra.IsAlgebraic.isIntegral + -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1}) und + -- die Kette K ⊆ Z ⊆ Z(m) ∋ m …“ — der gesamte Rest + -- des Skript-Beweises ist das Lemma isIntegral_trans. + exact (isIntegral_trans m hm).isAlgebraic + +/-! +## Übungsaufgabe + +Aus dem Skript: „Die Menge der über K algebraischen Elemente +von L bildet einen Unterkörper von L, genannt der algebraische +Abschluss von K im Oberkörper L.“ Die einzelnen +Abgeschlossenheiten kennt Mathlib als `IsIntegral.add`, +`IsIntegral.neg`, `IsIntegral.mul`, `IsIntegral.pow` und +`IsIntegral.inv`. Die Übung: Kombinieren Sie sie und ersetzen +Sie das `sorry` durch einen Beweis. +-/ + +theorem algebraisch_quadrat {K L : Type*} [Field K] + [Field L] [Algebra K L] {a : L} + (ha : IsIntegral K a) : + IsIntegral K (a ^ 2 + a) := by + sorry + +end AlgebraInLean diff --git a/Book.lean b/Book.lean index fb72c6e..6029e00 100644 --- a/Book.lean +++ b/Book.lean @@ -7,6 +7,7 @@ import Book.Quotients import Book.Ideals import Book.Polynomials import Book.Degrees +import Book.Elements import Book.LittleFermat import Book.Cauchy import Book.Frobenius @@ -72,6 +73,8 @@ oder der ausführlichen Anleitung am Anfang der {include 0 Book.Degrees} +{include 0 Book.Elements} + {include 0 Book.LittleFermat} {include 0 Book.Cauchy} diff --git a/Book/Degrees.lean b/Book/Degrees.lean index c272066..1953fde 100644 --- a/Book/Degrees.lean +++ b/Book/Degrees.lean @@ -158,19 +158,20 @@ Linearkombination“ des Skripts ist das Lemma `Basis.sum_repr`. Das $`(μ \cdot \ell) \cdot m = μ \cdot (\ell \cdot m)`. ```lean -theorem produkte_erzeugen {K L M : Type*} [Field K] [Field L] - [Field M] [Algebra K L] [Algebra L M] [Algebra K M] - [IsScalarTower K L M] {a b : ℕ} +theorem produkte_erzeugen {K L M : Type*} [Field K] + [Field L] [Field M] [Algebra K L] [Algebra L M] + [Algebra K M] [IsScalarTower K L M] {a b : ℕ} (ℓ : Module.Basis (Fin a) K L) (m : Module.Basis (Fin b) L M) : ⊤ ≤ Submodule.span K - (Set.range fun p : Fin a × Fin b => ℓ p.1 • m p.2) := by + (Set.range + fun p : Fin a × Fin b => ℓ p.1 • m p.2) := by -- „Es sei ein Element m ∈ M gegeben.“ intro x _ - -- „Schreibe m als L-Linearkombination der Basis m₁, …, m_b, - -- und schreibe danach jeden der Koeffizienten λⱼ als - -- K-Linearkombination der Basis ℓ₁, …, ℓ_a. Einsetzen - -- liefert m = ∑ μᵢⱼ·(ℓᵢ·mⱼ).“ + -- „Schreibe m als L-Linearkombination der Basis + -- m₁, …, m_b, und schreibe danach jeden der + -- Koeffizienten λⱼ als K-Linearkombination der Basis + -- ℓ₁, …, ℓ_a. Einsetzen liefert m = ∑ μᵢⱼ·(ℓᵢ·mⱼ).“ have einsetzen : x = ∑ j, ∑ i, ℓ.repr (m.repr x j) i • (ℓ i • m j) := by conv_lhs => rw [← m.sum_repr x] @@ -178,7 +179,8 @@ theorem produkte_erzeugen {K L M : Type*} [Field K] [Field L] conv_lhs => rw [← ℓ.sum_repr (m.repr x j)] rw [Finset.sum_smul] exact Finset.sum_congr rfl fun i _ => smul_assoc .. - -- Eine K-Linearkombination der Produkte liegt im Erzeugnis. + -- Eine K-Linearkombination der Produkte liegt im + -- Erzeugnis. rw [einsetzen] exact Submodule.sum_mem _ fun j _ => Submodule.sum_mem _ fun i _ => @@ -206,9 +208,9 @@ jede Richtung für die Basen `m` und `ℓ`, und einmal für die zu beweisende Aussage selbst. ```lean -theorem produkte_unabhaengig {K L M : Type*} [Field K] [Field L] - [Field M] [Algebra K L] [Algebra L M] [Algebra K M] - [IsScalarTower K L M] {a b : ℕ} +theorem produkte_unabhaengig {K L M : Type*} [Field K] + [Field L] [Field M] [Algebra K L] [Algebra L M] + [Algebra K M] [IsScalarTower K L M] {a b : ℕ} (ℓ : Module.Basis (Fin a) K L) (m : Module.Basis (Fin b) L M) : LinearIndependent K diff --git a/Book/Elements.lean b/Book/Elements.lean new file mode 100644 index 0000000..ea92e21 --- /dev/null +++ b/Book/Elements.lean @@ -0,0 +1,209 @@ +import VersoManual +import Manual.Meta +-- Minimal-Imports statt `import Mathlib`, ermittelt mit +-- `#min_imports`. +import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic +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) "Algebraische Elemente und Transitivität" => +%%% +htmlSplit := .never +tag := "elemente" +file := "elemente" +%%% + +Dieses Kapitel übersetzt zwei weitere Resultate aus Kapitel 3 des +Skripts nach Lean: den Satz über den Grad einer einfachen +algebraischen Erweiterung, $`[a:K] = [K(a):K]`, und die +Transitivität der Algebraizität. Beide bauen auf der Gradformel +aus dem letzten Kapitel auf. + +# Das Mathlib-Wörterbuch + +* „$`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 + `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 + 0-Konvention für $`\infty` aus dem letzten Kapitel. + +* Der Zwischenkörper $`K(a)` heißt `K⟮a⟯`, kurz für + `IntermediateField.adjoin K {a}`. Die Klammer-Notation wird + 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 + übernimmt `Algebra.IsAlgebraic.isAlgebraic`. + +# Der Grad eines Elements + +Satz 3.5.4 des Skripts verbindet den Grad eines Elements mit dem +Grad der von ihm erzeugten Körpererweiterung: + +> *Satz 3.5.4 (Grad von Körpererweiterungen und Grad von + Elementen).* Es sei $`L/K` eine Körpererweiterung und es sei + $`a ∈ L`. Dann gilt die Gleichheit $`[a:K] = [K(a):K]`. + +Der Beweis im algebraischen Fall: + +> _Beweis von Satz 3.5.4, falls $`a` algebraisch ist._ Setze + $`m := [a:K]` und schreibe das Minimalpolynom von $`a` über + $`K` als $`f(x) = λ_0 + λ_1 x + ⋯ + λ_{m-1} x^{m-1} + x^m`. + Die Menge $`\{1, a, a^2, …, a^{m-1}\} ⊆ K(a)` ist linear + unabhängig über $`K` … Betrachte deshalb den + $`m`-dimensionalen Untervektorraum + $`V := \langle 1, a, a^2, …, a^{m-1} \rangle_K ⊆ K(a)`. + 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 +„Abgeschlossenheit unter Multiplikation“ und „Abgeschlossenheit +unter Inversenbildung“ — ist in Mathlib 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. + +```lean +open IntermediateField + +theorem grad_element {K L : Type*} [Field K] [Field L] + [Algebra K L] {a : L} (ha : IsIntegral K a) : + Module.finrank K K⟮a⟯ = (minpoly K a).natDegree := by + -- „Betrachte deshalb den m-dimensionalen Untervektorraum + -- V := ⟨1, a, a², …, a^{m-1}⟩ ⊆ K(a). Ich behaupte, + -- dass V = K(a) ist …“ — die Potenzbasis von K⟮a⟯: + let pb := IntermediateField.adjoin.powerBasis ha + -- „… damit ist dann [K(a):K] = dim_K V = m und der Satz + -- ist bewiesen.“ + rw [Module.finrank_eq_card_basis pb.basis, + Fintype.card_fin] + rfl +``` + +Den transzendenten Fall — $`[a:K] = ∞ = [K(a):K]` — behandelt +das Skript 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`. + +# Die Transitivität der Algebraizität + +Das Hauptresultat von Kapitel 3 des Skripts: + +> *Korollar 3.7.1 (Transitivität der Algebraizität).* Es seien + $`L/K` und $`M/L` zwei algebraische Körpererweiterungen. Dann + ist auch $`M/K` algebraisch. + +> _Beweis._ Es sei ein Element $`m ∈ M` gegeben. Wir wissen, + dass $`m` algebraisch über $`L` ist; es sei + $`f(x) = λ_0 + λ_1 x + ⋯ + λ_{n-1} x^{n-1} + x^n` das + Minimalpolynom von $`m` über $`L`. Die Koeffizienten $`λ_i` + liegen in $`L`. Betrachte jetzt den Körper + $`Z := K(λ_0, …, λ_{n-1})` und die Kette von + Körpererweiterungen $`K ⊆ Z ⊆ Z(m) ∋ m`. Die Erweiterung + $`L/K` ist algebraisch, also sind die endlich vielen Elemente + $`λ_0, …, λ_{n-1}` allesamt algebraisch über $`K`; deshalb ist + $`[Z:K] < ∞`. Weiter liegt das Polynom $`f` in $`Z[x]` und + hat $`m` als Nullstelle. Also ist $`m` auch algebraisch über + $`Z`, und Satz 3.5.4 liefert $`[Z(m):Z] < ∞`. Mit der + Gradformel folgt $`[Z(m):K] = [Z(m):Z]·[Z:K] < ∞`. Also ist + 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 +Rahmensätze des Skripts und zitiert für den Kern dieses Lemma: + +```lean +theorem transitivitaet (K L M : Type*) [Field K] [Field L] + [Field M] [Algebra K L] [Algebra L M] [Algebra K M] + [IsScalarTower K L M] + [Algebra.IsAlgebraic K L] [Algebra.IsAlgebraic L M] : + Algebra.IsAlgebraic K M := by + constructor + -- „Es sei ein Element m ∈ M gegeben.“ + intro m + -- „Wir wissen, dass m algebraisch über L ist“ — über + -- Körpern gleichbedeutend: m ist ganz über L. + have hm : IsIntegral L m := + (Algebra.IsAlgebraic.isAlgebraic m).isIntegral + -- Ebenso ist die algebraische Erweiterung L/K ganz. + have : Algebra.IsIntegral K L := + Algebra.IsAlgebraic.isIntegral + -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1}) und + -- die Kette K ⊆ Z ⊆ Z(m) ∋ m …“ — der gesamte Rest + -- des Skript-Beweises ist das Lemma isIntegral_trans. + exact (isIntegral_trans m hm).isAlgebraic +``` + +Das Skript warnt an dieser Stelle: + +> *Warnung (Prüfungsfalle).* Der Satz über die Transitivität der + Algebraizität wird in Prüfungen sehr gern gefragt. Beachten + Sie, dass der Beweis ziemlich indirekt ist. In Prüfungen + sehen wir oft, dass Kandidatinnen und Kandidaten für ein + gegebenes $`a ∈ M` direkt ein Minimalpolynom konstruieren + wollen. Das hat in der Geschichte der Mathematik noch in + 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 +`isIntegral_trans` läuft über die Endlichkeit von Moduln, nicht +über explizite Polynome. + +# Bemerkungen + +1. Wer in den Beweis von `isIntegral_trans` hineinschaut, findet + die Schritte des Skripts wieder: Dort wird die von den + 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“. + +2. Als fertiges Zitat ist die Transitivität in Mathlib die + Instanz `Algebra.IsAlgebraic.trans K L M` — eine Zeile. + +# Übungsaufgabe + +Das Skript zieht aus der Transitivität eine schöne Folgerung: + +> *Satz und Definition (Algebraischer Abschluss in einem + Oberkörper).* Es sei $`L/K` eine Körpererweiterung. Dann + bildet die Menge + $`\overline{K} := \{ a ∈ L : a \text{ ist algebraisch über } K \}` + einen Unterkörper von $`L`, genannt der _algebraische + Abschluss von $`K` im Oberkörper $`L`_. + +Die einzelnen Abgeschlossenheiten kennt Mathlib als +`IsIntegral.add`, `IsIntegral.neg`, `IsIntegral.mul`, +`IsIntegral.pow` und `IsIntegral.inv`. Die Übung: Kombinieren +Sie sie. Öffnen Sie `AlgebraInLean/Elements.lean` und ersetzen +Sie das `sorry` durch einen Beweis. + +```lean +theorem algebraisch_quadrat {K L : Type*} [Field K] + [Field L] [Algebra K L] {a : L} + (ha : IsIntegral K a) : + IsIntegral K (a ^ 2 + a) := by + sorry +```