6.1. 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 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. 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 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“ 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.

6.2. Satz 3.5.4🔗

Der Satz 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 zerfällt in die beiden Beweisschritte „Abgeschlossenheit unter Multiplikation“ und „Abgeschlossenheit 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; den vollständigen Beweis holen wir wie dort am Ende des Kapitels nach.

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.

6.3. Übungsaufgabe🔗

Das erste Korollar des Skripts zu Satz 3.5.4:

Es sei L/K eine Körpererweiterung und es sei a ∈ L. Falls [a:K] < ∞ ist, dann ist K(a) algebraisch über K.

Die beiden Zutaten kennt Mathlib als IntermediateField.adjoin.finiteDimensional („der Grad ist endlich“) und Algebra.IsAlgebraic.of_finite („endliche Erweiterungen sind algebraisch“). Beachten Sie, dass die Endlichkeit mit have := … in den Kontext geholt werden muss, damit die Instanzsuche sie sieht. Öffnen Sie AlgebraInLean/Elements.lean und ersetzen Sie das sorry durch einen Beweis.

6.4. Der vollständige Beweis🔗

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, der unter Multiplikation abgeschlossen ist, automatisch auch Inverse enthält.

Die Hauptfigur ist der Untervektorraum aus dem Skript:

Betrachte deshalb den m-dimensionalen Untervektorraum V := \langle 1, a, a^2, …, a^{m-1} \rangle_K ⊆ K(a).

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 λ_0, …, λ_m ∈ K, die nicht alle gleich Null sind, sodass 0 = \sum_{i} λ_i \cdot a^i ist. Dann wäre a aber eine Nullstelle des Polynoms f(x) = \sum_i λ_i \cdot x^i ∈ K[x], welches nicht das Nullpolynom ist.

Wir formulieren es deshalb als eigenes Hilfslemma: Eine nichttriviale lineare Relation unter den Potenzen liefert ein Polynom.

Damit folgt die lineare Unabhängigkeit wie im Skript:

Die Menge \{1, a, a^2, …, a^{m-1}\} ⊆ K(a) ist linear unabhängig über K: Jede nicht-triviale Linearkombination der Null lieferte nämlich ein Polynom vom Grad kleiner m, welches nicht das Nullpolynom ist und a als Nullstelle hat — im Widerspruch zur Minimalität des Grades des Minimalpolynoms.

Die „Minimalität des Grades“ heißt in Mathlib minpoly.degree_le_of_ne_zero.

Nun der erste Schritt des Skripts:

Schritt 1: Abgeschlossenheit unter Multiplikation. Weil a eine Nullstelle des Minimalpolynoms f ist, gilt die Gleichung a^m = -\sum_{i=0}^{m-1} λ_i \cdot a^i ∈ V. Durch wiederholte Anwendung dieser Gleichung folgt induktiv, dass a^n ∈ V ist, für alle Zahlen n ∈ ℕ. Jedes Produkt von Elementen aus V ist eine K-Linearkombination von Potenzen von a, also gilt für alle v_1, v_2 ∈ V, dass v_1 \cdot v_2 ∈ V ist.