import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`, ermittelt mit
-- `#min_imports`.
import Mathlib.LinearAlgebra.FreeModule.PID
import Mathlib.RingTheory.Flat.TorsionFree
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) "Körpererweiterungen und die Gradformel" =>
%%%
htmlSplit := .never
tag := "gradformel"
file := "gradformel"
%%%

Dieses Kapitel übersetzt die Gradformel aus Kapitel 3 des Skripts nach
Lean — unsere erste Begegnung mit linearer Algebra: Basen, Dimensionen
und Körpererweiterungen als Vektorräume.

# Das Mathlib-Wörterbuch

* Eine Körpererweiterung $`L/K` ist in Mathlib eine
  `Algebra K L`-Instanz zwischen zwei Körpern — $`L` wird damit
  insbesondere ein $`K`-Vektorraum, genau wie im Skript.

* Eine Kette $`K \subseteq L \subseteq M` besteht aus drei
  Algebra-Instanzen und der Verträglichkeitsbedingung
  `IsScalarTower K L M` („erst nach $`L`, dann nach $`M` einbetten
  ist dasselbe wie direkt nach $`M`“).

* Der Grad $`[L:K]` heißt `Module.finrank K L`.  Achtung, hier weicht
  die Konvention vom Skript ab: `finrank` hat Werte in $`\mathbb{N}`,
  und unendlichdimensionale Erweiterungen bekommen den Wert 0 — wo
  das Skript in seiner Fußnote mit $`\infty` rechnet, rechnet Mathlib
  mit 0.  „$`[L:K]` ist endlich“ ist die Typklasse
  `FiniteDimensional K L`.

# Die Gradformel

Satz 3.6.1 des Skripts, mit Beweis:

> *Satz 3.6.1 (Gradformel).* Es sei $`K \subseteq L \subseteq M` eine
  Kette von Körpererweiterungen.  Dann gilt die Gleichung
  $`[M:K] = [M:L] \cdot [L:K]`.

> _Beweis._ Wir kümmern uns zuerst um die unendlichen Fälle. …  Es
  seien jetzt also $`a := [L:K]` und $`b := [M:L]` beide endlich.
  Wähle Basen $`\ell_1, \dots, \ell_a` von $`L` als
  $`K`-Vektorraum und $`m_1, \dots, m_b` von $`M` als
  $`L`-Vektorraum.  Ich behaupte, dass die $`a \cdot b` Produkte
  $`(\ell_i \cdot m_j)` eine Basis von $`M` als $`K`-Vektorraum
  bilden; damit ist dann sofort $`[M:K] = a \cdot b` gezeigt.

Die unendlichen Fälle entfallen in unserer Fassung, weil wir
Endlichkeit voraussetzen; in Mathlibs 0-Konvention gilt die Formel
sogar uneingeschränkt (`Module.finrank_mul_finrank`).

Die Behauptung — mit den beiden Beweisschritten „Die Produkte bilden
ein Erzeugendensystem“ und „Die Produkte sind linear unabhängig“ —
ist in Mathlib die Konstruktion `Basis.smulTower`: Aus einer Basis
$`\ell` von $`L/K` und einer Basis $`m` von $`M/L` baut sie die
Basis $`(\ell_i \cdot m_j)` von $`M/K` (das Lemma
`Basis.smulTower_apply` bestätigt,
dass die Basiselemente wirklich die Produkte sind).  Der Rest ist
Abzählen der Indexmenge.

```lean
theorem gradformel (K L M : Type*) [Field K] [Field L]
    [Field M] [Algebra K L] [Algebra L M] [Algebra K M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional L M] :
    Module.finrank K M
      = Module.finrank L M * Module.finrank K L := by
  -- „Wähle Basen ℓ₁, …, ℓ_a von L als K-Vektorraum und
  --  m₁, …, m_b von M als L-Vektorraum.“
  let ℓ := Module.finBasis K L
  let m := Module.finBasis L M
  -- „Ich behaupte, dass die a·b Produkte (ℓᵢ·mⱼ) eine
  --  Basis von M als K-Vektorraum bilden …“
  let basis := ℓ.smulTower m
  -- „… damit ist dann sofort [M:K] = a·b gezeigt.“
  rw [Module.finrank_eq_card_basis basis, Fintype.card_prod,
    Fintype.card_fin, Fintype.card_fin, mul_comm]
```

# Bemerkungen

Die beiden Beweisschritte des Skripts stecken im Beweis von
`Basis.smulTower`: Das „Einsetzen“ im Erzeugendensystem-Schritt und
das „Umsortieren“ im Unabhängigkeits-Schritt werden dort durch die
Komposition der Koordinatenabbildungen erledigt —
`Basis.smulTower_repr` sagt, dass die (i,j)-Koordinate von `x` gerade
die i-te Koordinate der j-ten Koordinate ist: exakt das `μᵢⱼ` aus dem
Skript.

# Übungsaufgabe

Das erste Korollar des Skripts zur Gradformel:

> Es sei $`K \subseteq L \subseteq M` eine Kette von
  Körpererweiterungen.  Wenn $`[M:K]` endlich ist, dann ist
  $`[L:K]` endlich, und sogar ein Teiler von $`[M:K]`.

Der erste Teil ist `Module.Finite.left` (und `Module.Finite.right`
liefert die Endlichkeit von $`[M:L]`) — beide müssen mit `have := …`
in den Kontext geholt werden, damit die Instanzsuche sie sieht.  Der
Teiler-Teil ist die Übung: Öffnen Sie `AlgebraInLean/Degrees.lean`
und ersetzen Sie das `sorry` durch einen Beweis mit `gradformel`.

```lean
theorem grad_teilt (K L M : Type*) [Field K] [Field L]
    [Field M] [Algebra K L] [Algebra L M] [Algebra K M]
    [IsScalarTower K L M] [FiniteDimensional K M] :
    Module.finrank K L ∣ Module.finrank K M := by
  sorry
```