128 lines
4.3 KiB
Lean4
128 lines
4.3 KiB
Lean4
import VersoManual
|
||
import Manual.Meta
|
||
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
|
||
-- `#min_imports`, ergänzt um die Galois-Theorie (die das
|
||
-- Werkzeug wieder übersehen hat).
|
||
import Mathlib.Algebra.Field.Defs
|
||
import Mathlib.Algebra.GroupWithZero.Units.Basic
|
||
import Mathlib.Algebra.Ring.Equiv
|
||
import Mathlib.FieldTheory.Galois.Basic
|
||
|
||
open Verso.Genre
|
||
open Verso.Genre.Manual.InlineLean
|
||
|
||
set_option pp.rawOnError true
|
||
set_option verso.docstring.allowMissing true
|
||
|
||
#doc (Manual) "Galois-Theorie" =>
|
||
%%%
|
||
htmlSplit := .never
|
||
tag := "galois"
|
||
file := "galois"
|
||
%%%
|
||
|
||
Dieses Kapitel zeigt, wie Mathlib die Begriffe der Galoistheorie aus
|
||
den Kapiteln 15 und 16 des Skripts darstellt, und übersetzt die
|
||
Fixkörper-Konstruktion. Deren Beweis ist im Skript eine
|
||
„Hausaufgabe“ und bleibt es auch hier.
|
||
|
||
# Das Mathlib-Wörterbuch
|
||
|
||
* Die Galoisgruppe einer Körpererweiterung $`L/K` ist der Typ
|
||
`L ≃ₐ[K] L` der K-Algebren-Automorphismen; Mathlib stellt dafür
|
||
sogar die Notation `Gal(L/K)` bereit.
|
||
|
||
* „$`L/K` ist galoissch“ ist die Typklasse `IsGalois K L`, definiert
|
||
als „separabel und normal“, genau wie im Skript.
|
||
|
||
* Ein Zwischenkörper ist ein Term `Z : IntermediateField K L`; der
|
||
Fixkörper einer Untergruppe `H : Subgroup Gal(L/K)` heißt
|
||
`IntermediateField.fixedField H`.
|
||
|
||
# Der Fixkörper
|
||
|
||
Satz und Definition 16.1.1 des Skripts:
|
||
|
||
> *Satz und Definition 16.1.1 (Invariante Elemente, Fixkörper).* Sei
|
||
$`L` ein Körper und $`G` eine Menge von Automorphismen
|
||
$`L \to L`. Dann ist die Menge
|
||
$`\operatorname{Fix} G = \{ a \in L : \sigma(a) = a \ \forall \sigma \in G \}`
|
||
ein Unterkörper von $`L`. … Der Beweis des folgenden Satzes ist
|
||
eine Hausaufgabe.
|
||
|
||
Wir definieren die Menge in Lean und beweisen exemplarisch die
|
||
Abgeschlossenheit unter der Multiplikation. Der Rest der Hausaufgabe
|
||
ist, wie im Skript, Ihre Übungsaufgabe.
|
||
|
||
```lean
|
||
def Fix {L : Type*} [Field L] (G : Set (L ≃+* L)) :
|
||
Set L :=
|
||
{a | ∀ σ ∈ G, σ a = a}
|
||
|
||
theorem mul_mem_fix {L : Type*} [Field L]
|
||
{G : Set (L ≃+* L)} {a b : L}
|
||
(ha : a ∈ Fix G) (hb : b ∈ Fix G) :
|
||
a * b ∈ Fix G := by
|
||
-- Automorphismen respektieren die Multiplikation:
|
||
intro σ hσ
|
||
rw [map_mul, ha σ hσ, hb σ hσ]
|
||
```
|
||
|
||
# Der Satz von Artin und der Hauptsatz
|
||
|
||
Auch die großen Sätze dieses Teils der Vorlesung stehen in Mathlib;
|
||
wir zitieren sie mit ihren Namen.
|
||
|
||
> *Satz von Emil Artin (Satz 16.1.2).* Es sei $`G` eine endliche
|
||
Untergruppe der Automorphismengruppe eines Körpers $`L` und es sei
|
||
$`K := \operatorname{Fix} G`. Dann ist $`L/K` eine
|
||
Galoiserweiterung mit Galoisgruppe
|
||
$`\operatorname{Gal}(L/K) = G`. Insbesondere ist
|
||
$`[L:K] = |G|`.
|
||
|
||
Die Gradaussage ist `FixedPoints.finrank_eq_card`; das gebündelte
|
||
Fixkörper-Objekt heißt dort `FixedPoints.subfield G L`.
|
||
|
||
> *Hauptsatz der Galoistheorie (Satz 16.3.2).* Es sei $`L/K` eine
|
||
Galoiserweiterung mit Galoisgruppe $`G`. Dann sind die Abbildungen
|
||
$`Z \mapsto \operatorname{Gal}(L/Z)` und
|
||
$`H \mapsto \operatorname{Fix} H` zueinander inverse,
|
||
inklusionsumkehrende Bijektionen zwischen Zwischenkörpern und
|
||
Untergruppen. …
|
||
|
||
In Mathlib ist das der ordnungsumkehrende Isomorphismus
|
||
`IsGalois.intermediateFieldEquivSubgroup`; das „ᵒᵈ“ (_order dual_)
|
||
in seinem Typ ist genau das „inklusionsumkehrend“ des Skripts. Die
|
||
Gradaussage $`|\operatorname{Gal}(L/K)| = [L:K]` für
|
||
Galoiserweiterungen heißt
|
||
`IsGalois.card_aut_eq_finrank`:
|
||
|
||
```lean
|
||
example (K L : Type*) [Field K] [Field L] [Algebra K L]
|
||
[FiniteDimensional K L] [IsGalois K L] :
|
||
Nat.card (L ≃ₐ[K] L) = Module.finrank K L :=
|
||
IsGalois.card_aut_eq_finrank K L
|
||
```
|
||
|
||
# Übungsaufgabe
|
||
|
||
Die „Hausaufgabe“ des Skripts: Vervollständigen Sie den Nachweis,
|
||
dass `Fix G` ein Unterkörper ist, also die Abgeschlossenheit unter
|
||
Addition und unter Inversen. Für die Addition ist `map_add` das Gegenstück zu
|
||
`map_mul`; für das Inverse respektieren Körperautomorphismen auch die
|
||
Division: `map_inv₀`. Öffnen Sie `AlgebraInLean/Galois.lean` und
|
||
ersetzen Sie die beiden `sorry` durch Beweise.
|
||
|
||
```lean
|
||
theorem add_mem_fix {L : Type*} [Field L]
|
||
{G : Set (L ≃+* L)} {a b : L}
|
||
(ha : a ∈ Fix G) (hb : b ∈ Fix G) :
|
||
a + b ∈ Fix G := by
|
||
sorry
|
||
|
||
theorem inv_mem_fix {L : Type*} [Field L]
|
||
{G : Set (L ≃+* L)} {a : L} (ha : a ∈ Fix G) :
|
||
a⁻¹ ∈ Fix G := by
|
||
sorry
|
||
```
|