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.  Damit wird $`L`
  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
  also 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 zerfällt in die beiden Beweisschritte „Die Produkte
bilden ein Erzeugendensystem“ und „Die Produkte sind linear
unabhängig“.  In Mathlib ist sie 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.  Wer der Mathlib nicht trauen will, findet
im letzten Abschnitt dieses Kapitels den vollständigen Beweis, Satz
für Satz aus dem Skript übersetzt.

```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
$`μ_{ij}` 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
```

# Der vollständige Beweis

Der Beweis oben ist ehrlich, aber kurz: Die eigentliche Arbeit haben
wir bei `Basis.smulTower` eingekauft, nämlich die Behauptung über die
Produkte.  Zum Abschluss führen wir den Skript-Beweis selbst aus,
Satz für Satz.  Die unendlichen Fälle entfallen wie zuvor, weil wir
Endlichkeit voraussetzen.

Wir formulieren die beiden Beweisschritte als eigenständige Lemmata.
Statt der nummerierten Basen $`\ell_1, \dots, \ell_a` und
$`m_1, \dots, m_b` des Skripts sprechen wir von Basen `ℓ` und `m`,
die über die Indexmengen `Fin a` und `Fin b` laufen; die Familie der
Produkte $`(\ell_i \cdot m_j)` ist dann über Paare
`p : Fin a × Fin b` indiziert.

Der erste Schritt des Skripts:

> _Schritt 1: Die Produkte bilden ein Erzeugendensystem._ Es sei ein
  Element $`m ∈ M` gegeben.  Schreibe $`m` als $`L`-Linearkombination
  der Basis $`m_1, …, m_b`, nämlich $`m = \sum_j λ_j \cdot m_j` mit
  $`λ_j ∈ L`, und schreibe danach jeden der Koeffizienten $`λ_j` als
  $`K`-Linearkombination der Basis $`\ell_1, …, \ell_a`, nämlich
  $`λ_j = \sum_i μ_{ij} \cdot \ell_i` mit $`μ_{ij} ∈ K`.  Einsetzen
  liefert $`m = \sum_{i,j} μ_{ij} \cdot (\ell_i \cdot m_j)`.

In Lean heißen die Koeffizienten $`λ_j` und $`μ_{ij}` gerade
`m.repr x j` und `ℓ.repr (m.repr x j) i`.  Das „Schreibe … als
Linearkombination“ des Skripts ist das Lemma `Basis.sum_repr`.  Das
„Einsetzen“ ist eine kleine Rechnung mit dem Distributivgesetz
`Finset.sum_smul` und der Turmbedingung `smul_assoc`,
$`(μ \cdot \ell) \cdot m = μ \cdot (\ell \cdot m)`.

```lean
theorem produkte_erzeugen {K L M : Type*} [Field K]
    [Field L] [Field M] [Algebra K L] [Algebra L M]
    [Algebra K M] [IsScalarTower K L M] {a b : ℕ}
    (ℓ : Module.Basis (Fin a) K L)
    (m : Module.Basis (Fin b) L M) :
    ⊤ ≤ Submodule.span K
      (Set.range
        fun p : Fin a × Fin b => ℓ p.1 • m p.2) := by
  -- „Es sei ein Element m ∈ M gegeben.“
  intro x _
  -- „Schreibe m als L-Linearkombination der Basis
  --  m₁, …, m_b, und schreibe danach jeden der
  --  Koeffizienten λⱼ als K-Linearkombination der Basis
  --  ℓ₁, …, ℓ_a.  Einsetzen liefert m = ∑ μᵢⱼ·(ℓᵢ·mⱼ).“
  have einsetzen : x = ∑ j, ∑ i,
      ℓ.repr (m.repr x j) i • (ℓ i • m j) := by
    conv_lhs => rw [← m.sum_repr x]
    refine Finset.sum_congr rfl fun j _ => ?_
    conv_lhs => rw [← ℓ.sum_repr (m.repr x j)]
    rw [Finset.sum_smul]
    exact Finset.sum_congr rfl fun i _ => smul_assoc ..
  -- Eine K-Linearkombination der Produkte liegt im
  -- Erzeugnis.
  rw [einsetzen]
  exact Submodule.sum_mem _ fun j _ =>
    Submodule.sum_mem _ fun i _ =>
      Submodule.smul_mem _ _
        (Submodule.subset_span ⟨(i, j), rfl⟩)
```

Der zweite Schritt:

> _Schritt 2: Die Produkte sind linear unabhängig._ Es sei eine
  $`K`-lineare Relation gegeben, das heißt
  $`0 = \sum_{i,j} μ_{ij} \cdot (\ell_i \cdot m_j)` mit
  $`μ_{ij} ∈ K`.  Umsortieren liefert
  $`0 = \sum_j \bigl(\sum_i μ_{ij} \cdot \ell_i\bigr) \cdot m_j`.
  Dies ist eine $`L`-lineare Relation unter den Basiselementen
  $`m_j`, also verschwinden alle Koeffizienten: Für jeden Index
  $`j` ist $`\sum_i μ_{ij} \cdot \ell_i = 0`.  Das wiederum ist
  jeweils eine $`K`-lineare Relation unter den Basiselementen
  $`\ell_i`, also ist $`μ_{ij} = 0` für alle Indizes $`i` und $`j`.

Das Lemma `Fintype.linearIndependent_iff` übersetzt „linear
unabhängig“ in genau die Sprechweise des Skripts: Jede Relation hat
verschwindende Koeffizienten.  Wir benutzen es dreimal: einmal in
jede Richtung für die Basen `m` und `ℓ`, und einmal für die zu
beweisende Aussage selbst.

```lean
theorem produkte_unabhaengig {K L M : Type*} [Field K]
    [Field L] [Field M] [Algebra K L] [Algebra L M]
    [Algebra K M] [IsScalarTower K L M] {a b : ℕ}
    (ℓ : Module.Basis (Fin a) K L)
    (m : Module.Basis (Fin b) L M) :
    LinearIndependent K
      fun p : Fin a × Fin b => ℓ p.1 • m p.2 := by
  -- „Es sei eine K-lineare Relation gegeben, das heißt
  --  0 = ∑ μᵢⱼ·(ℓᵢ·mⱼ), wobei μᵢⱼ ∈ K.“
  rw [Fintype.linearIndependent_iff]
  intro μ relation p
  -- Schreibe die Summe über alle Paare als Doppelsumme.
  have relation' :
      ∑ i, ∑ j, μ (i, j) • (ℓ i • m j) = 0 := by
    simpa [Fintype.sum_prod_type] using relation
  -- „Umsortieren liefert 0 = ∑ⱼ (∑ᵢ μᵢⱼ·ℓᵢ)·mⱼ.“
  have umsortiert :
      ∑ j, (∑ i, μ (i, j) • ℓ i) • m j = 0 := by
    calc ∑ j, (∑ i, μ (i, j) • ℓ i) • m j
        = ∑ j, ∑ i, μ (i, j) • (ℓ i • m j) := by
          simp_rw [Finset.sum_smul, smul_assoc]
      _ = ∑ i, ∑ j, μ (i, j) • (ℓ i • m j) :=
          Finset.sum_comm
      _ = 0 := relation'
  -- „Dies ist eine L-lineare Relation unter den Basis-
  --  elementen mⱼ, also verschwinden alle Koeffizienten:
  --  Für jeden Index j ist ∑ᵢ μᵢⱼ·ℓᵢ = 0.“
  have koeff : ∀ j, ∑ i, μ (i, j) • ℓ i = 0 :=
    Fintype.linearIndependent_iff.mp m.linearIndependent _
      umsortiert
  -- „Das wiederum ist jeweils eine K-lineare Relation
  --  unter den Basiselementen ℓᵢ, also ist μᵢⱼ = 0 für
  --  alle Indizes.“
  exact Fintype.linearIndependent_iff.mp
    ℓ.linearIndependent _ (koeff p.2) p.1
```

Zum Schluss der Zusammenbau, wie im Skript angekündigt:

> Ich behaupte, dass die $`a \cdot b` Produkte
  $`(\ell_i \cdot m_j)_{1 ≤ i ≤ a,\ 1 ≤ j ≤ b}` eine Basis von $`M`
  als $`K`-Vektorraum bilden; damit ist dann sofort
  $`[M:K] = a \cdot b` gezeigt.

Aus unseren beiden Lemmata (linear unabhängig, erzeugend) baut die
Konstruktion `Module.Basis.mk` eine Basis.  Das „sofort gezeigt“
ist wieder das Abzählen der Indexmenge `Fin a × Fin b`.

```lean
theorem gradformel_vollstaendig
    (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 : Module.Basis (Fin _ × Fin _) K M :=
    Module.Basis.mk (produkte_unabhaengig ℓ m)
      (produkte_erzeugen ℓ 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]
```