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