kebekus/AlgebraInLean
1
0
Fork 0
Code Pull Requests Actions Packages Releases Wiki Activity

Next chapter

Browse Source
This commit is contained in:
Stefan Kebekus
2026-08-11 07:56:09 +02:00
parent 321aa6b651
commit 6345ab1441
7 changed files with 587 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
AlgebraInLean.lean
+2
View File
@@ -1,5 +1,7 @@
-- Wurzelmodul: importiert alle Übungsdateien.
import AlgebraInLean.Basics
import AlgebraInLean.Quotients
import AlgebraInLean.Ideals
import AlgebraInLean.Polynomials
import AlgebraInLean.LittleFermat
import AlgebraInLean.Cauchy
AlgebraInLean/Ideals.lean
+143
View File
@@ -0,0 +1,143 @@
/-
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.
-/
import Mathlib
namespace AlgebraInLean
/-!
# Ringe und Ideale
## Das Mathlib-Wörterbuch
* 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 `I.mul_mem_left` (für alle r ∈ R und
a ∈ I ist r·a ∈ 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 „Hauptideale und Teilbarkeit“ des Skripts ist
das Lemma `Ideal.mem_span_singleton : b ∈ span {a} ↔
a ∣ b`.
* „Jedes Ideal ist endlich erzeugt / ein Hauptideal“ sind
die Prädikate `IsNoetherianRing R` und
`IsPrincipalIdealRing R`.
## ℤ ist ein Hauptidealring
Der Satz „ℤ ist ein Hauptidealring“ aus Kapitel 9 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.
Also enthält I positive Elemente. Sei a ∈ I jetzt das
kleinste positive Element. Wir werden zeigen, dass I = (a)
ist. Die Inklusion (a) ⊆ I ist klar. Sei b ∈ I irgendein
positives Element, dann teilen wir mit Rest: b = q·a + r
mit 0 ≤ r < a. Die Zahl r ist jetzt aber in I, denn b und
q·a sind in I. Weiter muss wegen der Minimalität von a
also r = 0 sein und somit b ∈ (a).“
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 ganzen Zahlen.
-/
theorem int_hauptidealring (I : Ideal ℤ) :
∃ a : ℤ, I = Ideal.span {a} := by
-- „… und I ≠ {0}.“ Das Nullideal erledigt a = 0:
by_cases hI : I = ⊥
· exact ⟨0, by simp [hI]⟩
-- „Dann gibt es ein x ∈ I∖{0}.“
· obtain ⟨x, hxI, hx0⟩ :=
Submodule.exists_mem_ne_zero_of_ne_bot hI
-- „Beachte, dass dann auch −x = (−1)·x in I ist. Also
-- enthält I positive Elemente.“
have hmx : -x ∈ I := by
have h := I.mul_mem_left (-1) hxI
simpa using h
have hpos : ∃ y, y ∈ I ∧ 0 < y := by
rcases lt_or_gt_of_ne hx0 with h | h
· exact ⟨-x, hmx, by omega⟩
· exact ⟨x, hxI, h⟩
-- „Sei a ∈ I jetzt das kleinste positive Element.“
obtain ⟨a, ⟨haI, ha⟩, hmin⟩ :=
Int.exists_least_of_bdd
(P := fun y => y ∈ I ∧ 0 < y)
⟨1, fun z hz => by have := hz.2; omega⟩ hpos
-- „Wir werden zeigen, dass I = (a) ist.“
refine ⟨a, le_antisymm ?_ ?_⟩
· -- „Sei b ∈ I irgendein Element, dann teilen wir mit
-- Rest: b = q·a + r mit 0 ≤ r < a.“
intro b hb
set q := b / a with hq_def
set r := b % a with hr_def
have hdiv : b = a * q + r := by
rw [hq_def, hr_def]
exact (Int.mul_ediv_add_emod b a).symm
have hr0 : 0 ≤ r := Int.emod_nonneg b (by omega)
have hra : r < a := Int.emod_lt_of_pos b ha
-- „Die Zahl r ist jetzt aber in I, denn b und q·a
-- sind in I.“
have hqaI : a * q ∈ I := I.mul_mem_right q haI
have hrI : r ∈ I := by
have hr_eq : r = b - a * q := by rw [hdiv]; ring
rw [hr_eq]
exact I.sub_mem hb hqaI
-- „Weiter muss wegen der Minimalität von a also r = 0
-- sein …“
have hr : r = 0 := by
by_contra hr
have : a ≤ r := hmin r ⟨hrI, by omega⟩
omega
-- „… und somit b ∈ (a).“
rw [Ideal.mem_span_singleton]
exact ⟨q, by rw [hdiv, hr]; ring⟩
· -- „Die Inklusion (a) ⊆ I ist klar.“
rw [Ideal.span_le, Set.singleton_subset_iff]
exact haI
/-!
## Bemerkungen
1. 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 Satz 9.3.8 des Skripts abgedeckt: K[x] ist
euklidisch (Division mit Rest, wobei der Grad die Rolle
des Betrags übernimmt), also ein Hauptidealring.
2. Auch der Hilbertsche Basissatz aus diesem Kapitel steht
in Mathlib: `Polynomial.isNoetherianRing`.
## Übungsaufgabe
Das Beispiel „Triviale Ideale“ des Skripts: „Wenn R ein
Körper und I ⊂ R ein Ideal ist und a ∈ I∖{0}, dann ist auch
jedes andere Körperelement in I. Sei nämlich irgendein
Element r ∈ R gegeben. Nach Definition ist
r = (r·a⁻¹)·a ∈ I. Also ist I = R.“ Übersetzen Sie dieses
Argument: Ersetzen Sie das `sorry` durch einen Beweis.
Tipp: Die Taktik `field_simp` räumt Brüche auf; sie benutzt
dabei die Hypothese `ha0` automatisch.
-/
theorem ideal_im_koerper {K : Type*} [Field K]
(I : Ideal K) {a : K} (haI : a ∈ I) (ha0 : a ≠ 0)
(r : K) : r ∈ I := by
sorry
end AlgebraInLean
AlgebraInLean/Polynomials.lean
+140
View File
@@ -0,0 +1,140 @@
/-
Algebra in Lean — Kapitel 7 des Skripts
=======================================
Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
(Stefan Kebekus, CC-BY 4.0). Sie übersetzt die beiden
Beispiele nach dem Eisenstein-Kriterium
(Satz_Eisenstein_Kriterium) nach Lean; das Kriterium selbst
zitieren wir aus Mathlib.
-/
import Mathlib
namespace AlgebraInLean
open Polynomial
/-!
# Polynome und Irreduzibilität
## Das Mathlib-Wörterbuch
* 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`.
* 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 irreduzibel“ ist `Irreducible f`; die Bedingung
„ggT der Koeffizienten ist 1“ aus dem Eisenstein-Kriterium
heißt `f.IsPrimitive` (kein Nichteinheits-Teiler in R).
## Das Eisenstein-Kriterium
Der Satz aus Kapitel 7 des Skripts:
**Satz (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 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
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
`f.leadingCoeff ∉ P`.
## Erstes Beispiel: xⁿ − r
„Das Polynom xⁿ − r ∈ ℤ[x] ist irreduzibel, wenn r durch
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
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.
-/
theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
(p : ℕ) (hp : p.Prime) (hpr : (p : ℤ) ∣ r)
(hp2r : ¬ (p : ℤ) ^ 2 ∣ r) :
Irreducible (X ^ n - C r) := by
-- Das Primelement p des Skripts wird zum Primideal (p):
have hprime : Prime (p : ℤ) :=
Nat.prime_iff_prime_int.mp hp
have hP : (Ideal.span {(p : ℤ)}).IsPrime :=
(Ideal.span_singleton_prime hprime.ne_zero).mpr hprime
-- Grad und Leitkoeffizient von f = xⁿ − r:
have hmonic : (X ^ n - C r).Monic :=
monic_X_pow_sub_C r hn.ne'
have hdeg := degree_X_pow_sub_C hn r
apply irreducible_of_eisenstein_criterion hP
-- „p ∤ aₙ“: Der Leitkoeffizient ist 1, und p ∤ 1, weil
-- p keine Einheit ist.
· 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
-- durch p teilbar.
· intro k hk
have hkn : k < n := by
rw [hdeg] at hk
exact_mod_cast hk
rw [coeff_sub, coeff_X_pow, if_neg hkn.ne, coeff_C,
Ideal.mem_span_singleton]
rcases eq_or_ne k 0 with h0 | h0
· subst h0
simpa using hpr
· simp [h0]
-- „… vom Grad n > 0.“
· rw [hdeg]
exact_mod_cast hn
-- „p² ∤ a₀“: Der konstante Koeffizient ist −r.
· rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton,
coeff_sub, coeff_X_pow, if_neg hn.ne, coeff_C,
if_pos rfl, zero_sub, dvd_neg]
exact hp2r
-- „ggT(a₀, …, aₙ) = 1“: f ist normiert, also primitiv.
· exact hmonic.isPrimitive
/-!
## Bemerkungen
1. Mathlibs Beweis des Eisenstein-Kriteriums folgt derselben
Idee wie das Erklärvideo 9-1: Reduktion der Koeffizienten
modulo p. Auch das Gauß-Kriterium aus dem ersten Teil
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.
## Ü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 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
Beweis.
-/
theorem xn_sub_p_irreduzibel (n : ℕ) (hn : 0 < n) (p : ℕ)
(hp : p.Prime) :
Irreducible (X ^ n - C (p : ℤ)) := by
sorry
end AlgebraInLean
Book.lean
+6
View File
@@ -4,6 +4,8 @@ import VersoManual
import Book.Basics
import Book.Quotients
import Book.Ideals
import Book.Polynomials
import Book.LittleFermat
import Book.Cauchy
@@ -60,6 +62,10 @@ oder der ausführlichen Anleitung am Anfang der
{include 0 Book.Quotients}
{include 0 Book.Ideals}
{include 0 Book.Polynomials}
{include 0 Book.LittleFermat}
{include 0 Book.Cauchy}
Book/Ideals.lean
+150
View File
@@ -0,0 +1,150 @@
import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
-- `#min_imports`, ergänzt um die Taktiken `ring` und
-- `field_simp`.
import Mathlib.Data.Int.LeastGreatest
import Mathlib.RingTheory.Ideal.Operations
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
open Verso.Genre Manual
open Verso.Genre.Manual.InlineLean
set_option pp.rawOnError true
set_option verso.docstring.allowMissing true
#doc (Manual) "Ringe und Ideale" =>
%%%
htmlSplit := .never
tag := "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.
# Das Mathlib-Wörterbuch
* 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
`I.mul_mem_left` (für alle `r ∈ R` und `a ∈ I` ist `r·a ∈ 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
„Hauptideale und Teilbarkeit“ des Skripts ist das Lemma
`Ideal.mem_span_singleton : b ∈ span {a} ↔ a ∣ b`.
* „Jedes Ideal ist endlich erzeugt / ein Hauptideal“ sind die
Prädikate `IsNoetherianRing R` und `IsPrincipalIdealRing R`.
# ℤ ist ein Hauptidealring
Der Satz aus Kapitel 9 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.
> Also enthält `I` positive Elemente. Sei `a ∈ I` jetzt das kleinste
> positive Element. Wir werden zeigen, dass `I = (a)` ist. Die
> Inklusion `(a) ⊆ I` ist klar. Sei `b ∈ I` irgendein positives
> Element, dann teilen wir mit Rest: `b = q·a + r` mit `0 ≤ r < a`.
> Die Zahl `r` ist jetzt aber in `I`, denn `b` und `q·a` sind in `I`.
> Weiter muss wegen der Minimalität von `a` also `r = 0` sein und
> somit `b ∈ (a)`.
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
ganzen Zahlen.
```lean
theorem int_hauptidealring (I : Ideal ℤ) :
∃ a : ℤ, I = Ideal.span {a} := by
-- „… und I ≠ {0}.“ Das Nullideal erledigt a = 0:
by_cases hI : I = ⊥
· exact ⟨0, by simp [hI]⟩
-- „Dann gibt es ein x ∈ I∖{0}.“
· obtain ⟨x, hxI, hx0⟩ :=
Submodule.exists_mem_ne_zero_of_ne_bot hI
-- „Beachte, dass dann auch −x = (−1)·x in I ist. Also
-- enthält I positive Elemente.“
have hmx : -x ∈ I := by
have h := I.mul_mem_left (-1) hxI
simpa using h
have hpos : ∃ y, y ∈ I ∧ 0 < y := by
rcases lt_or_gt_of_ne hx0 with h | h
· exact ⟨-x, hmx, by omega⟩
· exact ⟨x, hxI, h⟩
-- „Sei a ∈ I jetzt das kleinste positive Element.“
obtain ⟨a, ⟨haI, ha⟩, hmin⟩ :=
Int.exists_least_of_bdd
(P := fun y => y ∈ I ∧ 0 < y)
⟨1, fun z hz => by have := hz.2; omega⟩ hpos
-- „Wir werden zeigen, dass I = (a) ist.“
refine ⟨a, le_antisymm ?_ ?_⟩
· -- „Sei b ∈ I irgendein Element, dann teilen wir mit
-- Rest: b = q·a + r mit 0 ≤ r < a.“
intro b hb
set q := b / a with hq_def
set r := b % a with hr_def
have hdiv : b = a * q + r := by
rw [hq_def, hr_def]
exact (Int.mul_ediv_add_emod b a).symm
have hr0 : 0 ≤ r := Int.emod_nonneg b (by omega)
have hra : r < a := Int.emod_lt_of_pos b ha
-- „Die Zahl r ist jetzt aber in I, denn b und q·a
-- sind in I.“
have hqaI : a * q ∈ I := I.mul_mem_right q haI
have hrI : r ∈ I := by
have hr_eq : r = b - a * q := by rw [hdiv]; ring
rw [hr_eq]
exact I.sub_mem hb hqaI
-- „Weiter muss wegen der Minimalität von a also r = 0
-- sein …“
have hr : r = 0 := by
by_contra hr
have : a ≤ r := hmin r ⟨hrI, by omega⟩
omega
-- „… und somit b ∈ (a).“
rw [Ideal.mem_span_singleton]
exact ⟨q, by rw [hdiv, hr]; ring⟩
· -- „Die Inklusion (a) ⊆ I ist klar.“
rw [Ideal.span_le, Set.singleton_subset_iff]
exact haI
```
# Bemerkungen
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
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`.
# Übungsaufgabe
Das Beispiel „Triviale Ideale“ des Skripts:
> Wenn `R` ein Körper und `I ⊂ R` ein Ideal ist und `a ∈ I∖{0}`,
> dann ist auch jedes andere Körperelement in `I`. Sei nämlich
> irgendein Element `r ∈ R` gegeben. Nach Definition ist
> `r = (r·a⁻¹)·a ∈ I`. Also ist `I = R`.
Übersetzen Sie dieses Argument: Öffnen Sie
`AlgebraInLean/Ideals.lean` und ersetzen Sie das `sorry` durch einen
Beweis. Tipp: Die Taktik `field_simp` räumt Brüche auf; sie benutzt
dabei die Hypothese `ha0` automatisch.
```lean
theorem ideal_im_koerper {K : Type*} [Field K]
(I : Ideal K) {a : K} (haI : a ∈ I) (ha0 : a ≠ 0)
(r : K) : r ∈ I := by
sorry
```
Book/Polynomials.lean
+144
View File
@@ -0,0 +1,144 @@
import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`, ermittelt mit
-- `#min_imports`.
import Mathlib.Data.Nat.Prime.Int
import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
open Verso.Genre
open Verso.Genre.Manual.InlineLean
set_option pp.rawOnError true
set_option verso.docstring.allowMissing true
#doc (Manual) "Polynome und Irreduzibilität" =>
%%%
htmlSplit := .never
tag := "polynome"
%%%
Dieses Kapitel übersetzt die beiden Beispiele nach dem
Eisenstein-Kriterium aus Kapitel 7 des Skripts nach Lean; das
Kriterium selbst zitieren wir aus Mathlib. Nebenbei lernen wir die
Polynom-API kennen.
# Das Mathlib-Wörterbuch
* 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`.
* 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
irreduzibel“ ist `Irreducible f`; die Bedingung „ggT der
Koeffizienten ist 1“ aus dem Eisenstein-Kriterium heißt
`f.IsPrimitive` (kein Nichteinheits-Teiler in `R`).
# Das Eisenstein-Kriterium
Der Satz aus Kapitel 7 des Skripts:
> *Satz (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
> 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 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
`f.leadingCoeff ∉ P`.
# Erstes Beispiel: xⁿ − r
> Das Polynom `xⁿ − r ∈ ℤ[x]` ist irreduzibel, wenn `r` durch 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 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.
```lean
open Polynomial
theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
(p : ℕ) (hp : p.Prime) (hpr : (p : ℤ) ∣ r)
(hp2r : ¬ (p : ℤ) ^ 2 ∣ r) :
Irreducible (X ^ n - C r) := by
-- Das Primelement p des Skripts wird zum Primideal (p):
have hprime : Prime (p : ℤ) :=
Nat.prime_iff_prime_int.mp hp
have hP : (Ideal.span {(p : ℤ)}).IsPrime :=
(Ideal.span_singleton_prime hprime.ne_zero).mpr hprime
-- Grad und Leitkoeffizient von f = xⁿ − r:
have hmonic : (X ^ n - C r).Monic :=
monic_X_pow_sub_C r hn.ne'
have hdeg := degree_X_pow_sub_C hn r
apply irreducible_of_eisenstein_criterion hP
-- „p ∤ aₙ“: Der Leitkoeffizient ist 1, und p ∤ 1, weil
-- p keine Einheit ist.
· 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
-- durch p teilbar.
· intro k hk
have hkn : k < n := by
rw [hdeg] at hk
exact_mod_cast hk
rw [coeff_sub, coeff_X_pow, if_neg hkn.ne, coeff_C,
Ideal.mem_span_singleton]
rcases eq_or_ne k 0 with h0 | h0
· subst h0
simpa using hpr
· simp [h0]
-- „… vom Grad n > 0.“
· rw [hdeg]
exact_mod_cast hn
-- „p² ∤ a₀“: Der konstante Koeffizient ist −r.
· rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton,
coeff_sub, coeff_X_pow, if_neg hn.ne, coeff_C,
if_pos rfl, zero_sub, dvd_neg]
exact hp2r
-- „ggT(a₀, …, aₙ) = 1“: f ist normiert, also primitiv.
· exact hmonic.isPrimitive
```
# Bemerkungen
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ⁿ − p` ist irreduzibel und deshalb
das Minimalpolynom von `ⁿ√p` — greifen wir im Kapitel über
Körpererweiterungen wieder auf.
# Ü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`
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
`sorry` durch einen Beweis.
```lean
theorem xn_sub_p_irreduzibel (n : ℕ) (hn : 0 < n) (p : ℕ)
(hp : p.Prime) :
Irreducible (X ^ n - C (p : ℤ)) := by
sorry
```
README.md
+2
View File
@@ -34,6 +34,8 @@ Lean/Mathlib.
|------|---------------|-------|
| `AlgebraInLean/Basics.lean` | Kapitel 2 | First steps: tactics, groups in 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/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 |