AlgebraInLean/Book/Elements.lean

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 — und wie dort holen wir den vollständigen
Beweis am Ende des Kapitels nach.

```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;
der letzte Abschnitt des Kapitels führt auch diesen Beweis
Satz für Satz aus:

```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
```

# Der vollständige Beweis von Satz 3.5.4

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
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)`.

```lean
open Polynomial

variable {K L : Type*} [Field K] [Field L] [Algebra K L]

-- Der Untervektorraum V = ⟨1, a, …, a^{m-1}⟩ des Skripts.
noncomputable def potenzraum (K : Type*) {L : Type*}
    [Field K] [Field L] [Algebra K L] (a : L) :
    Submodule K L :=
  Submodule.span K (Set.range
    fun i : Fin (minpoly K a).natDegree => a ^ (i : ℕ))
```

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.

```lean
theorem polynom_aus_relation {k : ℕ} (y : L) (μ : Fin k → K)
    (hrel : ∑ i, μ i • y ^ (i : ℕ) = 0) (i₀ : Fin k)
    (hμ : μ i₀ ≠ 0) :
    ∃ g : K[X],
      g ≠ 0 ∧ g.degree < (k : ℕ) ∧ aeval y g = 0 := by
  -- Das Polynom g = ∑ μᵢ·xⁱ …
  refine ⟨∑ i : Fin k, C (μ i) * X ^ (i : ℕ), ?_, ?_, ?_⟩
  -- „… welches nicht das Nullpolynom ist“: sein i₀-ter
  -- Koeffizient ist μᵢ₀ ≠ 0.
  · intro h0
    apply hμ
    have hc := congrArg (fun g => coeff g (i₀ : ℕ)) h0
    simpa [finsetSum_coeff, coeff_C_mul, coeff_X_pow,
      Fin.val_inj] using hc
  -- … hat Grad < k …
  · refine lt_of_le_of_lt (degree_sum_le _ _) ?_
    rw [Finset.sup_lt_iff
      (by exact_mod_cast WithBot.bot_lt_coe k)]
    intro i _
    exact lt_of_le_of_lt (degree_C_mul_X_pow_le _ _)
      (by exact_mod_cast i.isLt)
  -- … und „y wäre eine Nullstelle des Polynoms“.
  · rw [map_sum]
    simp_rw [map_mul, aeval_C, map_pow, aeval_X,
      ← Algebra.smul_def]
    exact hrel
```

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`.

```lean
theorem potenzen_unabhaengig {a : L} (ha : IsIntegral K a) :
    LinearIndependent K
      (fun i : Fin (minpoly K a).natDegree =>
        a ^ (i : ℕ)) := by
  rw [Fintype.linearIndependent_iff]
  intro μ hrel i₀
  by_contra hμ
  -- „Jede nicht-triviale Linearkombination der Null
  --  lieferte ein Polynom vom Grad kleiner m … mit a als
  --  Nullstelle“
  obtain ⟨g, hg0, hdeg, hroot⟩ :=
    polynom_aus_relation a μ hrel i₀ hμ
  -- „im Widerspruch zur Minimalität des Grades des
  --  Minimalpolynoms.“
  have hle := minpoly.degree_le_of_ne_zero K a hg0 hroot
  rw [degree_eq_natDegree (minpoly.ne_zero ha)] at hle
  exact absurd (hle.trans_lt hdeg) (lt_irrefl _)
```

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.

```lean
-- „Weil a eine Nullstelle des Minimalpolynoms f ist, gilt
--  die Gleichung a^m = -∑ λᵢ·aⁱ.“
theorem hoechste_potenz {a : L} (ha : IsIntegral K a) :
    a ^ (minpoly K a).natDegree =
      -∑ i ∈ Finset.range (minpoly K a).natDegree,
        (minpoly K a).coeff i • a ^ i := by
  have h := minpoly.aeval K a
  rw [aeval_eq_sum_range, Finset.sum_range_succ,
    (minpoly.monic ha).coeff_natDegree, one_smul] at h
  exact eq_neg_of_add_eq_zero_right h

-- „Durch wiederholte Anwendung dieser Gleichung folgt
--  induktiv, dass aⁿ ∈ V ist, für alle Zahlen n ∈ ℕ.“
theorem potenz_mem {a : L} (ha : IsIntegral K a) (n : ℕ) :
    a ^ n ∈ potenzraum K a := by
  induction n using Nat.strong_induction_on with
  | _ n IH =>
    by_cases hn : n < (minpoly K a).natDegree
    · exact Submodule.subset_span ⟨⟨n, hn⟩, rfl⟩
    · rw [not_lt] at hn
      have hm0 : 0 < (minpoly K a).natDegree :=
        minpoly.natDegree_pos ha
      have hsplit : a ^ n =
          a ^ (n - (minpoly K a).natDegree)
            * a ^ (minpoly K a).natDegree := by
        rw [← pow_add]
        congr 1
        omega
      rw [hsplit, hoechste_potenz ha, mul_neg,
        Finset.mul_sum]
      refine Submodule.neg_mem _
        (Submodule.sum_mem _ fun i hi => ?_)
      rw [mul_smul_comm, ← pow_add]
      refine Submodule.smul_mem _ _ (IH _ ?_)
      have := Finset.mem_range.mp hi
      omega

-- „Jedes Produkt von Elementen aus V ist eine
--  K-Linearkombination von Potenzen von a, also gilt für
--  alle v₁, v₂ ∈ V, dass v₁·v₂ ∈ V ist.“
theorem produkt_mem {a : L} (ha : IsIntegral K a) {x y : L}
    (hx : x ∈ potenzraum K a) (hy : y ∈ potenzraum K a) :
    x * y ∈ potenzraum K a := by
  induction hx, hy using Submodule.span_induction₂ with
  | mem_mem u v hu hv =>
    obtain ⟨i, rfl⟩ := hu
    obtain ⟨j, rfl⟩ := hv
    simpa [pow_add] using potenz_mem ha ((i : ℕ) + (j : ℕ))
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u v w _ _ hw h1 h2 =>
    rw [add_mul]
    exact Submodule.add_mem _ h1 h2
  | add_right u v w hu _ _ h1 h2 =>
    rw [mul_add]
    exact Submodule.add_mem _ h1 h2
  | smul_left r u v _ _ h =>
    rw [smul_mul_assoc]
    exact Submodule.smul_mem _ _ h
  | smul_right r u v _ _ h =>
    rw [mul_smul_comm]
    exact Submodule.smul_mem _ _ h
```

Das „Jedes Produkt … ist eine $`K`-Linearkombination“ erledigt
`Submodule.span_induction₂`: Es genügt, die Behauptung für die
erzeugenden Potenzen zu prüfen (der Fall `mem_mem`, dort ist
$`a^i \cdot a^j = a^{i+j}`); Summen und Vielfache vererben sich.

Der zweite Schritt ist das Herzstück:

> _Schritt 2: Abgeschlossenheit unter Inversenbildung._ Es sei
  $`y ∈ V` mit $`y ≠ 0` gegeben.  Weil $`V` abgeschlossen unter
  der Multiplikation ist, liegen alle Potenzen
  $`1, y, y^2, …, y^m` in $`V`.  Das sind $`m+1` Elemente in
  einem Vektorraum der Dimension $`m`, also sind diese Elemente
  linear abhängig über $`K`.  Insbesondere ist $`y` algebraisch
  über $`K`.  Es sei $`g(x) = c_0 + c_1 x + ⋯ + x^n` das
  Minimalpolynom von $`y` über $`K`.  Dann ist $`c_0 ≠ 0`:
  Andernfalls könnte ich nämlich in $`g` einmal $`x`
  ausklammern, also $`g = x \cdot h` schreiben.  Weil $`K(a)`
  ein Körper und $`y ≠ 0` ist, folgte aus
  $`0 = g(y) = y \cdot h(y)` schon $`h(y) = 0` — im Widerspruch
  zur Minimalität des Grades von $`g`.  Aus der Gleichung
  $`0 = g(y) = y \cdot (y^{n-1} + c_{n-1} y^{n-2} + ⋯ + c_1) + c_0`
  folgt jetzt $`1/y = (y^{n-1} + ⋯ + c_1)/(-c_0) ∈ V`, denn der
  Zähler ist eine $`K`-Linearkombination von Potenzen von $`y`,
  liegt also in $`V`, und der Nenner $`-c_0` liegt in $`K`.

Das Zählargument „$`m+1` Elemente in Dimension $`m`“ ist
`LinearIndependent.fintype_card_le_finrank`; die Dimension von
$`V` kennen wir aus der linearen Unabhängigkeit
(`finrank_span_eq_card`).

```lean
theorem invers_mem {a : L} (ha : IsIntegral K a) {y : L}
    (hy : y ∈ potenzraum K a) (hy0 : y ≠ 0) :
    y⁻¹ ∈ potenzraum K a := by
  -- „Weil V abgeschlossen unter der Multiplikation ist,
  --  liegen alle Potenzen 1, y, y², … in V.“
  have hyn : ∀ j : ℕ, y ^ j ∈ potenzraum K a := by
    intro j
    induction j with
    | zero => simpa using potenz_mem ha 0
    | succ j IH =>
      rw [pow_succ]
      exact produkt_mem ha IH hy
  -- „Das sind m+1 Elemente in einem Vektorraum der
  --  Dimension m, also sind diese Elemente linear abhängig
  --  über K.“
  have hfin : FiniteDimensional K (potenzraum K a) := by
    unfold potenzraum
    exact FiniteDimensional.span_of_finite K
      (Set.finite_range _)
  have hdim : Module.finrank K (potenzraum K a)
      = (minpoly K a).natDegree := by
    unfold potenzraum
    rw [finrank_span_eq_card (potenzen_unabhaengig ha),
      Fintype.card_fin]
  have habh : ¬ LinearIndependent K
      (fun i : Fin ((minpoly K a).natDegree + 1) =>
        (⟨y ^ (i : ℕ), hyn i⟩ : potenzraum K a)) := by
    intro h
    have hcard := h.fintype_card_le_finrank
    rw [Fintype.card_fin, hdim] at hcard
    omega
  -- „Insbesondere ist y algebraisch über K.“
  rw [Fintype.not_linearIndependent_iff] at habh
  obtain ⟨μ, hrel, i₀, hμ0⟩ := habh
  have hrelL : ∑ i : Fin ((minpoly K a).natDegree + 1),
      μ i • y ^ (i : ℕ) = 0 := by
    simpa using congrArg
      (Submodule.subtype (potenzraum K a)) hrel
  obtain ⟨g, hg0, _, hgroot⟩ :=
    polynom_aus_relation y μ hrelL i₀ hμ0
  have hyint : IsIntegral K y :=
    (IsAlgebraic.isIntegral ⟨g, hg0, hgroot⟩)
  -- „Es sei g das Minimalpolynom von y über K.  Dann ist
  --  c₀ ≠ 0: Andernfalls könnte ich nämlich in g einmal x
  --  ausklammern, also g = x·h schreiben.  Weil K(a) ein
  --  Körper und y ≠ 0 ist, folgte aus 0 = g(y) = y·h(y)
  --  schon h(y) = 0 — im Widerspruch zur Minimalität des
  --  Grades von g.“
  have hc0 : (minpoly K y).coeff 0 ≠ 0 := by
    intro h0
    obtain ⟨h, hh⟩ := X_dvd_iff.mpr h0
    have hhy : aeval y h = 0 := by
      have haev := minpoly.aeval K y
      rw [hh, map_mul, aeval_X] at haev
      rcases mul_eq_zero.mp haev with h1 | h1
      · exact absurd h1 hy0
      · exact h1
    have hhne : h ≠ 0 := by
      rintro rfl
      rw [mul_zero] at hh
      exact minpoly.ne_zero hyint hh
    have hle := minpoly.degree_le_of_ne_zero K y hhne hhy
    rw [hh, mul_comm] at hle
    exact absurd hle
      (not_le.mpr (degree_lt_degree_mul_X hhne))
  -- „Aus der Gleichung 0 = g(y) = y·(y^{n-1} + ⋯ + c₁) + c₀
  --  folgt jetzt 1/y = (y^{n-1} + ⋯ + c₁)/(-c₀) ∈ V …“
  have expand := minpoly.aeval K y
  rw [aeval_eq_sum_range, Finset.sum_range_succ'] at expand
  simp_rw [pow_succ, ← smul_mul_assoc, pow_zero] at expand
  rw [← Finset.sum_mul] at expand
  have hwy : (∑ i ∈ Finset.range (minpoly K y).natDegree,
        (minpoly K y).coeff (i + 1) • y ^ i) * y
      = -((minpoly K y).coeff 0 • 1) :=
    eq_neg_of_add_eq_zero_left expand
  have hone : y * ((-(minpoly K y).coeff 0)⁻¹ •
      ∑ i ∈ Finset.range (minpoly K y).natDegree,
        (minpoly K y).coeff (i + 1) • y ^ i) = 1 := by
    rw [mul_smul_comm, mul_comm y, hwy, ← neg_smul,
      smul_smul, inv_mul_cancel₀ (neg_ne_zero.mpr hc0),
      one_smul]
  rw [inv_eq_of_mul_eq_one_right hone]
  -- „… denn der Zähler ist eine K-Linearkombination von
  --  Potenzen von y, liegt also in V, und der Nenner -c₀
  --  liegt in K.“
  exact Submodule.smul_mem _ _
    (Submodule.sum_mem _ fun i _ =>
      Submodule.smul_mem _ _ (hyn i))
```

Bleibt der Zusammenbau:

> Ich behaupte, dass $`V = K(a)` ist; damit ist dann
  $`[K(a):K] = \dim_K V = m` und der Satz ist bewiesen.  Um die
  Behauptung zu zeigen, genügt es zu zeigen, dass $`V` ein
  Unterkörper von $`K(a)` ist.  Denn $`V` enthält $`K` und das
  Element $`a`, und $`K(a)` ist per Definition der kleinste
  Unterkörper, der $`K` und $`a` enthält.  Weil $`V` ein
  Untervektorraum ist, ist $`V` abgeschlossen unter der
  Addition.

Das „Bündeln“ von $`V` mit den bewiesenen Abgeschlossenheiten zu
einem Unterkörper ist in Lean das Ausfüllen der Strukturfelder
von `Subalgebra` und `IntermediateField`; das „per Definition
der kleinste Unterkörper“ ist `adjoin_simple_le_iff`.

```lean
theorem grad_element_vollstaendig {a : L}
    (ha : IsIntegral K a) :
    Module.finrank K K⟮a⟯ = (minpoly K a).natDegree := by
  -- „… genügt es zu zeigen, dass V ein Unterkörper von K(a)
  --  ist.“ — wir bündeln V zu einem Zwischenkörper F:
  let A : Subalgebra K L :=
    { carrier := potenzraum K a
      mul_mem' := fun hx hy => produkt_mem ha hx hy
      one_mem' := by simpa using potenz_mem ha 0
      add_mem' := fun hx hy => Submodule.add_mem _ hx hy
      zero_mem' := Submodule.zero_mem _
      algebraMap_mem' := fun c => by
        rw [Algebra.algebraMap_eq_smul_one]
        exact Submodule.smul_mem _ _
          (by simpa using potenz_mem ha 0) }
  let F : IntermediateField K L :=
    { A with
      inv_mem' := fun x hx => by
        by_cases hx0 : x = 0
        · rw [hx0, inv_zero]
          exact Submodule.zero_mem _
        · exact invers_mem ha hx hx0 }
  -- „Denn V enthält K und das Element a, und K(a) ist per
  --  Definition der kleinste Unterkörper, der K und a
  --  enthält.“
  have haF : a ∈ F := by
    show a ∈ potenzraum K a
    simpa using potenz_mem ha 1
  have oben : K⟮a⟯ ≤ F := adjoin_simple_le_iff.mpr haF
  have unten : F ≤ K⟮a⟯ := by
    intro x hx
    have hVsub : potenzraum K a ≤
        Subalgebra.toSubmodule K⟮a⟯.toSubalgebra := by
      unfold potenzraum
      rw [Submodule.span_le]
      rintro _ ⟨i, rfl⟩
      exact pow_mem (mem_adjoin_simple_self K a) _
    exact hVsub hx
  have hFK : F = K⟮a⟯ := le_antisymm unten oben
  -- „… damit ist dann [K(a):K] = dim_K V = m und der Satz
  --  ist bewiesen.“
  rw [← hFK]
  have h1 : Module.finrank K F
      = Module.finrank K (potenzraum K a) :=
    (Subalgebra.finrank_toSubmodule A).symm
  rw [h1]
  unfold potenzraum
  rw [finrank_span_eq_card (potenzen_unabhaengig ha),
    Fintype.card_fin]
```

# Der vollständige Beweis der Transitivität

Zum Schluss der Skript-Beweis der Transitivität, ohne das Zitat
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:

* Die Koeffizienten $`λ_i` des Minimalpolynoms liegen in $`L`;
  das Skript liest sie stillschweigend als Elemente von $`M`.
  In Lean geschieht das explizit über die Einbettung
  `algebraMap L M`.  Die endliche Menge der Koeffizienten eines
  Polynoms heißt `Polynomial.coeffs`.

* „$`f` liegt in $`Z[x]`“ ist in Lean ein echter
  Übersetzungsschritt: `Polynomial.toSubring` fasst ein Polynom,
  dessen Koeffizienten in einem Teilring liegen, als Polynom
  über diesem Teilring auf.

* Das Skript zitiert zweimal Satz 3.6.5 (endlich erzeugt von
  algebraischen Elementen ⟺ endlich ⟹ algebraisch); in Mathlib
  sind das `IntermediateField.finiteDimensional_adjoin` und
  `Algebra.IsAlgebraic.of_finite`.  Die Gradformel steckt in
  `FiniteDimensional.trans`.

```lean
theorem transitivitaet_vollstaendig (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 x
  -- „Wir wissen, dass m algebraisch über L ist; es sei f
  --  das Minimalpolynom von m über L.“
  have hxL : IsIntegral L x :=
    (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
  -- „Die Koeffizienten λᵢ liegen in L.“ — wir fassen sie
  --  über die Einbettung L → M als Elemente von M auf.
  set S : Set M :=
    algebraMap L M '' ↑(minpoly L x).coeffs
  -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1})“
  set Z : IntermediateField K M :=
    IntermediateField.adjoin K S
  -- „Die Erweiterung L/K ist algebraisch, also sind die
  --  endlich vielen Elemente λ₀, …, λ_{n-1} allesamt
  --  algebraisch über K.“
  have hS : ∀ s ∈ S, IsIntegral K s := by
    rintro _ ⟨c, _, rfl⟩
    exact ((Algebra.IsAlgebraic.isAlgebraic
        (R := K) c).isIntegral).map
      (IsScalarTower.toAlgHom K L M)
  have hSfin : S.Finite :=
    Set.Finite.image _ (minpoly L x).coeffs.finite_toSet
  have : Finite ↥S := hSfin.to_subtype
  -- „Satz 3.6.5 sagt deshalb, dass [Z:K] < ∞ ist.“
  have hZfin : FiniteDimensional K Z :=
    IntermediateField.finiteDimensional_adjoin hS
  -- „Weiter liegt das Polynom f in Z[x] und hat m als
  --  Nullstelle.  Also ist m auch algebraisch über Z.“
  have hxZ : IsIntegral Z x := by
    have hco : (↑((minpoly L x).map (algebraMap L M)).coeffs
        : Set M) ⊆ ↑Z.toSubalgebra.toSubring := by
      intro c hc
      obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hc
      rw [coeff_map]
      have hne : (minpoly L x).coeff n ≠ 0 := by
        intro h0
        rw [mem_support_iff, coeff_map, h0, map_zero] at hn
        exact hn rfl
      exact subset_adjoin K S
        ⟨(minpoly L x).coeff n, coeff_mem_coeffs hne, rfl⟩
    refine ⟨((minpoly L x).map (algebraMap L M)).toSubring
      Z.toSubalgebra.toSubring hco, ?_, ?_⟩
    · exact (monic_toSubring _ _ _).mpr
        ((minpoly.monic hxL).map _)
    · rw [show algebraMap Z M
          = (Z.toSubalgebra.toSubring).subtype from rfl,
        eval₂_eq_eval_map, map_toSubring, eval_map,
        ← aeval_def, minpoly.aeval]
  -- „… und Satz 3.5.4 liefert [Z(m):Z] < ∞.“
  have hE : FiniteDimensional Z Z⟮x⟯ :=
    IntermediateField.adjoin.finiteDimensional hxZ
  -- „Mit der Gradformel folgt
  --  [Z(m):K] = [Z(m):Z]·[Z:K] < ∞.“
  have hZM : FiniteDimensional K (Z⟮x⟯.restrictScalars K) :=
    FiniteDimensional.trans K Z Z⟮x⟯
  -- „Wieder nach Satz 3.6.5 ist die Erweiterung Z(m)/K dann
  --  algebraisch.“
  have halg :
      Algebra.IsAlgebraic K (Z⟮x⟯.restrictScalars K) :=
    Algebra.IsAlgebraic.of_finite K _
  -- „Insbesondere ist das Element m ∈ Z(m) algebraisch
  --  über K.“
  have hmem : x ∈ Z⟮x⟯.restrictScalars K :=
    mem_adjoin_simple_self Z x
  exact IntermediateField.isAlgebraic_iff.mp
    (Algebra.IsAlgebraic.isAlgebraic
      (⟨x, hmem⟩ : Z⟮x⟯.restrictScalars K))
```

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
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
$`m` algebraisch über $`Z`“ die kleine Rechnung, dass Auswerten
über $`Z` und Auswerten über $`M` dasselbe ergeben
(`eval₂_eq_eval_map` und `map_toSubring`).