Update Degrees.lean

Book/Degrees.lean

@@ -70,7 +70,9 @@ $`\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.
+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]
@@ -122,3 +124,154 @@ theorem grad_teilt (K L M : Type*) [Field K] [Field L]
     Module.finrank K L ∣ Module.finrank K M := by
   sorry
 ```
+
+# Der vollständige Beweis
+
+Der Beweis oben ist ehrlich, aber kurz: Die eigentliche Arbeit —
+die Behauptung über die Produkte — haben wir bei `Basis.smulTower`
+eingekauft.  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.
+
+Die Konstruktion `Module.Basis.mk` baut aus unseren beiden Lemmata —
+linear unabhängig und erzeugend — 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]
+```