125 lines
4.8 KiB
Lean4
125 lines
4.8 KiB
Lean4
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
|
||
```
|