|
|
|
|
|
import TestGame.Metadata
|
|
|
|
|
|
|
|
|
|
|
|
import Mathlib.Data.Real.Basic -- definiert `ℝ`
|
|
|
|
|
|
import Mathlib.Algebra.Module.Basic -- definiert `module`
|
|
|
|
|
|
import Mathlib.Tactic.LibrarySearch
|
|
|
|
|
|
|
|
|
|
|
|
set_option tactic.hygienic false
|
|
|
|
|
|
|
|
|
|
|
|
Game "TestGame"
|
|
|
|
|
|
World "Module"
|
|
|
|
|
|
Level 1
|
|
|
|
|
|
|
|
|
|
|
|
Title "Module"
|
|
|
|
|
|
|
|
|
|
|
|
Introduction
|
|
|
|
|
|
"
|
|
|
|
|
|
Vektorräume sind in Lean etwas algemeiner definiert, als dies normalerweise in
|
|
|
|
|
|
einer Einführungsvorlesung antrifft: Man definiert ein \"Modul\" (Plural: Moduln)
|
|
|
|
|
|
über einem Ring. Ein Modul über einem Körper wird auch \"Vektorraum\" genannt.
|
|
|
|
|
|
Konkret heisst das:
|
|
|
|
|
|
|
|
|
|
|
|
Sei `R` ein Ring. Ein `R`-Modul ist eine kommutative Gruppe `(V, +)` zusammen mit
|
|
|
|
|
|
einer Abbildung `• : R × V → V` (Skalarmultiplitation genannt), die folgende
|
|
|
|
|
|
Eigenschaften beliebige `(r s : R)` und `(v w : V)`erfüllt:
|
|
|
|
|
|
- `r • (v + w) = r • v + r • w`
|
|
|
|
|
|
- `(r + s) • v = r • v + s • v`
|
|
|
|
|
|
- `(r * s) • v = r • s • v`
|
|
|
|
|
|
- `1 • r = r`
|
|
|
|
|
|
- `0 • v = 0`
|
|
|
|
|
|
- `r • 0 = 0`
|
|
|
|
|
|
|
|
|
|
|
|
Bemerkungen:
|
|
|
|
|
|
1) Über einem `[field R]` sind die letzten beiden Eigenschaften überflüssig, diese kann
|
|
|
|
|
|
man beweisen, wenn man Cancellation (`a₁ + x = a₂ + x → a₁ = a₂`) hat. In einem generellen
|
|
|
|
|
|
Ring, muss das aber nicht gegeben sein (siehe Nullteiler).
|
|
|
|
|
|
2) Die nötigen Annahmen um ein Modul in Lean zu erhalten sind tatsächlich noch etwas lockerer,
|
|
|
|
|
|
so muss `R` nicht ganz ein Ring sein (nur `[semiring R]`) und
|
|
|
|
|
|
`V` muss nicht ganz eine kommutative Gruppe sein (nur `[add_comm_monoid V]`).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Einen abstrakten Vektorraum definiert man wie folgt:
|
|
|
|
|
|
`variables {R V : Type*} [field R] [add_comm_monoid V] [module R V]`
|
|
|
|
|
|
|
|
|
|
|
|
Wenn man hingegen konkret zeigen will, dass ein existierendes Objekt ein Vektorraum ist,
|
|
|
|
|
|
kann man eine einsprechende Instanz wie folgt definieren:
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
instance Q_module : Module ℚ ℝ :=
|
|
|
|
|
|
{ smul := λa r, ↑a * r
|
|
|
|
|
|
smul_zero := _
|
|
|
|
|
|
zero_smul := _
|
|
|
|
|
|
one_smul := _
|
|
|
|
|
|
smul_add := _
|
|
|
|
|
|
add_smul := _
|
|
|
|
|
|
mul_smul := _ }
|
|
|
|
|
|
```
|
|
|
|
|
|
Man muss also angeben, welche Skalarmultiplikation man gerne hätte
|
|
|
|
|
|
(`smul`. In unserem Fall sagen wir einfach, diese soll Multiplikation in `ℝ` sein.)
|
|
|
|
|
|
und dazu jegliche Beweise, dass die Skalarmultiplikation sich mit der Ringstruktur verträgt.
|
|
|
|
|
|
Im nachfolgenden beweisen wir die Eigenschaften einzeln.
|
|
|
|
|
|
"
|
|
|
|
|
|
|
|
|
|
|
|
Statement
|
|
|
|
|
|
"Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
|
|
|
|
|
|
: Module ℚ ℝ :=
|
|
|
|
|
|
{ smul := fun a r ↦ ↑a * r,
|
|
|
|
|
|
smul_zero := by
|
|
|
|
|
|
intro a
|
|
|
|
|
|
rw [smul_zero]
|
|
|
|
|
|
zero_smul := by
|
|
|
|
|
|
intro a
|
|
|
|
|
|
change (0 : ℚ) * a = 0
|
|
|
|
|
|
simp
|
|
|
|
|
|
one_smul := by
|
|
|
|
|
|
intro b
|
|
|
|
|
|
change (1 : ℚ) * b = b
|
|
|
|
|
|
rw [Rat.cast_one, one_mul]
|
|
|
|
|
|
smul_add := by
|
|
|
|
|
|
intro a x y
|
|
|
|
|
|
change a * (x + y) = a * x + a * y
|
|
|
|
|
|
rw [mul_add]
|
|
|
|
|
|
add_smul := by
|
|
|
|
|
|
intro r s x
|
|
|
|
|
|
change (r + s : ℚ) * x = r * x + s * x
|
|
|
|
|
|
rw [Rat.cast_add, add_mul]
|
|
|
|
|
|
mul_smul := by
|
|
|
|
|
|
intro x y b
|
|
|
|
|
|
change (x * y : ℚ) * b = x * (y * b)
|
|
|
|
|
|
rw [Rat.cast_mul, mul_assoc]}
|
