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) "Die Transitivität der Algebraizität" =>
%%%
htmlSplit := .never
tag := "transitivitaet"
file := "transitivitaet"
%%%

Dieses Kapitel übersetzt das Hauptresultat von Kapitel 3 des
Skripts nach Lean: die Transitivität der Algebraizität.  Der
Beweis kombiniert die Gradformel mit dem Satz über den Grad
eines Elements; das Mathlib-Wörterbuch des letzten Kapitels
gilt unverändert weiter.

# Korollar 3.7.1

> *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/Transitivity.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

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
open Polynomial IntermediateField

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