First chapters
This commit is contained in:
Stefan Kebekus committed
1 parent
006a51cd8e
commit
321aa6b651
269 files changed
+50018
-219
No files matched your search
@@ -1 +1,3 @@
|
||||
.lake/
|
||||
_out/
|
||||
public/
|
||||
+3
-1
@@ -1,3 +1,5 @@
|
||||
-- Root module: imports all chapters of "Algebra in Lean".
|
||||
-- Wurzelmodul: importiert alle Übungsdateien.
|
||||
import AlgebraInLean.Basics
|
||||
import AlgebraInLean.Quotients
|
||||
import AlgebraInLean.LittleFermat
|
||||
import AlgebraInLean.Cauchy
|
||||
@@ -0,0 +1,95 @@
|
||||
/-
|
||||
Algebra in Lean — Kapitel 2 des Skripts
|
||||
=======================================
|
||||
|
||||
Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
|
||||
(Stefan Kebekus, CC-BY 4.0). Sie ist der Einstieg: erste
|
||||
Taktiken, erste Beweise, und die Frage, wie Mathlib den
|
||||
Begriff „Gruppe“ aus Definition 2.1.1 des Skripts darstellt.
|
||||
-/
|
||||
import Mathlib
|
||||
|
||||
namespace AlgebraInLean
|
||||
|
||||
/-!
|
||||
# Erste Schritte
|
||||
|
||||
## Beweise lesen und schreiben
|
||||
|
||||
Ein Beweis in Lean beginnt mit `by` und besteht aus
|
||||
*Taktiken*. Setzen Sie den Cursor in einen Beweis und
|
||||
beobachten Sie das Infoview-Panel: Es zeigt zu jedem
|
||||
Zeitpunkt die Hypothesen und das noch zu zeigende Ziel.
|
||||
|
||||
Vier Taktiken reichen für den Anfang erstaunlich weit:
|
||||
|
||||
* `norm_num` verrechnet konkrete Zahlen,
|
||||
* `ring` beweist Gleichungen, die in jedem kommutativen
|
||||
Ring gelten,
|
||||
* `omega` löst lineare Arithmetik über ℕ und ℤ,
|
||||
* `rw [h]` schreibt mit einer Gleichung `h` um.
|
||||
-/
|
||||
|
||||
example : 2 + 3 = 5 := by norm_num
|
||||
|
||||
example (a b : ℤ) :
|
||||
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
|
||||
ring
|
||||
|
||||
example (n : ℕ) (h : n < 5) : n ≤ 7 := by omega
|
||||
|
||||
example (x y : ℚ) (h : x = y) : x + 1 = y + 1 := by
|
||||
rw [h]
|
||||
|
||||
/-!
|
||||
## Gruppen in Mathlib
|
||||
|
||||
Definition 2.1.1 des Skripts:
|
||||
|
||||
**Definition (Gruppe).** *Eine Gruppe ist eine nicht-leere
|
||||
Menge G mit einer Abbildung m : G ⨯ G → G, sodass folgende
|
||||
Eigenschaften gelten. Assoziativität: … Neutrales Element:
|
||||
Es gibt genau ein Element e aus G, sodass für alle a aus G
|
||||
gilt: m(e,a) = m(a,e) = a. Inverse Elemente: Für alle a aus
|
||||
G gibt es genau ein Element b aus G, sodass
|
||||
m(a,b) = m(b,a) = e ist.*
|
||||
|
||||
In Mathlib ist eine Gruppe eine Typklasse `Group G`. Die
|
||||
Verknüpfung schreibt sich `a * b`, das neutrale Element `1`,
|
||||
das Inverse `a⁻¹`; die Axiome heißen `mul_assoc`, `one_mul`,
|
||||
`mul_one`, `inv_mul_cancel`, `mul_inv_cancel`.
|
||||
|
||||
Ein Unterschied fällt auf: Das Skript *fordert* die
|
||||
Eindeutigkeit von neutralem Element und Inversen, Mathlib
|
||||
nicht. Das ist kein Widerspruch — die Eindeutigkeit folgt
|
||||
aus den übrigen Axiomen. Genau das beweisen wir jetzt, mit
|
||||
dem Standardargument aus der linearen Algebra:
|
||||
|
||||
*Es sei e ein weiteres Element, das von links neutral wirkt.
|
||||
Weil 1 neutral ist, gilt e·1 = e. Weil e neutral wirkt,
|
||||
gilt e·1 = 1. Zusammen folgt e = e·1 = 1.*
|
||||
-/
|
||||
|
||||
theorem neutral_eindeutig {G : Type*} [Group G] (e : G)
|
||||
(he : ∀ a : G, e * a = a) : e = 1 := by
|
||||
-- „Weil 1 neutral ist, gilt e·1 = e. Weil e neutral
|
||||
-- wirkt, gilt e·1 = 1. Zusammen folgt e = e·1 = 1.“
|
||||
calc e = e * 1 := (mul_one e).symm
|
||||
_ = 1 := he 1
|
||||
|
||||
/-!
|
||||
## Übungsaufgabe
|
||||
|
||||
Zeigen Sie ebenso die Eindeutigkeit des Inversen: Wenn
|
||||
a·b = 1 ist, dann ist b bereits *das* Inverse a⁻¹. Das
|
||||
Standardargument: b = 1·b = (a⁻¹·a)·b = a⁻¹·(a·b) = a⁻¹·1
|
||||
= a⁻¹. Ersetzen Sie das `sorry` durch einen Beweis — die
|
||||
Taktik `calc` aus dem Beweis oben und die Lemmata `one_mul`,
|
||||
`inv_mul_cancel`, `mul_assoc`, `mul_one` genügen.
|
||||
-/
|
||||
|
||||
theorem inverses_eindeutig {G : Type*} [Group G] (a b : G)
|
||||
(h : a * b = 1) : b = a⁻¹ := by
|
||||
sorry
|
||||
|
||||
end AlgebraInLean
|
||||
+201
-158
@@ -1,13 +1,13 @@
|
||||
/-
|
||||
Algebra in Lean — Chapter 18
|
||||
Algebra in Lean — Kapitel 18
|
||||
============================
|
||||
|
||||
This file accompanies the lecture notes "Algebra und Zahlentheorie"
|
||||
(Stefan Kebekus, CC-BY 4.0). It translates the central key lemma
|
||||
(`lem:zsl`) and Cauchy's theorem (`Satz_von_Cauchy`) from Chapter 18
|
||||
into Lean, following the proof of the lecture notes sentence by
|
||||
sentence. The German original of every sentence is quoted as a comment
|
||||
directly above the Lean code that implements it.
|
||||
Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
|
||||
(Stefan Kebekus, CC-BY 4.0). Sie übersetzt das zentrale
|
||||
Schlüssellemma (`lem:zsl`) und den Satz von Cauchy
|
||||
(`Satz_von_Cauchy`) aus Kapitel 18 Satz für Satz nach Lean.
|
||||
Das deutsche Original jedes Beweissatzes steht als Kommentar
|
||||
direkt über dem Lean-Code, der ihn umsetzt.
|
||||
-/
|
||||
import Mathlib
|
||||
|
||||
@@ -16,252 +16,295 @@ namespace AlgebraInLean
|
||||
open Equiv.Perm
|
||||
open Equiv.Perm.VectorsProdEqOne
|
||||
open MulAction
|
||||
open Multiplicative
|
||||
|
||||
/-!
|
||||
# The key lemma and Cauchy's theorem
|
||||
# Das Schlüssellemma und der Satz von Cauchy
|
||||
|
||||
## The key lemma
|
||||
## Das zentrale Schlüssellemma
|
||||
|
||||
**Lemma (Zentrales Schlüssellemma).** *Es sei m ∈ ℕ und es sei p eine
|
||||
Primzahl. Weiter sei G eine Gruppe der Ordnung p^m, die auf einer
|
||||
endlichen Menge M operiert. Weiter sei M₀ = { m ∈ M : ∀ g ∈ G: g·m = m }
|
||||
die Menge der Fixpunkte. Dann ist |M| ≡ |M₀| (mod p).*
|
||||
**Lemma (Zentrales Schlüssellemma).** *Es sei m ∈ ℕ und es
|
||||
sei p eine Primzahl. Weiter sei G eine Gruppe der Ordnung
|
||||
p^m, die auf einer endlichen Menge M operiert. Weiter sei
|
||||
M₀ = { m ∈ M : ∀ g ∈ G: g·m = m } die Menge der Fixpunkte.
|
||||
Dann ist |M| ≡ |M₀| (mod p).*
|
||||
|
||||
How does Mathlib say all this?
|
||||
Wie sagt Mathlib das alles?
|
||||
|
||||
* "eine Gruppe der Ordnung p^m": Mathlib has a predicate `IsPGroup p G`
|
||||
for this ("the order of every element is a power of p" — for finite
|
||||
groups this is equivalent, by Cauchy's theorem below!). The lemma
|
||||
`IsPGroup.of_card` converts our hypothesis `Nat.card G = p ^ m` into
|
||||
it.
|
||||
* „eine Gruppe der Ordnung p^m“: Dafür hat Mathlib ein
|
||||
Prädikat `IsPGroup p G` („die Ordnung jedes Elements ist
|
||||
eine p-Potenz“ — für endliche Gruppen ist das äquivalent,
|
||||
nach dem Satz von Cauchy unten!). Das Lemma
|
||||
`IsPGroup.of_card` übersetzt unsere Voraussetzung
|
||||
`Nat.card G = p ^ m` dorthin.
|
||||
|
||||
* "die auf einer endlichen Menge M operiert": an action of `G` on `M` is
|
||||
a typeclass, `[MulAction G M]`; finiteness of `M` is the typeclass
|
||||
`[Finite M]`.
|
||||
* „die auf einer endlichen Menge M operiert“: Eine Wirkung von
|
||||
`G` auf `M` ist eine Typklasse, `[MulAction G M]`; die
|
||||
Endlichkeit von `M` ist die Typklasse `[Finite M]`.
|
||||
|
||||
* The set of fixed points is `MulAction.fixedPoints G M`, and the
|
||||
congruence `|M| ≡ |M₀| (mod p)` is written
|
||||
* Die Fixpunktmenge heißt `MulAction.fixedPoints G M`, und die
|
||||
Kongruenz |M| ≡ |M₀| (mod p) schreibt sich
|
||||
`Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p]`.
|
||||
|
||||
The proof in the lecture notes decomposes M into orbits and quotes the
|
||||
Bahnengleichung. This is *exactly* how Mathlib proves the statement
|
||||
`IsPGroup.card_modEq_card_fixedPoints` — so here, just as the lecture
|
||||
notes quote Satz 17.2.6, we simply cite the library.
|
||||
Der Beweis im Skript zerlegt M in Bahnen und zitiert die
|
||||
Bahnengleichung. Genau so beweist Mathlib die Aussage
|
||||
`IsPGroup.card_modEq_card_fixedPoints` — wir zitieren hier
|
||||
also einfach die Bibliothek, so wie das Skript an dieser
|
||||
Stelle Satz 17.2.6 zitiert.
|
||||
-/
|
||||
|
||||
theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*} [Group G]
|
||||
(hG : Nat.card G = p ^ m) (M : Type*) [Finite M] [MulAction G M] :
|
||||
theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*}
|
||||
[Group G] (hG : Nat.card G = p ^ m) (M : Type*)
|
||||
[Finite M] [MulAction G M] :
|
||||
Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p] := by
|
||||
have : Fact p.Prime := ⟨hp⟩
|
||||
exact (IsPGroup.of_card hG).card_modEq_card_fixedPoints M
|
||||
|
||||
/-!
|
||||
## Cauchy's theorem
|
||||
## Der Satz von Cauchy
|
||||
|
||||
**Satz (Satz von Cauchy).** *Wenn die Ordnung einer endlichen Gruppe
|
||||
durch p teilbar ist, dann existiert ein Element von Ordnung p.*
|
||||
**Satz (Satz von Cauchy).** *Wenn die Ordnung einer endlichen
|
||||
Gruppe durch p teilbar ist, dann existiert ein Element von
|
||||
Ordnung p.*
|
||||
|
||||
We follow the proof of the lecture notes sentence by sentence. The
|
||||
proof constructs a clever auxiliary set with a clever group action, so
|
||||
this time there is real work to do *before* the final theorem: we set up
|
||||
the set and the action first.
|
||||
Wir folgen dem Beweis des Skripts Satz für Satz. Der Beweis
|
||||
konstruiert eine raffinierte Hilfsmenge mit einer raffinierten
|
||||
Gruppenwirkung — diesmal gibt es also vor dem eigentlichen
|
||||
Satz echte Arbeit: Wir bauen erst die Menge und die Wirkung.
|
||||
|
||||
„Betrachte die Menge M = { (a₁, …, a_p) ∈ G ⨯ ⋯ ⨯ G : a₁·a₂ ⋯ a_p = e }.“
|
||||
„Betrachte die Menge
|
||||
M = { (a₁, …, a_p) ∈ G ⨯ ⋯ ⨯ G : a₁·a₂ ⋯ a_p = e }.“
|
||||
|
||||
Mathlib knows this set. A p-tuple of group elements is a
|
||||
`List.Vector G p` — a list of length p — and M is the set
|
||||
`Equiv.Perm.vectorsProdEqOne G p` of all vectors whose entries multiply
|
||||
to 1.
|
||||
Mathlib kennt diese Menge. Ein p-Tupel von Gruppenelementen
|
||||
ist ein `List.Vector G p` — eine Liste der Länge p —, und M
|
||||
ist die Menge `Equiv.Perm.vectorsProdEqOne G p` aller
|
||||
Vektoren, deren Einträge sich zu 1 multiplizieren.
|
||||
|
||||
„Gegeben ein Tupel (a₁, …, a_p) ∈ M, dann stellen wir erst einmal fest,
|
||||
dass der letzte Eintrag des Tupels durch die ersten Einträge eindeutig
|
||||
bestimmt ist, a_p = (a₁ ⋯ a_{p-1})⁻¹. Wir erhalten die folgende
|
||||
Gleichung: |M| = |G^{p-1}| = |G|^{p-1}.“
|
||||
„Gegeben ein Tupel (a₁, …, a_p) ∈ M, dann stellen wir erst
|
||||
einmal fest, dass der letzte Eintrag des Tupels durch die
|
||||
ersten Einträge eindeutig bestimmt ist,
|
||||
a_p = (a₁ ⋯ a_{p-1})⁻¹. Wir erhalten die folgende Gleichung:
|
||||
|M| = |G^{p-1}| = |G|^{p-1}.“
|
||||
|
||||
This, too, is already in Mathlib: the bijection
|
||||
(a₁, …, a_{p-1}) ↦ (a₁, …, a_{p-1}, (a₁ ⋯ a_{p-1})⁻¹) is
|
||||
`VectorsProdEqOne.vectorEquiv`, and the resulting counting formula is
|
||||
`VectorsProdEqOne.card`:
|
||||
-/
|
||||
Auch das steht schon in Mathlib: Die Bijektion
|
||||
(a₁, …, a_{p-1}) ↦ (a₁, …, a_{p-1}, (a₁ ⋯ a_{p-1})⁻¹) heißt
|
||||
`VectorsProdEqOne.vectorEquiv`, die resultierende Zählformel
|
||||
`VectorsProdEqOne.card`.
|
||||
|
||||
#check @Equiv.Perm.VectorsProdEqOne.card
|
||||
-- ∀ (G : Type u_1) [inst : Group G] (n : ℕ) [inst_1 : Fintype G],
|
||||
-- Fintype.card ↥(vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)
|
||||
„Als Nächstes brauchen wir eine schicke Gruppenwirkung, denn
|
||||
wir wollen das zentrale Schlüssellemma anwenden. Dazu lassen
|
||||
wir die zyklische Gruppe ℤ/(p) auf M durch zyklisches
|
||||
Vertauschen wirken.“
|
||||
|
||||
/-!
|
||||
„Als Nächstes brauchen wir eine schicke Gruppenwirkung, denn wir wollen
|
||||
das zentrale Schlüssellemma anwenden. Dazu lassen wir die zyklische
|
||||
Gruppe ℤ/(p) auf M durch zyklisches Vertauschen wirken.“
|
||||
Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p`
|
||||
um k Stellen ist `VectorsProdEqOne.rotate v k`. Die Fußnote
|
||||
des Skripts — der Shift bildet M auf sich ab, „weil in jeder
|
||||
Gruppe aus a·b = e auch b·a = e gilt“ — ist das Mathlib-Lemma
|
||||
`List.prod_rotate_eq_one_of_prod_eq_one`, das schon in der
|
||||
Definition von `rotate` steckt.
|
||||
|
||||
The cyclic shift of a vector `v ∈ vectorsProdEqOne G p` by k places is
|
||||
`VectorsProdEqOne.rotate v k`. The footnote of the lecture notes — the
|
||||
shift maps M to itself „weil in jeder Gruppe aus a·b = e auch b·a = e
|
||||
gilt“ — is the Mathlib lemma `List.prod_rotate_eq_one_of_prod_eq_one`,
|
||||
which is used in the very definition of `rotate`.
|
||||
|
||||
To let ℤ/(p) act *as a group* we must check the action axioms: rotating
|
||||
by 0 does nothing, and rotating by j + k is the same as rotating by k
|
||||
and then by j. Mathlib provides `rotate_zero`, `rotate_rotate` and
|
||||
`rotate_length` (rotating by the full length p does nothing); from the
|
||||
last one we first derive that rotation only depends on the shift
|
||||
*modulo p* — this is why ℤ/(p), and not just ℕ, acts on M.
|
||||
Damit ℤ/(p) *als Gruppe* wirkt, müssen wir die
|
||||
Wirkungsaxiome nachprüfen: Der Shift um 0 tut nichts, und der
|
||||
Shift um j + k ist der Shift um k gefolgt vom Shift um j.
|
||||
Mathlib stellt `rotate_zero`, `rotate_rotate` und
|
||||
`rotate_length` bereit (der Shift um die volle Länge p tut
|
||||
nichts); daraus leiten wir zuerst ab, dass der Shift nur von
|
||||
der Verschiebung *modulo p* abhängt — genau deshalb wirkt
|
||||
ℤ/(p) und nicht bloß ℕ.
|
||||
-/
|
||||
|
||||
theorem rotate_mul {G : Type*} [Group G] {p : ℕ}
|
||||
(v : vectorsProdEqOne G p) (q : ℕ) : rotate v (p * q) = v := by
|
||||
(v : vectorsProdEqOne G p) (q : ℕ) :
|
||||
rotate v (p * q) = v := by
|
||||
induction q with
|
||||
| zero => rw [Nat.mul_zero, rotate_zero]
|
||||
| succ q ih => rw [Nat.mul_succ, ← rotate_rotate, ih, rotate_length]
|
||||
| succ q ih =>
|
||||
rw [Nat.mul_succ, ← rotate_rotate, ih, rotate_length]
|
||||
|
||||
theorem rotate_mod {G : Type*} [Group G] {p : ℕ}
|
||||
(v : vectorsProdEqOne G p) (k : ℕ) : rotate v (k % p) = rotate v k := by
|
||||
(v : vectorsProdEqOne G p) (k : ℕ) :
|
||||
rotate v (k % p) = rotate v k := by
|
||||
calc rotate v (k % p)
|
||||
= rotate (rotate v (k % p)) (p * (k / p)) := (rotate_mul _ _).symm
|
||||
_ = rotate v (k % p + p * (k / p)) := rotate_rotate _ _ _
|
||||
= rotate (rotate v (k % p)) (p * (k / p)) :=
|
||||
(rotate_mul _ _).symm
|
||||
_ = rotate v (k % p + p * (k / p)) :=
|
||||
rotate_rotate _ _ _
|
||||
_ = rotate v k := by rw [Nat.mod_add_div]
|
||||
|
||||
/-- „Dazu lassen wir die zyklische Gruppe ℤ/(p) auf M durch zyklisches
|
||||
Vertauschen wirken.“ — An element k of ℤ/(p) acts by rotating k places.
|
||||
/-!
|
||||
Nun können wir die Wirkung definieren. Zwei technische
|
||||
Anmerkungen. Mathlibs `MulAction` erwartet eine
|
||||
multiplikativ geschriebene Gruppe; ℤ/(p) = `ZMod p` ist aber
|
||||
additiv geschrieben. Der Wrapper `Multiplicative` wechselt
|
||||
die Notation. Die Voraussetzung `[NeZero p]` schließt p = 0
|
||||
aus, wo „Shift um eine Restklasse“ sinnlos wäre.
|
||||
-/
|
||||
|
||||
Two technical remarks. Mathlib's `MulAction` wants a multiplicatively
|
||||
written group, while ℤ/(p) = `ZMod p` is written additively; the wrapper
|
||||
`Multiplicative` performs the change of notation. The assumption
|
||||
`[NeZero p]` excludes p = 0, where "rotation by a residue class" would
|
||||
make no sense. -/
|
||||
instance rotateAction {G : Type*} [Group G] {p : ℕ} [NeZero p] :
|
||||
MulAction (Multiplicative (ZMod p)) (vectorsProdEqOne G p) where
|
||||
smul k v := rotate v (Multiplicative.toAdd k).val
|
||||
/-- „Dazu lassen wir die zyklische Gruppe ℤ/(p) auf M durch
|
||||
zyklisches Vertauschen wirken.“ — Ein Element k von ℤ/(p)
|
||||
wirkt durch den Shift um k Stellen. -/
|
||||
instance rotateAction {G : Type*} [Group G] {p : ℕ}
|
||||
[NeZero p] :
|
||||
MulAction (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p) where
|
||||
smul k v := rotate v (toAdd k).val
|
||||
one_smul v := by
|
||||
show rotate v (ZMod.val 0) = v
|
||||
rw [ZMod.val_zero, rotate_zero]
|
||||
mul_smul j k v := by
|
||||
show rotate v ((Multiplicative.toAdd j + Multiplicative.toAdd k).val) =
|
||||
rotate (rotate v (Multiplicative.toAdd k).val) (Multiplicative.toAdd j).val
|
||||
rw [ZMod.val_add, rotate_mod, rotate_rotate, Nat.add_comm]
|
||||
show rotate v ((toAdd j + toAdd k).val) =
|
||||
rotate (rotate v (toAdd k).val) (toAdd j).val
|
||||
rw [ZMod.val_add, rotate_mod, rotate_rotate,
|
||||
Nat.add_comm]
|
||||
|
||||
/-!
|
||||
„Die Fixpunktmenge dieser Wirkung ist M₀ = { (a, …, a) ∈ G^p : a^p = e }.“
|
||||
„Die Fixpunktmenge dieser Wirkung ist
|
||||
M₀ = { (a, …, a) ∈ G^p : a^p = e }.“
|
||||
|
||||
In other words: a tuple is a fixed point if and only if it is constant,
|
||||
i.e. its underlying list is `List.replicate p a` — the list (a, …, a) —
|
||||
for some a. (The condition a^p = e then holds automatically, because
|
||||
the entries of a tuple in M multiply to e.) The key step is the lemma
|
||||
`List.rotate_one_eq_self_iff_eq_replicate`: a list that is unchanged by
|
||||
the cyclic shift by *one* place is constant.
|
||||
Mit anderen Worten: Ein Tupel ist genau dann ein Fixpunkt,
|
||||
wenn es konstant ist, seine Liste also für ein a die Liste
|
||||
`List.replicate p a` — das ist (a, …, a) — ist. (Die
|
||||
Bedingung a^p = e gilt dann automatisch, weil sich die
|
||||
Einträge eines Tupels in M zu e multiplizieren.) Der
|
||||
Schlüsselschritt ist das Lemma
|
||||
`List.rotate_one_eq_self_iff_eq_replicate`: Eine Liste, die
|
||||
der zyklische Shift um *eine* Stelle nicht ändert, ist
|
||||
konstant.
|
||||
-/
|
||||
|
||||
theorem mem_fixedPoints_iff_replicate {G : Type*} [Group G] {p : ℕ}
|
||||
[Fact (1 < p)] (v : vectorsProdEqOne G p) :
|
||||
v ∈ fixedPoints (Multiplicative (ZMod p)) (vectorsProdEqOne G p) ↔
|
||||
∃ a : G, (v : List.Vector G p).toList = List.replicate p a := by
|
||||
theorem mem_fixedPoints_iff_replicate {G : Type*} [Group G]
|
||||
{p : ℕ} [Fact (1 < p)] (v : vectorsProdEqOne G p) :
|
||||
v ∈ fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p) ↔
|
||||
∃ a : G,
|
||||
(v : List.Vector G p).toList
|
||||
= List.replicate p a := by
|
||||
rw [mem_fixedPoints]
|
||||
constructor
|
||||
· -- A fixed point is in particular fixed by 1 ∈ ℤ/(p), so it is
|
||||
-- unchanged by the cyclic shift by one place …
|
||||
· -- Ein Fixpunkt wird insbesondere von 1 ∈ ℤ/(p) fixiert,
|
||||
-- bleibt also unter dem Shift um eine Stelle
|
||||
-- unverändert …
|
||||
intro hv
|
||||
have h1 : rotate v 1 = v := by
|
||||
have h := hv (Multiplicative.ofAdd (1 : ZMod p))
|
||||
rwa [show Multiplicative.ofAdd (1 : ZMod p) • v
|
||||
= rotate v (1 : ZMod p).val from rfl, ZMod.val_one] at h
|
||||
-- … and hence constant.
|
||||
obtain ⟨a, ha⟩ := List.rotate_one_eq_self_iff_eq_replicate.mp
|
||||
(Subtype.ext_iff.mp (Subtype.ext_iff.mp h1))
|
||||
have h := hv (ofAdd (1 : ZMod p))
|
||||
rwa [show ofAdd (1 : ZMod p) • v
|
||||
= rotate v (1 : ZMod p).val from rfl,
|
||||
ZMod.val_one] at h
|
||||
-- … und ist daher konstant.
|
||||
obtain ⟨a, ha⟩ :=
|
||||
List.rotate_one_eq_self_iff_eq_replicate.mp
|
||||
(Subtype.ext_iff.mp (Subtype.ext_iff.mp h1))
|
||||
refine ⟨a, ha.trans ?_⟩
|
||||
congr 1
|
||||
exact (v : List.Vector G p).2
|
||||
· -- Conversely, a constant tuple is unchanged by every cyclic shift.
|
||||
· -- Umgekehrt ändert kein zyklischer Shift ein konstantes
|
||||
-- Tupel.
|
||||
rintro ⟨a, ha⟩ g
|
||||
apply Subtype.ext
|
||||
apply Subtype.ext
|
||||
show (v : List.Vector G p).toList.rotate (Multiplicative.toAdd g).val =
|
||||
show (v : List.Vector G p).toList.rotate (toAdd g).val =
|
||||
(v : List.Vector G p).toList
|
||||
rw [ha, List.rotate_replicate]
|
||||
|
||||
/-!
|
||||
Now we can put the pieces together, following the lecture notes line by
|
||||
line.
|
||||
Jetzt setzen wir die Teile zusammen und folgen dem Skript
|
||||
Zeile für Zeile.
|
||||
-/
|
||||
|
||||
theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ} (hp : p.Prime)
|
||||
(hdvd : p ∣ Fintype.card G) : ∃ a : G, orderOf a = p := by
|
||||
-- Register the consequences of primality that instance search needs:
|
||||
theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ}
|
||||
(hp : p.Prime) (hdvd : p ∣ Fintype.card G) :
|
||||
∃ a : G, orderOf a = p := by
|
||||
-- Die Konsequenzen der Primalität, die die Instanzsuche
|
||||
-- braucht:
|
||||
have : Fact p.Prime := ⟨hp⟩
|
||||
have : NeZero p := ⟨hp.ne_zero⟩
|
||||
have : Fact (1 < p) := ⟨hp.one_lt⟩
|
||||
-- „Wir erhalten die folgende Gleichung: |M| = |G^{p-1}| = |G|^{p-1}.“
|
||||
have hM : Nat.card (vectorsProdEqOne G p) = Fintype.card G ^ (p - 1) := by
|
||||
-- Abkürzung: M₀ ist die Fixpunktmenge der Wirkung.
|
||||
set M₀ := fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)
|
||||
-- „Wir erhalten die folgende Gleichung:
|
||||
-- |M| = |G^{p-1}| = |G|^{p-1}.“
|
||||
have hM : Nat.card (vectorsProdEqOne G p)
|
||||
= Fintype.card G ^ (p - 1) := by
|
||||
rw [Nat.card_eq_fintype_card, VectorsProdEqOne.card]
|
||||
-- „Die zyklische Gruppe ℤ/(p)“ has order p = p¹, so the key lemma
|
||||
-- applies to the rotation action and gives |M| ≡ |M₀| (mod p):
|
||||
have hZp : Nat.card (Multiplicative (ZMod p)) = p ^ 1 := by
|
||||
-- Die zyklische Gruppe ℤ/(p) hat Ordnung p = p¹; das
|
||||
-- Schlüssellemma, angewandt auf die Rotationswirkung,
|
||||
-- liefert |M| ≡ |M₀| (mod p):
|
||||
have hZp :
|
||||
Nat.card (Multiplicative (ZMod p)) = p ^ 1 := by
|
||||
simp [Nat.card_eq_fintype_card]
|
||||
have hcong :
|
||||
Nat.card (vectorsProdEqOne G p) ≡
|
||||
Nat.card (fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)) [MOD p] :=
|
||||
Nat.card M₀ [MOD p] :=
|
||||
key_lemma hp hZp (vectorsProdEqOne G p)
|
||||
-- „Auf der anderen Seite folgt aus dem zentralen Schlüssellemma, dass
|
||||
-- „Auf der anderen Seite folgt aus dem zentralen
|
||||
-- Schlüssellemma, dass
|
||||
-- |M₀| ≡ |M| ≡ |G|^{p-1} ≡ 0 (mod p) ist.“
|
||||
have hdvdM0 : p ∣ Nat.card (fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)) := by
|
||||
have hdvdM0 : p ∣ Nat.card M₀ := by
|
||||
have hp1 : p - 1 ≠ 0 := by have := hp.one_lt; omega
|
||||
have h0 : (0 : ℕ) ≡ Nat.card (fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)) [MOD p] :=
|
||||
have h0 : (0 : ℕ) ≡ Nat.card M₀ [MOD p] :=
|
||||
calc (0 : ℕ)
|
||||
≡ Fintype.card G ^ (p - 1) [MOD p] :=
|
||||
(Nat.modEq_zero_iff_dvd.mpr (dvd_pow hdvd hp1)).symm
|
||||
(Nat.modEq_zero_iff_dvd.mpr
|
||||
(dvd_pow hdvd hp1)).symm
|
||||
_ = Nat.card (vectorsProdEqOne G p) := hM.symm
|
||||
_ ≡ _ [MOD p] := hcong
|
||||
_ ≡ Nat.card M₀ [MOD p] := hcong
|
||||
exact Nat.modEq_zero_iff_dvd.mp h0.symm
|
||||
-- „Wegen (e, …, e) ∈ M₀ ist schon einmal klar, dass M₀ ≠ ∅ ist.“
|
||||
-- „Wegen (e, …, e) ∈ M₀ ist schon einmal klar, dass
|
||||
-- M₀ ≠ ∅ ist.“
|
||||
let v₀ : vectorsProdEqOne G p :=
|
||||
⟨List.Vector.replicate p 1, (List.prod_replicate p 1).trans (one_pow p)⟩
|
||||
have hv₀ : v₀ ∈ fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p) :=
|
||||
⟨List.Vector.replicate p 1,
|
||||
(List.prod_replicate p 1).trans (one_pow p)⟩
|
||||
have hv₀ : v₀ ∈ M₀ :=
|
||||
(mem_fixedPoints_iff_replicate v₀).mpr ⟨1, rfl⟩
|
||||
-- M₀ is nonempty and its cardinality is divisible by p ≥ 2, so
|
||||
-- |M₀| ≥ p > 1 …
|
||||
have := Fintype.ofFinite (fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p))
|
||||
have hlt : 1 < Fintype.card (fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)) := by
|
||||
-- M₀ ist nichtleer, und |M₀| ist durch p ≥ 2 teilbar,
|
||||
-- also ist |M₀| ≥ p > 1 …
|
||||
have := Fintype.ofFinite M₀
|
||||
have hlt : 1 < Fintype.card M₀ := by
|
||||
rw [← Nat.card_eq_fintype_card]
|
||||
have hpos : 0 < Nat.card (fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)) := Nat.card_pos_iff.mpr ⟨⟨⟨v₀, hv₀⟩⟩, inferInstance⟩
|
||||
have hpos : 0 < Nat.card M₀ :=
|
||||
Nat.card_pos_iff.mpr ⟨⟨⟨v₀, hv₀⟩⟩, inferInstance⟩
|
||||
have := Nat.le_of_dvd hpos hdvdM0
|
||||
have := hp.one_lt
|
||||
omega
|
||||
-- „Also existiert mindestens ein a ≠ e mit a^p = e.“
|
||||
obtain ⟨w, hw⟩ := Fintype.exists_ne_of_one_lt_card hlt ⟨v₀, hv₀⟩
|
||||
obtain ⟨a, ha⟩ := (mem_fixedPoints_iff_replicate w.1).mp w.2
|
||||
-- The tuple w lies in M, so its entries multiply to e; being constant,
|
||||
-- this says exactly a^p = e:
|
||||
obtain ⟨w, hw⟩ :=
|
||||
Fintype.exists_ne_of_one_lt_card hlt ⟨v₀, hv₀⟩
|
||||
obtain ⟨a, ha⟩ :=
|
||||
(mem_fixedPoints_iff_replicate w.1).mp w.2
|
||||
-- Das Tupel w liegt in M, sein Produkt ist also e; weil
|
||||
-- das Tupel konstant ist, heißt das genau a^p = e:
|
||||
have hpow : a ^ p = 1 := by
|
||||
have hprod : (w.1 : List.Vector G p).toList.prod = 1 := w.1.2
|
||||
have hprod : (w.1 : List.Vector G p).toList.prod = 1 :=
|
||||
w.1.2
|
||||
rwa [ha, List.prod_replicate] at hprod
|
||||
-- and a ≠ e, because otherwise w would be the tuple (e, …, e) = v₀:
|
||||
-- Und a ≠ e, denn sonst wäre w das Tupel (e, …, e) = v₀:
|
||||
have hne : a ≠ 1 := by
|
||||
rintro rfl
|
||||
exact hw (Subtype.ext (Subtype.ext (Subtype.ext ha)))
|
||||
-- „Nach Satz 17.4.11 hat a dann automatisch die Ordnung p.“
|
||||
-- „Nach Satz 17.4.11 hat a dann automatisch die
|
||||
-- Ordnung p.“
|
||||
exact ⟨a, orderOf_eq_prime hpow hne⟩
|
||||
|
||||
/-!
|
||||
## Remarks
|
||||
## Bemerkungen
|
||||
|
||||
1. Mathlib's version of Cauchy's theorem is
|
||||
`exists_prime_orderOf_dvd_card`; its proof is the same
|
||||
counting argument, organized slightly differently.
|
||||
1. Mathlibs Fassung des Satzes von Cauchy heißt
|
||||
`exists_prime_orderOf_dvd_card`; ihr Beweis ist dasselbe
|
||||
Zählargument, nur etwas anders organisiert.
|
||||
|
||||
2. **Exercise** (Satz 18.2.3 of the lecture notes): *Es sei p eine
|
||||
Primzahl und G eine nichttriviale Gruppe, deren Ordnung eine p-Potenz
|
||||
ist. Dann ist das Zentrum von G nicht trivial.* Prove this in Lean:
|
||||
apply `key_lemma` to the conjugation action of G on itself — or find
|
||||
the statement in Mathlib. Replace the `sorry` below by a proof.
|
||||
2. **Übungsaufgabe** (Satz 18.2.3 im Skript): *Es sei p eine
|
||||
Primzahl und G eine nichttriviale Gruppe, deren Ordnung
|
||||
eine p-Potenz ist. Dann ist das Zentrum von G nicht
|
||||
trivial.* Beweisen Sie das in Lean: Wenden Sie
|
||||
`key_lemma` auf die Konjugationswirkung von G auf sich
|
||||
selbst an — oder finden Sie die Aussage in Mathlib.
|
||||
Ersetzen Sie dazu das `sorry` durch einen Beweis.
|
||||
-/
|
||||
|
||||
theorem center_nontrivial {p m : ℕ} (hp : p.Prime) {G : Type*} [Group G]
|
||||
[Finite G] (hm : m ≠ 0) (hG : Nat.card G = p ^ m) :
|
||||
theorem center_nontrivial {p m : ℕ} (hp : p.Prime)
|
||||
{G : Type*} [Group G] [Finite G] (hm : m ≠ 0)
|
||||
(hG : Nat.card G = p ^ m) :
|
||||
Nontrivial (Subgroup.center G) := by
|
||||
sorry
|
||||
|
||||
|
||||
@@ -1,104 +1,120 @@
|
||||
/-
|
||||
Algebra in Lean — pilot file
|
||||
Algebra in Lean — Kapitel 17
|
||||
============================
|
||||
|
||||
This file accompanies the lecture notes "Algebra und Zahlentheorie"
|
||||
(Stefan Kebekus, CC-BY 4.0). It translates one theorem of the notes —
|
||||
Fermat's little theorem, `satz:kleinerFermat` in Chapter 17 — into Lean,
|
||||
following the proof of the lecture notes *sentence by sentence*. The
|
||||
German original of every sentence is quoted as a comment directly above
|
||||
the Lean code that implements it, so you can see how the standard
|
||||
phrases of a lecture-style proof translate into Lean/Mathlib.
|
||||
Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
|
||||
(Stefan Kebekus, CC-BY 4.0). Sie übersetzt einen Satz des
|
||||
Skripts — den kleinen Satz von Fermat, `satz:kleinerFermat` in
|
||||
Kapitel 17 — Satz für Satz nach Lean. Das deutsche Original
|
||||
jedes Beweissatzes steht als Kommentar direkt über dem
|
||||
Lean-Code, der ihn umsetzt: So sieht man, wie sich die
|
||||
Standardphrasen eines Vorlesungsbeweises nach Lean/Mathlib
|
||||
übersetzen.
|
||||
-/
|
||||
import Mathlib
|
||||
|
||||
namespace AlgebraInLean
|
||||
|
||||
/-!
|
||||
# Fermat's little theorem
|
||||
# Der kleine Satz von Fermat
|
||||
|
||||
**Satz (Kleiner Satz von Fermat).** *Es sei p ∈ ℕ eine Primzahl und es
|
||||
sei a ∈ ℤ irgendeine Zahl. Dann ist a^p ≡ a (mod p).*
|
||||
**Satz (Kleiner Satz von Fermat).** *Es sei p ∈ ℕ eine
|
||||
Primzahl und es sei a ∈ ℤ irgendeine Zahl. Dann ist
|
||||
a^p ≡ a (mod p).*
|
||||
|
||||
Before we can state this in Lean, we need to know how Mathlib speaks
|
||||
about the objects involved.
|
||||
Bevor wir das in Lean formulieren können, müssen wir wissen,
|
||||
wie Mathlib über die beteiligten Objekte spricht.
|
||||
|
||||
* The ring ℤ/(p) of residue classes is called `ZMod p`. The residue
|
||||
class of an integer `a : ℤ` is written `(a : ZMod p)` — Lean inserts
|
||||
the canonical ring morphism ℤ → ℤ/(p) automatically ("coercion").
|
||||
* Der Restklassenring ℤ/(p) heißt `ZMod p`. Die Restklasse
|
||||
einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)` —
|
||||
Lean fügt den kanonischen Ringmorphismus ℤ → ℤ/(p)
|
||||
automatisch ein („Koerzion“).
|
||||
|
||||
* The congruence `a ≡ b (mod p)` for integers is written
|
||||
* Die Kongruenz a ≡ b (mod p) für ganze Zahlen schreibt sich
|
||||
`a ≡ b [ZMOD p]`.
|
||||
|
||||
* The multiplicative group 𝔽_p^* is the group of *units* of the ring
|
||||
`ZMod p`, written `(ZMod p)ˣ`. A unit `u : (ZMod p)ˣ` remembers its
|
||||
inverse; the underlying ring element is again written `(u : ZMod p)`.
|
||||
* Die multiplikative Gruppe 𝔽_p^* ist die Gruppe der
|
||||
*Einheiten* des Rings `ZMod p`, geschrieben `(ZMod p)ˣ`.
|
||||
Eine Einheit `u : (ZMod p)ˣ` kennt ihr Inverses; das
|
||||
zugrundeliegende Ringelement schreibt sich wieder
|
||||
`(u : ZMod p)`.
|
||||
|
||||
* The lecture notes say "es sei p eine Primzahl". In Lean we carry the
|
||||
primality of `p` as a hypothesis `hp : p.Prime`. Some facts —
|
||||
for instance that ℤ/(p) is a field — are found by Lean's automation
|
||||
only if the hypothesis is registered as an *instance*; this is what
|
||||
the first line `have : Fact p.Prime := ⟨hp⟩` of the proof does.
|
||||
* Das Skript sagt „es sei p eine Primzahl“. In Lean führen
|
||||
wir die Primalität von `p` als Hypothese `hp : p.Prime` mit.
|
||||
Manche Tatsachen — etwa dass ℤ/(p) ein Körper ist — findet
|
||||
Leans Automatisierung nur, wenn die Hypothese als *Instanz*
|
||||
registriert ist; genau das leistet die erste Beweiszeile
|
||||
`have : Fact p.Prime := ⟨hp⟩`.
|
||||
-/
|
||||
|
||||
theorem little_fermat (p : ℕ) (hp : p.Prime) (a : ℤ) :
|
||||
a ^ p ≡ a [ZMOD p] := by
|
||||
have : Fact p.Prime := ⟨hp⟩
|
||||
-- The congruence „a^p ≡ a (mod p)“ means precisely that a^p and a have
|
||||
-- the same residue class in ℤ/(p). So we may prove an *equation* in
|
||||
-- the ring `ZMod p` instead; the goal becomes
|
||||
-- Die Kongruenz „a^p ≡ a (mod p)“ bedeutet gerade, dass
|
||||
-- a^p und a dieselbe Restklasse in ℤ/(p) haben. Wir
|
||||
-- dürfen also stattdessen eine *Gleichung* im Ring
|
||||
-- `ZMod p` zeigen; das Beweisziel wird
|
||||
-- (a : ZMod p) ^ p = (a : ZMod p).
|
||||
rw [← ZMod.intCast_eq_intCast_iff]
|
||||
push_cast
|
||||
-- „Falls a ein Vielfaches von p ist, ist die Sache klar.“
|
||||
by_cases ha : (a : ZMod p) = 0
|
||||
· rw [ha, zero_pow hp.ne_zero]
|
||||
-- „Ansonsten liefert die Restklasse von a ein nicht-verschwindendes
|
||||
-- Element ā ∈ ℤ/(p) = 𝔽_p, also ein Element der multiplikativen
|
||||
-- Gruppe 𝔽_p^*, …“
|
||||
· obtain ⟨u, hu⟩ : IsUnit (a : ZMod p) := isUnit_iff_ne_zero.mpr ha
|
||||
-- „Ansonsten liefert die Restklasse von a ein
|
||||
-- nicht-verschwindendes Element ā ∈ ℤ/(p) = 𝔽_p, also
|
||||
-- ein Element der multiplikativen Gruppe 𝔽_p^*, …“
|
||||
· obtain ⟨u, hu⟩ : IsUnit (a : ZMod p) :=
|
||||
isUnit_iff_ne_zero.mpr ha
|
||||
rw [← hu]
|
||||
-- „… welche p−1 Elemente hat.“
|
||||
have card_units : Nat.card (ZMod p)ˣ = p - 1 := by
|
||||
rw [Nat.card_eq_fintype_card, ZMod.card_units p]
|
||||
-- „Nach Satz 17.3.6 («Satz von Lagrange») ist die Ordnung von ā, also
|
||||
-- die Größe der von ā erzeugten Untergruppe, ein Teiler von
|
||||
-- |𝔽_p^*| = p−1.“
|
||||
have lagrange : Nat.card (Subgroup.zpowers u) ∣ Nat.card (ZMod p)ˣ :=
|
||||
-- „Nach Satz 17.3.6 («Satz von Lagrange») ist die
|
||||
-- Ordnung von ā, also die Größe der von ā erzeugten
|
||||
-- Untergruppe, ein Teiler von |𝔽_p^*| = p−1.“
|
||||
have lagrange :
|
||||
Nat.card (Subgroup.zpowers u) ∣
|
||||
Nat.card (ZMod p)ˣ :=
|
||||
Subgroup.card_subgroup_dvd_card (Subgroup.zpowers u)
|
||||
have ord_dvd : orderOf u ∣ p - 1 := by
|
||||
rw [← Nat.card_zpowers, ← card_units]
|
||||
exact lagrange
|
||||
-- „Es gilt also ā^(p−1) = 1 ∈ 𝔽_p^* …“
|
||||
have pow_eq_one : u ^ (p - 1) = 1 := orderOf_dvd_iff_pow_eq_one.mp ord_dvd
|
||||
have pow_eq_one : u ^ (p - 1) = 1 :=
|
||||
orderOf_dvd_iff_pow_eq_one.mp ord_dvd
|
||||
-- „… oder äquivalent a^p ≡ a (mod p).“
|
||||
have key : u ^ p = u := by
|
||||
calc u ^ p = u ^ (p - 1 + 1) := by rw [Nat.sub_add_cancel hp.one_lt.le]
|
||||
calc u ^ p
|
||||
= u ^ (p - 1 + 1) := by
|
||||
rw [Nat.sub_add_cancel hp.one_lt.le]
|
||||
_ = u ^ (p - 1) * u := pow_succ u (p - 1)
|
||||
_ = u := by rw [pow_eq_one, one_mul]
|
||||
exact_mod_cast congrArg Units.val key
|
||||
|
||||
/-!
|
||||
## Remarks
|
||||
## Bemerkungen
|
||||
|
||||
1. Mathlib of course already contains Fermat's little theorem; the
|
||||
statement about residue classes is `ZMod.pow_card`. You can find
|
||||
such lemmas yourself with the tactic `exact?`, or by searching on
|
||||
https://leansearch.net or https://loogle.lean-lang.org.
|
||||
1. Mathlib enthält den kleinen Satz von Fermat natürlich
|
||||
längst; die Aussage über Restklassen heißt `ZMod.pow_card`.
|
||||
Solche Lemmata findet man selbst mit der Taktik `exact?`
|
||||
oder über die Suchmaschinen https://leansearch.net und
|
||||
https://loogle.lean-lang.org.
|
||||
-/
|
||||
|
||||
example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a :=
|
||||
ZMod.pow_card a
|
||||
|
||||
/-!
|
||||
2. **Exercise** (this is `bem:kleinerFermat` of the lecture notes).
|
||||
In applications one often uses the equivalent formulation
|
||||
a^(p−1) ≡ 1 (mod p) for a not divisible by p. Derive it from
|
||||
`little_fermat` — or give a direct proof following the ideas above.
|
||||
Replace the `sorry` below by a proof.
|
||||
2. **Übungsaufgabe** (das ist `bem:kleinerFermat` im Skript).
|
||||
In Anwendungen verwendet man häufig die äquivalente
|
||||
Formulierung a^(p−1) ≡ 1 (mod p) für nicht durch p
|
||||
teilbare a. Leiten Sie sie aus `little_fermat` ab — oder
|
||||
geben Sie einen direkten Beweis nach den Ideen oben.
|
||||
Ersetzen Sie dazu das `sorry` durch einen Beweis.
|
||||
-/
|
||||
|
||||
theorem little_fermat' (p : ℕ) (hp : p.Prime) (a : ℤ) (ha : ¬ (p : ℤ) ∣ a) :
|
||||
theorem little_fermat' (p : ℕ) (hp : p.Prime) (a : ℤ)
|
||||
(ha : ¬ (p : ℤ) ∣ a) :
|
||||
a ^ (p - 1) ≡ 1 [ZMOD p] := by
|
||||
sorry
|
||||
|
||||
|
||||
@@ -0,0 +1,141 @@
|
||||
/-
|
||||
Algebra in Lean — Kapitel 2 und 17 des Skripts
|
||||
==============================================
|
||||
|
||||
Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
|
||||
(Stefan Kebekus, CC-BY 4.0). Sie übersetzt zwei Beweise
|
||||
rund um normale Untergruppen Satz für Satz nach Lean: das
|
||||
Argument aus Erklärvideo 1-1, dass Kerne von
|
||||
Gruppenmorphismen abgeschlossen unter Konjugation sind, und
|
||||
die Beobachtung aus Kapitel 17.3, dass U·N für normales N
|
||||
wieder eine Untergruppe ist.
|
||||
-/
|
||||
import Mathlib
|
||||
|
||||
namespace AlgebraInLean
|
||||
|
||||
/-!
|
||||
# Gruppen und Restklassengruppen
|
||||
|
||||
## Das Mathlib-Wörterbuch
|
||||
|
||||
* Eine Untergruppe von `G` ist ein Term `U : Subgroup G`;
|
||||
die Mitgliedschaft schreibt sich `g ∈ U`. Dass `U` unter
|
||||
Verknüpfung und Inversen abgeschlossen ist, sagen
|
||||
`U.mul_mem` und `U.inv_mem`.
|
||||
|
||||
* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein
|
||||
„Bündel“ aus der Abbildung und den Nachweisen
|
||||
`map_mul : φ (a·b) = φ a · φ b` (daraus folgen
|
||||
`map_one` und `map_inv`). Der Kern heißt `φ.ker`;
|
||||
Mitgliedschaft entpackt `MonoidHom.mem_ker : g ∈ φ.ker ↔
|
||||
φ g = 1`.
|
||||
|
||||
* „N ist Normalteiler“ ist das Prädikat `N.Normal`; sein
|
||||
Feld `conj_mem` ist wörtlich die Bedingung des Skripts:
|
||||
für alle n ∈ N und alle g ist g·n·g⁻¹ ∈ N.
|
||||
|
||||
## Kerne sind abgeschlossen unter Konjugation
|
||||
|
||||
Aus Erklärvideo 1-1 des Skripts: „Die Antwort lautet: Nein!
|
||||
Nicht jede Untergruppe kann Kern eines Gruppenmorphismus
|
||||
sein. Wenn es nämlich einen Gruppenmorphismus φ : G → Q
|
||||
mit H = ker(φ) gibt, dann gilt für alle h ∈ H und alle
|
||||
g ∈ G die Gleichung φ(g·h·g⁻¹) = φ(g)·φ(h)·φ(g)⁻¹ = e,
|
||||
wobei e das neutrale Element von Q bezeichnet. Also ist
|
||||
stets g·h·g⁻¹ ∈ H.“
|
||||
-/
|
||||
|
||||
theorem kern_konjugation {G Q : Type*} [Group G] [Group Q]
|
||||
(φ : G →* Q) {h : G} (hh : h ∈ φ.ker) (g : G) :
|
||||
g * h * g⁻¹ ∈ φ.ker := by
|
||||
-- Mitgliedschaft im Kern heißt: φ bildet auf 1 ab.
|
||||
rw [MonoidHom.mem_ker] at hh ⊢
|
||||
-- „… dann gilt für alle h ∈ H und alle g ∈ G die
|
||||
-- Gleichung φ(g·h·g⁻¹) = φ(g)·φ(h)·φ(g)⁻¹ = e …“
|
||||
calc φ (g * h * g⁻¹)
|
||||
= φ g * φ h * (φ g)⁻¹ := by
|
||||
rw [map_mul, map_mul, map_inv]
|
||||
_ = φ g * 1 * (φ g)⁻¹ := by rw [hh]
|
||||
_ = 1 := by rw [mul_one, mul_inv_cancel]
|
||||
|
||||
/-!
|
||||
Mathlib kennt diese Aussage als Instanz
|
||||
`MonoidHom.normal_ker : φ.ker.Normal`. Das Skript fährt
|
||||
fort: Untergruppen mit dieser Eigenschaft heißen *normale
|
||||
Untergruppen* oder *Normalteiler*, und die Bedingung ist
|
||||
nicht nur notwendig, sondern auch hinreichend — zu jedem
|
||||
Normalteiler existiert eine Restklassengruppe.
|
||||
|
||||
## Die Restklassengruppe und ihre universelle Eigenschaft
|
||||
|
||||
Das Skript definiert die Restklassengruppe in Kapitel 17.3
|
||||
über ihre universelle Eigenschaft. Mathlib stellt beides
|
||||
bereit: den Quotienten `G ⧸ N` mit der Quotientenabbildung
|
||||
`QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle
|
||||
Eigenschaft als `QuotientGroup.lift` — gegeben ein
|
||||
Morphismus `α : G →* H` mit `N ≤ α.ker` erhält man den
|
||||
induzierten Morphismus auf dem Quotienten:
|
||||
-/
|
||||
|
||||
example {G H : Type*} [Group G] [Group H] (N : Subgroup G)
|
||||
[N.Normal] (α : G →* H) (hα : N ≤ α.ker) :
|
||||
G ⧸ N →* H :=
|
||||
QuotientGroup.lift N α
|
||||
fun _g hg => MonoidHom.mem_ker.mp (hα hg)
|
||||
|
||||
/-!
|
||||
## Die Beobachtung: U·N ist eine Untergruppe
|
||||
|
||||
Beobachtung aus Kapitel 17.3 des Skripts: „Es sei G eine
|
||||
Gruppe und es sei N ⊂ G eine normale Untergruppe. Weiter
|
||||
sei U ⊂ G irgendeine Untergruppe. Dann ist
|
||||
U·N = {u·n : u ∈ U, n ∈ N} wieder eine Untergruppe. Zum
|
||||
Beweis müssen wir lediglich zeigen, dass U·N abgeschlossen
|
||||
unter der Gruppenoperation ist. … Wir wissen, dass N
|
||||
normal ist. Also ist ñ₁ := u₂⁻¹·n₁·u₂ ∈ N und es gilt
|
||||
n₁·u₂ = u₂·ñ₁. Demnach ist u₁n₁u₂n₂ = u₁u₂·ñ₁n₂ ∈ U·N.
|
||||
Fertig ist der Beweis.“
|
||||
|
||||
Neu ist hier die Taktik `group`: Sie verrechnet Ausdrücke,
|
||||
die allein mit den Gruppenaxiomen ineinander umgeformt
|
||||
werden können. (Das ñ₁ des Skripts heißt im Code `n₁'`.)
|
||||
-/
|
||||
|
||||
theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
|
||||
(hN : N.Normal) {u₁ n₁ u₂ n₂ : G}
|
||||
(hu₁ : u₁ ∈ U) (hn₁ : n₁ ∈ N)
|
||||
(hu₂ : u₂ ∈ U) (hn₂ : n₂ ∈ N) :
|
||||
∃ u ∈ U, ∃ n ∈ N, u₁ * n₁ * (u₂ * n₂) = u * n := by
|
||||
-- „Wir wissen, dass N normal ist. Also ist
|
||||
-- ñ₁ := u₂⁻¹·n₁·u₂ ∈ N …“
|
||||
set n₁' := u₂⁻¹ * n₁ * u₂ with hn₁'_def
|
||||
have hn₁' : n₁' ∈ N := hN.conj_mem' n₁ hn₁ u₂
|
||||
-- „… und es gilt n₁·u₂ = u₂·ñ₁.“
|
||||
have hswap : n₁ * u₂ = u₂ * n₁' := by
|
||||
rw [hn₁'_def]; group
|
||||
-- „Demnach ist u₁n₁u₂n₂ = u₁u₂·ñ₁n₂ ∈ U·N.“
|
||||
refine ⟨u₁ * u₂, U.mul_mem hu₁ hu₂,
|
||||
n₁' * n₂, N.mul_mem hn₁' hn₂, ?_⟩
|
||||
calc u₁ * n₁ * (u₂ * n₂)
|
||||
= u₁ * (n₁ * u₂) * n₂ := by group
|
||||
_ = u₁ * (u₂ * n₁') * n₂ := by rw [hswap]
|
||||
_ = u₁ * u₂ * (n₁' * n₂) := by group
|
||||
|
||||
/-!
|
||||
## Übungsaufgabe
|
||||
|
||||
Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit
|
||||
unter der Verknüpfung zu zeigen — prüfen Sie den
|
||||
verschwiegenen Teil selbst nach: U·N ist auch abgeschlossen
|
||||
unter Inversen. Tipp: (u·n)⁻¹ = u⁻¹·(u·n⁻¹·u⁻¹), und der
|
||||
zweite Faktor liegt nach `conj_mem` in N. Ersetzen Sie das
|
||||
`sorry` durch einen Beweis.
|
||||
-/
|
||||
|
||||
theorem inv_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
|
||||
(hN : N.Normal) {u n : G} (hu : u ∈ U) (hn : n ∈ N) :
|
||||
∃ u' ∈ U, ∃ n' ∈ N, (u * n)⁻¹ = u' * n' := by
|
||||
sorry
|
||||
|
||||
end AlgebraInLean
|
||||
@@ -0,0 +1,65 @@
|
||||
-- Wurzeldokument der Kursnotizen: `lake exe algebrainlean
|
||||
-- --output _out` rendert sie nach `_out/html-multi`.
|
||||
import VersoManual
|
||||
|
||||
import Book.Basics
|
||||
import Book.Quotients
|
||||
import Book.LittleFermat
|
||||
import Book.Cauchy
|
||||
|
||||
open Verso.Genre Manual
|
||||
|
||||
#doc (Manual) "Algebra in Lean" =>
|
||||
%%%
|
||||
tag := "algebra-in-lean"
|
||||
authors := ["Stefan Kebekus"]
|
||||
%%%
|
||||
|
||||
Dies sind Kursnotizen zum Formalisieren von Algebra mit dem
|
||||
interaktiven Theorembeweiser [Lean](https://lean-lang.org) und seiner
|
||||
Mathematikbibliothek [Mathlib](https://leanprover-community.github.io).
|
||||
Sie begleiten die Vorlesung _Algebra und Zahlentheorie_ (Universität
|
||||
Freiburg, Winter 2026/27) mit ihrem deutschsprachigen Skript und sind
|
||||
dafür gedacht, parallel zum Kurs
|
||||
[_Interactive Theorem Proving using Lean_](https://pfaffelh.github.io/leancourse/)
|
||||
von Peter Pfaffelhuber gelesen zu werden, der Lean selbst einführt.
|
||||
Wir gehen hier den komplementären Weg: Wir nehmen an, dass Sie gerade
|
||||
die _Algebra_ lernen, und zeigen an Beispielen, dass sich der Stoff der
|
||||
Vorlesung mit vertretbarem Aufwand formalisieren lässt — und dass das
|
||||
sogar richtig Spaß machen kann.
|
||||
|
||||
*Wie diese Notizen funktionieren.* Ausgewählte Beweise aus dem Skript
|
||||
werden _Satz für Satz_ nach Lean übersetzt: Jeder deutsche Originalsatz
|
||||
steht als Kommentar direkt über dem Lean-Code, der ihn umsetzt. Sie
|
||||
werden sehen, dass die Standardphrasen eines Vorlesungsbeweises —
|
||||
„Ansonsten liefert die Restklasse …“, „Nach dem Satz von Lagrange …“,
|
||||
„Also existiert mindestens ein …“ — wiedererkennbaren Zügen in Lean
|
||||
entsprechen. Jedes Kapitel endet mit einer Übungsaufgabe, deren
|
||||
`sorry` Sie durch einen Beweis ersetzen sollen.
|
||||
|
||||
*Woher bekomme ich das Material?* Die Übungsdateien liegen im selben
|
||||
Repository wie diese Notizen, im Ordner `AlgebraInLean/`:
|
||||
|
||||
```
|
||||
git clone https://git.cplx.vm.uni-freiburg.de/kebekus/AlgebraInLean.git
|
||||
cd AlgebraInLean
|
||||
lake exe cache get
|
||||
code .
|
||||
```
|
||||
|
||||
Öffnen Sie dann zum Beispiel `AlgebraInLean/LittleFermat.lean`.
|
||||
Warten Sie, bis die orangefarbenen Balken verschwinden; setzen Sie den
|
||||
Cursor in einen Beweis und beobachten Sie, wie das _Infoview_-Panel
|
||||
den aktuellen Beweiszustand anzeigt. Für die Installation von Lean
|
||||
und VS Code selbst folgen Sie der
|
||||
[Anleitung der Lean-Community](https://leanprover-community.github.io/get_started.html)
|
||||
oder der ausführlichen Anleitung am Anfang der
|
||||
[Notizen von Peter Pfaffelhuber](https://pfaffelh.github.io/leancourse/).
|
||||
|
||||
{include 0 Book.Basics}
|
||||
|
||||
{include 0 Book.Quotients}
|
||||
|
||||
{include 0 Book.LittleFermat}
|
||||
|
||||
{include 0 Book.Cauchy}
|
||||
@@ -0,0 +1,100 @@
|
||||
import VersoManual
|
||||
import Manual.Meta
|
||||
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
|
||||
-- `#min_imports`, ergänzt um Taktik-Module und ℚ.
|
||||
import Mathlib.Algebra.Group.Basic
|
||||
import Mathlib.Data.Rat.Defs
|
||||
import Mathlib.Tactic.Ring
|
||||
import Mathlib.Tactic.NormNum
|
||||
|
||||
open Verso.Genre Manual
|
||||
open Verso.Genre.Manual.InlineLean
|
||||
|
||||
set_option pp.rawOnError true
|
||||
set_option verso.docstring.allowMissing true
|
||||
|
||||
#doc (Manual) "Erste Schritte" =>
|
||||
%%%
|
||||
htmlSplit := .never
|
||||
tag := "erste-schritte"
|
||||
%%%
|
||||
|
||||
Ein Beweis in Lean beginnt mit `by` und besteht aus _Taktiken_.
|
||||
Öffnen Sie die Übungsdatei `AlgebraInLean/Basics.lean`, setzen Sie den
|
||||
Cursor in einen Beweis und beobachten Sie das _Infoview_-Panel: Es
|
||||
zeigt zu jedem Zeitpunkt die Hypothesen und das noch zu zeigende Ziel.
|
||||
|
||||
# Vier Taktiken für den Anfang
|
||||
|
||||
* `norm_num` verrechnet konkrete Zahlen,
|
||||
* `ring` beweist Gleichungen, die in jedem kommutativen Ring gelten,
|
||||
* `omega` löst lineare Arithmetik über `ℕ` und `ℤ`,
|
||||
* `rw [h]` schreibt mit einer Gleichung `h` um.
|
||||
|
||||
```lean
|
||||
example : 2 + 3 = 5 := by norm_num
|
||||
|
||||
example (a b : ℤ) :
|
||||
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
|
||||
ring
|
||||
|
||||
example (n : ℕ) (h : n < 5) : n ≤ 7 := by omega
|
||||
|
||||
example (x y : ℚ) (h : x = y) : x + 1 = y + 1 := by
|
||||
rw [h]
|
||||
```
|
||||
|
||||
# Gruppen in Mathlib
|
||||
|
||||
Definition 2.1.1 des Skripts:
|
||||
|
||||
> *Definition (Gruppe).* Eine Gruppe ist eine nicht-leere Menge `G`
|
||||
> mit einer Abbildung `m : G ⨯ G → G`, sodass folgende Eigenschaften
|
||||
> gelten. _Assoziativität:_ … _Neutrales Element:_ Es gibt genau ein
|
||||
> Element `e` aus `G`, sodass für alle `a` aus `G` gilt:
|
||||
> `m(e,a) = m(a,e) = a`. _Inverse Elemente:_ Für alle `a` aus `G`
|
||||
> gibt es genau ein Element `b` aus `G`, sodass `m(a,b) = m(b,a) = e`
|
||||
> ist.
|
||||
|
||||
In Mathlib ist eine Gruppe eine Typklasse `Group G`. Die Verknüpfung
|
||||
schreibt sich `a * b`, das neutrale Element `1`, das Inverse `a⁻¹`;
|
||||
die Axiome heißen `mul_assoc`, `one_mul`, `mul_one`,
|
||||
`inv_mul_cancel`, `mul_inv_cancel`.
|
||||
|
||||
Ein Unterschied fällt auf: Das Skript _fordert_ die Eindeutigkeit von
|
||||
neutralem Element und Inversen, Mathlib nicht. Das ist kein
|
||||
Widerspruch — die Eindeutigkeit folgt aus den übrigen Axiomen. Genau
|
||||
das beweisen wir jetzt, mit dem Standardargument aus der linearen
|
||||
Algebra:
|
||||
|
||||
> Es sei `e` ein weiteres Element, das von links neutral wirkt. Weil
|
||||
> `1` neutral ist, gilt `e·1 = e`. Weil `e` neutral wirkt, gilt
|
||||
> `e·1 = 1`. Zusammen folgt `e = e·1 = 1`.
|
||||
|
||||
Der Lean-Beweis benutzt die Taktik `calc`, die eine Kette von
|
||||
Gleichungen Schritt für Schritt abarbeitet — das Lean-Gegenstück zur
|
||||
Gleichungskette am Ende des Textbeweises:
|
||||
|
||||
```lean
|
||||
theorem neutral_eindeutig {G : Type*} [Group G] (e : G)
|
||||
(he : ∀ a : G, e * a = a) : e = 1 := by
|
||||
-- „Weil 1 neutral ist, gilt e·1 = e. Weil e neutral
|
||||
-- wirkt, gilt e·1 = 1. Zusammen folgt e = e·1 = 1.“
|
||||
calc e = e * 1 := (mul_one e).symm
|
||||
_ = 1 := he 1
|
||||
```
|
||||
|
||||
# Übungsaufgabe
|
||||
|
||||
Zeigen Sie ebenso die Eindeutigkeit des Inversen: Wenn `a·b = 1` ist,
|
||||
dann ist `b` bereits _das_ Inverse `a⁻¹`. Das Standardargument:
|
||||
`b = 1·b = (a⁻¹·a)·b = a⁻¹·(a·b) = a⁻¹·1 = a⁻¹`. Öffnen Sie
|
||||
`AlgebraInLean/Basics.lean` und ersetzen Sie das `sorry` durch einen
|
||||
Beweis — `calc` und die Lemmata `one_mul`, `inv_mul_cancel`,
|
||||
`mul_assoc`, `mul_one` genügen.
|
||||
|
||||
```lean
|
||||
theorem inverses_eindeutig {G : Type*} [Group G] (a b : G)
|
||||
(h : a * b = 1) : b = a⁻¹ := by
|
||||
sorry
|
||||
```
|
||||
@@ -0,0 +1,328 @@
|
||||
import VersoManual
|
||||
import Manual.Meta
|
||||
-- Minimal-Imports statt `import Mathlib`: lädt nur den
|
||||
-- benötigten Teil der Bibliothek und beschleunigt den
|
||||
-- Buch-Build erheblich (ermittelt mit `#min_imports`).
|
||||
import Mathlib.Algebra.Field.ZMod
|
||||
import Mathlib.Algebra.Torsor.Defs
|
||||
import Mathlib.Data.Finite.Vector
|
||||
import Mathlib.GroupTheory.PGroup
|
||||
import Mathlib.GroupTheory.Perm.Cycle.Type
|
||||
|
||||
open Verso.Genre Manual
|
||||
open Verso.Genre.Manual.InlineLean
|
||||
|
||||
set_option pp.rawOnError true
|
||||
set_option verso.docstring.allowMissing true
|
||||
|
||||
#doc (Manual) "Das Schlüssellemma und der Satz von Cauchy" =>
|
||||
%%%
|
||||
htmlSplit := .never
|
||||
tag := "cauchy"
|
||||
%%%
|
||||
|
||||
Dieses Kapitel übersetzt den Anfang von Kapitel 18 des Skripts: das
|
||||
_zentrale Schlüssellemma_ über Fixpunkte von p-Gruppen-Wirkungen und
|
||||
seine erste Anwendung, den Satz von Cauchy. Unterwegs werden wir zum
|
||||
ersten Mal selbst etwas in Lean _definieren_: eine Gruppenwirkung.
|
||||
|
||||
# Das zentrale Schlüssellemma
|
||||
|
||||
> *Lemma (Zentrales Schlüssellemma).* Es sei `m ∈ ℕ` und es sei `p`
|
||||
> eine Primzahl. Weiter sei `G` eine Gruppe der Ordnung `p^m`, die auf
|
||||
> einer endlichen Menge `M` operiert. Weiter sei
|
||||
> `M₀ = { m ∈ M : ∀ g ∈ G: g·m = m }` die Menge der Fixpunkte. Dann
|
||||
> ist `|M| ≡ |M₀| (mod p)`.
|
||||
|
||||
Wie sagt Mathlib das alles?
|
||||
|
||||
* „eine Gruppe der Ordnung `p^m`“: Dafür hat Mathlib ein Prädikat
|
||||
`IsPGroup p G` („die Ordnung jedes Elements ist eine p-Potenz“ — für
|
||||
endliche Gruppen ist das äquivalent, nach dem Satz von Cauchy
|
||||
unten!). Das Lemma `IsPGroup.of_card` übersetzt unsere
|
||||
Voraussetzung `Nat.card G = p ^ m` dorthin.
|
||||
|
||||
* „die auf einer endlichen Menge `M` operiert“: Eine Wirkung von `G`
|
||||
auf `M` ist eine Typklasse, `[MulAction G M]`; die Endlichkeit von
|
||||
`M` ist die Typklasse `[Finite M]`.
|
||||
|
||||
* Die Fixpunktmenge heißt `MulAction.fixedPoints G M`, und die
|
||||
Kongruenz `|M| ≡ |M₀| (mod p)` schreibt sich
|
||||
`Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p]`.
|
||||
|
||||
Der Beweis im Skript zerlegt `M` in Bahnen und zitiert die
|
||||
Bahnengleichung. Genau so beweist Mathlib die Aussage
|
||||
`IsPGroup.card_modEq_card_fixedPoints` — wir zitieren hier also
|
||||
einfach die Bibliothek, so wie das Skript an dieser Stelle Satz 17.2.6
|
||||
zitiert.
|
||||
|
||||
```lean
|
||||
open Equiv.Perm Equiv.Perm.VectorsProdEqOne
|
||||
open MulAction Multiplicative
|
||||
|
||||
theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*}
|
||||
[Group G] (hG : Nat.card G = p ^ m) (M : Type*)
|
||||
[Finite M] [MulAction G M] :
|
||||
Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p] := by
|
||||
have : Fact p.Prime := ⟨hp⟩
|
||||
exact (IsPGroup.of_card hG).card_modEq_card_fixedPoints M
|
||||
```
|
||||
|
||||
(Die `open`-Zeilen holen die Namensräume, die wir in diesem Kapitel
|
||||
brauchen, in den Geltungsbereich; `Equiv.Perm.vectorsProdEqOne` tritt
|
||||
gleich auf.)
|
||||
|
||||
# Der Satz von Cauchy
|
||||
|
||||
> *Satz (Satz von Cauchy).* Wenn die Ordnung einer endlichen Gruppe
|
||||
> durch `p` teilbar ist, dann existiert ein Element von Ordnung `p`.
|
||||
|
||||
Wir folgen dem Beweis des Skripts Satz für Satz. Der Beweis
|
||||
konstruiert eine raffinierte Hilfsmenge mit einer raffinierten
|
||||
Gruppenwirkung — diesmal gibt es also vor dem eigentlichen Satz echte
|
||||
Arbeit: Wir bauen erst die Menge und die Wirkung.
|
||||
|
||||
## Die Menge M
|
||||
|
||||
„Betrachte die Menge
|
||||
`M = { (a₁, …, a_p) ∈ G ⨯ ⋯ ⨯ G : a₁·a₂ ⋯ a_p = e }`.“
|
||||
|
||||
Mathlib kennt diese Menge. Ein p-Tupel von Gruppenelementen ist ein
|
||||
`List.Vector G p` — eine Liste der Länge `p` —, und `M` ist die Menge
|
||||
`Equiv.Perm.vectorsProdEqOne G p` aller Vektoren, deren Einträge sich
|
||||
zu 1 multiplizieren.
|
||||
|
||||
„Gegeben ein Tupel `(a₁, …, a_p) ∈ M`, dann stellen wir erst einmal
|
||||
fest, dass der letzte Eintrag des Tupels durch die ersten Einträge
|
||||
eindeutig bestimmt ist, `a_p = (a₁ ⋯ a_{p-1})⁻¹`. Wir erhalten die
|
||||
folgende Gleichung: `|M| = |G^{p-1}| = |G|^{p-1}`.“
|
||||
|
||||
Auch das steht schon in Mathlib: Die Bijektion
|
||||
`(a₁, …, a_{p-1}) ↦ (a₁, …, a_{p-1}, (a₁ ⋯ a_{p-1})⁻¹)` heißt
|
||||
`VectorsProdEqOne.vectorEquiv`, und die resultierende Zählformel ist
|
||||
`VectorsProdEqOne.card`:
|
||||
|
||||
```
|
||||
VectorsProdEqOne.card (G : Type) [Group G] (n : ℕ) [Fintype G] :
|
||||
Fintype.card ↑(vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)
|
||||
```
|
||||
|
||||
## Die Wirkung von ℤ/(p)
|
||||
|
||||
„Als Nächstes brauchen wir eine schicke Gruppenwirkung, denn wir
|
||||
wollen das zentrale Schlüssellemma anwenden. Dazu lassen wir die
|
||||
zyklische Gruppe `ℤ/(p)` auf `M` durch zyklisches Vertauschen wirken.“
|
||||
|
||||
Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p` um `k`
|
||||
Stellen ist `VectorsProdEqOne.rotate v k`. Die Fußnote des Skripts —
|
||||
der Shift bildet `M` auf sich ab, „weil in jeder Gruppe aus `a·b = e`
|
||||
auch `b·a = e` gilt“ — ist das Mathlib-Lemma
|
||||
`List.prod_rotate_eq_one_of_prod_eq_one`, das schon in der Definition
|
||||
von `rotate` steckt.
|
||||
|
||||
Damit `ℤ/(p)` _als Gruppe_ wirkt, müssen wir die Wirkungsaxiome
|
||||
nachprüfen: Der Shift um 0 tut nichts, und der Shift um `j + k` ist
|
||||
der Shift um `k` gefolgt vom Shift um `j`. Mathlib stellt
|
||||
`rotate_zero`, `rotate_rotate` und `rotate_length` bereit (der Shift
|
||||
um die volle Länge `p` tut nichts); daraus leiten wir zuerst ab, dass
|
||||
der Shift nur von der Verschiebung _modulo p_ abhängt — genau deshalb
|
||||
wirkt `ℤ/(p)` und nicht bloß `ℕ`.
|
||||
|
||||
```lean
|
||||
theorem rotate_mul {G : Type*} [Group G] {p : ℕ}
|
||||
(v : vectorsProdEqOne G p) (q : ℕ) :
|
||||
rotate v (p * q) = v := by
|
||||
induction q with
|
||||
| zero => rw [Nat.mul_zero, rotate_zero]
|
||||
| succ q ih =>
|
||||
rw [Nat.mul_succ, ← rotate_rotate, ih, rotate_length]
|
||||
|
||||
theorem rotate_mod {G : Type*} [Group G] {p : ℕ}
|
||||
(v : vectorsProdEqOne G p) (k : ℕ) :
|
||||
rotate v (k % p) = rotate v k := by
|
||||
calc rotate v (k % p)
|
||||
= rotate (rotate v (k % p)) (p * (k / p)) :=
|
||||
(rotate_mul _ _).symm
|
||||
_ = rotate v (k % p + p * (k / p)) :=
|
||||
rotate_rotate _ _ _
|
||||
_ = rotate v k := by rw [Nat.mod_add_div]
|
||||
```
|
||||
|
||||
Nun können wir die Wirkung definieren. Zwei technische Anmerkungen.
|
||||
Mathlibs `MulAction` erwartet eine multiplikativ geschriebene Gruppe;
|
||||
`ℤ/(p)` = `ZMod p` ist aber additiv geschrieben. Der Wrapper
|
||||
`Multiplicative` wechselt die Notation (dank
|
||||
`open Multiplicative` oben schreiben sich seine Übergänge kurz
|
||||
`toAdd` und `ofAdd`). Die Voraussetzung `[NeZero p]` schließt
|
||||
`p = 0` aus, wo „Shift um eine Restklasse“ sinnlos wäre.
|
||||
|
||||
```lean
|
||||
instance rotateAction {G : Type*} [Group G] {p : ℕ}
|
||||
[NeZero p] :
|
||||
MulAction (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p) where
|
||||
smul k v := rotate v (toAdd k).val
|
||||
one_smul v := by
|
||||
show rotate v (ZMod.val 0) = v
|
||||
rw [ZMod.val_zero, rotate_zero]
|
||||
mul_smul j k v := by
|
||||
show rotate v ((toAdd j + toAdd k).val) =
|
||||
rotate (rotate v (toAdd k).val) (toAdd j).val
|
||||
rw [ZMod.val_add, rotate_mod, rotate_rotate,
|
||||
Nat.add_comm]
|
||||
```
|
||||
|
||||
## Die Fixpunkte
|
||||
|
||||
„Die Fixpunktmenge dieser Wirkung ist
|
||||
`M₀ = { (a, …, a) ∈ G^p : a^p = e }`.“
|
||||
|
||||
Mit anderen Worten: Ein Tupel ist genau dann ein Fixpunkt, wenn es
|
||||
konstant ist, seine Liste also für ein `a` die Liste
|
||||
`List.replicate p a` — das ist `(a, …, a)` — ist. (Die Bedingung
|
||||
`a^p = e` gilt dann automatisch, weil sich die Einträge eines Tupels
|
||||
in `M` zu `e` multiplizieren.) Der Schlüsselschritt ist das Lemma
|
||||
`List.rotate_one_eq_self_iff_eq_replicate`: Eine Liste, die der
|
||||
zyklische Shift um _eine_ Stelle nicht ändert, ist konstant.
|
||||
|
||||
```lean
|
||||
theorem mem_fixedPoints_iff_replicate {G : Type*} [Group G]
|
||||
{p : ℕ} [Fact (1 < p)] (v : vectorsProdEqOne G p) :
|
||||
v ∈ fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p) ↔
|
||||
∃ a : G,
|
||||
(v : List.Vector G p).toList
|
||||
= List.replicate p a := by
|
||||
rw [mem_fixedPoints]
|
||||
constructor
|
||||
· -- Ein Fixpunkt wird insbesondere von 1 ∈ ℤ/(p) fixiert,
|
||||
-- bleibt also unter dem Shift um eine Stelle
|
||||
-- unverändert …
|
||||
intro hv
|
||||
have h1 : rotate v 1 = v := by
|
||||
have h := hv (ofAdd (1 : ZMod p))
|
||||
rwa [show ofAdd (1 : ZMod p) • v
|
||||
= rotate v (1 : ZMod p).val from rfl,
|
||||
ZMod.val_one] at h
|
||||
-- … und ist daher konstant.
|
||||
obtain ⟨a, ha⟩ :=
|
||||
List.rotate_one_eq_self_iff_eq_replicate.mp
|
||||
(Subtype.ext_iff.mp (Subtype.ext_iff.mp h1))
|
||||
refine ⟨a, ha.trans ?_⟩
|
||||
congr 1
|
||||
exact (v : List.Vector G p).2
|
||||
· -- Umgekehrt ändert kein zyklischer Shift ein konstantes
|
||||
-- Tupel.
|
||||
rintro ⟨a, ha⟩ g
|
||||
apply Subtype.ext
|
||||
apply Subtype.ext
|
||||
show (v : List.Vector G p).toList.rotate (toAdd g).val =
|
||||
(v : List.Vector G p).toList
|
||||
rw [ha, List.rotate_replicate]
|
||||
```
|
||||
|
||||
## Der Beweis
|
||||
|
||||
Jetzt setzen wir die Teile zusammen und folgen dem Skript Zeile für
|
||||
Zeile.
|
||||
|
||||
```lean
|
||||
theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ}
|
||||
(hp : p.Prime) (hdvd : p ∣ Fintype.card G) :
|
||||
∃ a : G, orderOf a = p := by
|
||||
-- Die Konsequenzen der Primalität, die die Instanzsuche
|
||||
-- braucht:
|
||||
have : Fact p.Prime := ⟨hp⟩
|
||||
have : NeZero p := ⟨hp.ne_zero⟩
|
||||
have : Fact (1 < p) := ⟨hp.one_lt⟩
|
||||
-- Abkürzung: M₀ ist die Fixpunktmenge der Wirkung.
|
||||
set M₀ := fixedPoints (Multiplicative (ZMod p))
|
||||
(vectorsProdEqOne G p)
|
||||
-- „Wir erhalten die folgende Gleichung:
|
||||
-- |M| = |G^{p-1}| = |G|^{p-1}.“
|
||||
have hM : Nat.card (vectorsProdEqOne G p)
|
||||
= Fintype.card G ^ (p - 1) := by
|
||||
rw [Nat.card_eq_fintype_card, VectorsProdEqOne.card]
|
||||
-- Die zyklische Gruppe ℤ/(p) hat Ordnung p = p¹; das
|
||||
-- Schlüssellemma, angewandt auf die Rotationswirkung,
|
||||
-- liefert |M| ≡ |M₀| (mod p):
|
||||
have hZp :
|
||||
Nat.card (Multiplicative (ZMod p)) = p ^ 1 := by
|
||||
simp [Nat.card_eq_fintype_card]
|
||||
have hcong :
|
||||
Nat.card (vectorsProdEqOne G p) ≡
|
||||
Nat.card M₀ [MOD p] :=
|
||||
key_lemma hp hZp (vectorsProdEqOne G p)
|
||||
-- „Auf der anderen Seite folgt aus dem zentralen
|
||||
-- Schlüssellemma, dass
|
||||
-- |M₀| ≡ |M| ≡ |G|^{p-1} ≡ 0 (mod p) ist.“
|
||||
have hdvdM0 : p ∣ Nat.card M₀ := by
|
||||
have hp1 : p - 1 ≠ 0 := by have := hp.one_lt; omega
|
||||
have h0 : (0 : ℕ) ≡ Nat.card M₀ [MOD p] :=
|
||||
calc (0 : ℕ)
|
||||
≡ Fintype.card G ^ (p - 1) [MOD p] :=
|
||||
(Nat.modEq_zero_iff_dvd.mpr
|
||||
(dvd_pow hdvd hp1)).symm
|
||||
_ = Nat.card (vectorsProdEqOne G p) := hM.symm
|
||||
_ ≡ Nat.card M₀ [MOD p] := hcong
|
||||
exact Nat.modEq_zero_iff_dvd.mp h0.symm
|
||||
-- „Wegen (e, …, e) ∈ M₀ ist schon einmal klar, dass
|
||||
-- M₀ ≠ ∅ ist.“
|
||||
let v₀ : vectorsProdEqOne G p :=
|
||||
⟨List.Vector.replicate p 1,
|
||||
(List.prod_replicate p 1).trans (one_pow p)⟩
|
||||
have hv₀ : v₀ ∈ M₀ :=
|
||||
(mem_fixedPoints_iff_replicate v₀).mpr ⟨1, rfl⟩
|
||||
-- M₀ ist nichtleer, und |M₀| ist durch p ≥ 2 teilbar,
|
||||
-- also ist |M₀| ≥ p > 1 …
|
||||
have := Fintype.ofFinite M₀
|
||||
have hlt : 1 < Fintype.card M₀ := by
|
||||
rw [← Nat.card_eq_fintype_card]
|
||||
have hpos : 0 < Nat.card M₀ :=
|
||||
Nat.card_pos_iff.mpr ⟨⟨⟨v₀, hv₀⟩⟩, inferInstance⟩
|
||||
have := Nat.le_of_dvd hpos hdvdM0
|
||||
have := hp.one_lt
|
||||
omega
|
||||
-- „Also existiert mindestens ein a ≠ e mit a^p = e.“
|
||||
obtain ⟨w, hw⟩ :=
|
||||
Fintype.exists_ne_of_one_lt_card hlt ⟨v₀, hv₀⟩
|
||||
obtain ⟨a, ha⟩ :=
|
||||
(mem_fixedPoints_iff_replicate w.1).mp w.2
|
||||
-- Das Tupel w liegt in M, sein Produkt ist also e; weil
|
||||
-- das Tupel konstant ist, heißt das genau a^p = e:
|
||||
have hpow : a ^ p = 1 := by
|
||||
have hprod : (w.1 : List.Vector G p).toList.prod = 1 :=
|
||||
w.1.2
|
||||
rwa [ha, List.prod_replicate] at hprod
|
||||
-- Und a ≠ e, denn sonst wäre w das Tupel (e, …, e) = v₀:
|
||||
have hne : a ≠ 1 := by
|
||||
rintro rfl
|
||||
exact hw (Subtype.ext (Subtype.ext (Subtype.ext ha)))
|
||||
-- „Nach Satz 17.4.11 hat a dann automatisch die
|
||||
-- Ordnung p.“
|
||||
exact ⟨a, orderOf_eq_prime hpow hne⟩
|
||||
```
|
||||
|
||||
# Bemerkungen
|
||||
|
||||
Mathlibs Fassung des Satzes von Cauchy heißt
|
||||
`exists_prime_orderOf_dvd_card`; ihr Beweis ist dasselbe Zählargument,
|
||||
nur etwas anders organisiert.
|
||||
|
||||
# Übungsaufgabe
|
||||
|
||||
Das ist Satz 18.2.3 im Skript: _Es sei `p` eine Primzahl und `G` eine
|
||||
nichttriviale Gruppe, deren Ordnung eine p-Potenz ist. Dann ist das
|
||||
Zentrum von `G` nicht trivial._ Beweisen Sie das in Lean: Wenden Sie
|
||||
`key_lemma` auf die Konjugationswirkung von `G` auf sich selbst an —
|
||||
oder finden Sie die Aussage in Mathlib. Öffnen Sie
|
||||
`AlgebraInLean/Cauchy.lean` im Übungs-Repository und ersetzen Sie das
|
||||
`sorry` durch einen Beweis.
|
||||
|
||||
```lean
|
||||
theorem center_nontrivial {p m : ℕ} (hp : p.Prime)
|
||||
{G : Type*} [Group G] [Finite G] (hm : m ≠ 0)
|
||||
(hG : Nat.card G = p ^ m) :
|
||||
Nontrivial (Subgroup.center G) := by
|
||||
sorry
|
||||
```
|
||||
@@ -0,0 +1,147 @@
|
||||
import VersoManual
|
||||
import Manual.Meta
|
||||
-- Minimal-Import statt `import Mathlib`: lädt nur den
|
||||
-- benötigten Teil der Bibliothek und beschleunigt den
|
||||
-- Buch-Build erheblich (ermittelt mit `#min_imports`).
|
||||
import Mathlib.FieldTheory.Finite.Basic
|
||||
|
||||
open Verso.Genre Manual
|
||||
open Verso.Genre.Manual.InlineLean
|
||||
|
||||
set_option pp.rawOnError true
|
||||
set_option verso.docstring.allowMissing true
|
||||
|
||||
#doc (Manual) "Der kleine Satz von Fermat" =>
|
||||
%%%
|
||||
htmlSplit := .never
|
||||
tag := "little-fermat"
|
||||
%%%
|
||||
|
||||
Unser erster Beweis übersetzt Satz 17.5.2 des Skripts. Hier das
|
||||
deutsche Original, Aussage und Beweis:
|
||||
|
||||
> *Satz (Kleiner Satz von Fermat).* Es sei `p ∈ ℕ` eine Primzahl und es
|
||||
> sei `a ∈ ℤ` irgendeine Zahl. Dann ist `a^p ≡ a (mod p)`.
|
||||
>
|
||||
> _Beweis._ Falls `a` ein Vielfaches von `p` ist, ist die Sache klar.
|
||||
> Ansonsten liefert die Restklasse von `a` ein nicht-verschwindendes
|
||||
> Element `ā ∈ ℤ/(p) = 𝔽_p`, also ein Element der multiplikativen
|
||||
> Gruppe `𝔽_p^*`, welche `p−1` Elemente hat. Nach dem Satz von
|
||||
> Lagrange ist die Ordnung von `ā`, also die Größe der von `ā`
|
||||
> erzeugten Untergruppe, ein Teiler von `|𝔽_p^*| = p−1`. Es gilt also
|
||||
> `ā^(p−1) = 1 ∈ 𝔽_p^*`, oder äquivalent `a^p ≡ a (mod p)`. ∎
|
||||
|
||||
Fünf Sätze. Unser Ziel ist ein Lean-Beweis mit genau dieser Struktur —
|
||||
jeder deutsche Satz kehrt als Kommentar über dem Lean-Code wieder, der
|
||||
ihn umsetzt.
|
||||
|
||||
# Das Mathlib-Wörterbuch
|
||||
|
||||
Bevor wir den Satz überhaupt formulieren können, müssen wir wissen, wie
|
||||
Mathlib über die beteiligten Objekte spricht.
|
||||
|
||||
* Der Restklassenring `ℤ/(p)` heißt `ZMod p`. Die Restklasse einer
|
||||
ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)` — Lean fügt den
|
||||
kanonischen Ringmorphismus `ℤ → ℤ/(p)` automatisch ein (eine
|
||||
_Koerzion_).
|
||||
|
||||
* Die Kongruenz `a ≡ b (mod p)` für ganze Zahlen schreibt sich
|
||||
`a ≡ b [ZMOD p]`.
|
||||
|
||||
* Die multiplikative Gruppe `𝔽_p^*` ist die Gruppe der _Einheiten_ des
|
||||
Rings `ZMod p`, geschrieben `(ZMod p)ˣ`. Eine Einheit
|
||||
`u : (ZMod p)ˣ` kennt ihr Inverses; das zugrundeliegende Ringelement
|
||||
schreibt sich wieder `(u : ZMod p)`.
|
||||
|
||||
* Das Skript sagt „es sei `p` eine Primzahl“. In Lean führen wir die
|
||||
Primalität von `p` als Hypothese `hp : p.Prime` mit. Manche
|
||||
Tatsachen — etwa dass `ℤ/(p)` ein Körper ist — findet Leans
|
||||
Automatisierung nur, wenn die Hypothese als _Instanz_ registriert
|
||||
ist; genau das leistet die erste Beweiszeile
|
||||
`have : Fact p.Prime := ⟨hp⟩`.
|
||||
|
||||
# Der Beweis, Satz für Satz
|
||||
|
||||
```lean
|
||||
theorem little_fermat (p : ℕ) (hp : p.Prime) (a : ℤ) :
|
||||
a ^ p ≡ a [ZMOD p] := by
|
||||
have : Fact p.Prime := ⟨hp⟩
|
||||
-- Die Kongruenz „a^p ≡ a (mod p)“ bedeutet gerade, dass
|
||||
-- a^p und a dieselbe Restklasse in ℤ/(p) haben. Wir
|
||||
-- dürfen also stattdessen eine *Gleichung* im Ring
|
||||
-- `ZMod p` zeigen; das Beweisziel wird
|
||||
-- (a : ZMod p) ^ p = (a : ZMod p).
|
||||
rw [← ZMod.intCast_eq_intCast_iff]
|
||||
push_cast
|
||||
-- „Falls a ein Vielfaches von p ist, ist die Sache klar.“
|
||||
by_cases ha : (a : ZMod p) = 0
|
||||
· rw [ha, zero_pow hp.ne_zero]
|
||||
-- „Ansonsten liefert die Restklasse von a ein
|
||||
-- nicht-verschwindendes Element ā ∈ ℤ/(p) = 𝔽_p, also
|
||||
-- ein Element der multiplikativen Gruppe 𝔽_p^*, …“
|
||||
· obtain ⟨u, hu⟩ : IsUnit (a : ZMod p) :=
|
||||
isUnit_iff_ne_zero.mpr ha
|
||||
rw [← hu]
|
||||
-- „… welche p−1 Elemente hat.“
|
||||
have card_units : Nat.card (ZMod p)ˣ = p - 1 := by
|
||||
rw [Nat.card_eq_fintype_card, ZMod.card_units p]
|
||||
-- „Nach Satz 17.3.6 («Satz von Lagrange») ist die
|
||||
-- Ordnung von ā, also die Größe der von ā erzeugten
|
||||
-- Untergruppe, ein Teiler von |𝔽_p^*| = p−1.“
|
||||
have lagrange :
|
||||
Nat.card (Subgroup.zpowers u) ∣
|
||||
Nat.card (ZMod p)ˣ :=
|
||||
Subgroup.card_subgroup_dvd_card (Subgroup.zpowers u)
|
||||
have ord_dvd : orderOf u ∣ p - 1 := by
|
||||
rw [← Nat.card_zpowers, ← card_units]
|
||||
exact lagrange
|
||||
-- „Es gilt also ā^(p−1) = 1 ∈ 𝔽_p^* …“
|
||||
have pow_eq_one : u ^ (p - 1) = 1 :=
|
||||
orderOf_dvd_iff_pow_eq_one.mp ord_dvd
|
||||
-- „… oder äquivalent a^p ≡ a (mod p).“
|
||||
have key : u ^ p = u := by
|
||||
calc u ^ p
|
||||
= u ^ (p - 1 + 1) := by
|
||||
rw [Nat.sub_add_cancel hp.one_lt.le]
|
||||
_ = u ^ (p - 1) * u := pow_succ u (p - 1)
|
||||
_ = u := by rw [pow_eq_one, one_mul]
|
||||
exact_mod_cast congrArg Units.val key
|
||||
```
|
||||
|
||||
Man beachte, wie treu die Übersetzung ist. Die Fallunterscheidung
|
||||
„Falls … ist die Sache klar / Ansonsten …“ wird zu `by_cases`; das
|
||||
Zitat des Satzes von Lagrange wird zum Bibliothekslemma
|
||||
`Subgroup.card_subgroup_dvd_card`; und die Formulierung „die Ordnung
|
||||
von `ā`, also die Größe der von `ā` erzeugten Untergruppe“ ist genau
|
||||
das Umschreiben mit `Nat.card_zpowers`, das `orderOf u` mit der
|
||||
Mächtigkeit der von `u` erzeugten Untergruppe `Subgroup.zpowers u`
|
||||
identifiziert.
|
||||
|
||||
# Bemerkungen
|
||||
|
||||
Mathlib enthält den kleinen Satz von Fermat natürlich längst; die
|
||||
Aussage über Restklassen heißt `ZMod.pow_card`. Solche Lemmata findet
|
||||
man selbst mit der Taktik `exact?` oder über die Suchmaschinen
|
||||
[leansearch.net](https://leansearch.net) und
|
||||
[loogle.lean-lang.org](https://loogle.lean-lang.org).
|
||||
|
||||
```lean
|
||||
example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a :=
|
||||
ZMod.pow_card a
|
||||
```
|
||||
|
||||
# Übungsaufgabe
|
||||
|
||||
Das ist die Bemerkung nach dem Satz im Skript: In Anwendungen
|
||||
verwendet man häufig die äquivalente Formulierung
|
||||
`a^(p−1) ≡ 1 (mod p)` für nicht durch `p` teilbare `a`. Leiten Sie
|
||||
sie aus `little_fermat` ab — oder geben Sie einen direkten Beweis nach
|
||||
den Ideen oben. Öffnen Sie `AlgebraInLean/LittleFermat.lean` im
|
||||
Übungs-Repository und ersetzen Sie das `sorry` durch einen Beweis.
|
||||
|
||||
```lean
|
||||
theorem little_fermat' (p : ℕ) (hp : p.Prime) (a : ℤ)
|
||||
(ha : ¬ (p : ℤ) ∣ a) :
|
||||
a ^ (p - 1) ≡ 1 [ZMOD p] := by
|
||||
sorry
|
||||
```
|
||||
@@ -0,0 +1,148 @@
|
||||
import VersoManual
|
||||
import Manual.Meta
|
||||
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
|
||||
-- `#min_imports`, ergänzt um QuotientGroup und die
|
||||
-- Taktik `group`.
|
||||
import Mathlib.Algebra.Group.Int.Defs
|
||||
import Mathlib.Algebra.Group.Subgroup.Ker
|
||||
import Mathlib.GroupTheory.QuotientGroup.Defs
|
||||
import Mathlib.Tactic.Group
|
||||
|
||||
open Verso.Genre Manual
|
||||
open Verso.Genre.Manual.InlineLean
|
||||
|
||||
set_option pp.rawOnError true
|
||||
set_option verso.docstring.allowMissing true
|
||||
|
||||
#doc (Manual) "Gruppen und Restklassengruppen" =>
|
||||
%%%
|
||||
htmlSplit := .never
|
||||
tag := "quotients"
|
||||
%%%
|
||||
|
||||
Dieses Kapitel übersetzt zwei Beweise rund um normale Untergruppen
|
||||
Satz für Satz nach Lean: das Argument aus Erklärvideo 1-1 des
|
||||
Skripts, dass Kerne von Gruppenmorphismen abgeschlossen unter
|
||||
Konjugation sind, und die Beobachtung aus Kapitel 17.3, dass `U·N`
|
||||
für normales `N` wieder eine Untergruppe ist.
|
||||
|
||||
# Das Mathlib-Wörterbuch
|
||||
|
||||
* Eine Untergruppe von `G` ist ein Term `U : Subgroup G`; die
|
||||
Mitgliedschaft schreibt sich `g ∈ U`. Dass `U` unter Verknüpfung
|
||||
und Inversen abgeschlossen ist, sagen `U.mul_mem` und `U.inv_mem`.
|
||||
|
||||
* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein „Bündel“ aus
|
||||
der Abbildung und den Nachweisen `map_mul : φ (a·b) = φ a · φ b`
|
||||
(daraus folgen `map_one` und `map_inv`). Der Kern heißt `φ.ker`;
|
||||
die Mitgliedschaft entpackt
|
||||
`MonoidHom.mem_ker : g ∈ φ.ker ↔ φ g = 1`.
|
||||
|
||||
* „`N` ist Normalteiler“ ist das Prädikat `N.Normal`; sein Feld
|
||||
`conj_mem` ist wörtlich die Bedingung des Skripts: für alle
|
||||
`n ∈ N` und alle `g` ist `g·n·g⁻¹ ∈ N`.
|
||||
|
||||
# Kerne sind abgeschlossen unter Konjugation
|
||||
|
||||
Aus Erklärvideo 1-1 des Skripts:
|
||||
|
||||
> Die Antwort lautet: Nein! Nicht jede Untergruppe kann Kern eines
|
||||
> Gruppenmorphismus sein. Wenn es nämlich einen Gruppenmorphismus
|
||||
> `φ : G → Q` mit `H = ker(φ)` gibt, dann gilt für alle `h ∈ H` und
|
||||
> alle `g ∈ G` die Gleichung `φ(g·h·g⁻¹) = φ(g)·φ(h)·φ(g)⁻¹ = e`,
|
||||
> wobei `e` das neutrale Element von `Q` bezeichnet. Also ist stets
|
||||
> `g·h·g⁻¹ ∈ H`.
|
||||
|
||||
```lean
|
||||
theorem kern_konjugation {G Q : Type*} [Group G] [Group Q]
|
||||
(φ : G →* Q) {h : G} (hh : h ∈ φ.ker) (g : G) :
|
||||
g * h * g⁻¹ ∈ φ.ker := by
|
||||
-- Mitgliedschaft im Kern heißt: φ bildet auf 1 ab.
|
||||
rw [MonoidHom.mem_ker] at hh ⊢
|
||||
-- „… dann gilt für alle h ∈ H und alle g ∈ G die
|
||||
-- Gleichung φ(g·h·g⁻¹) = φ(g)·φ(h)·φ(g)⁻¹ = e …“
|
||||
calc φ (g * h * g⁻¹)
|
||||
= φ g * φ h * (φ g)⁻¹ := by
|
||||
rw [map_mul, map_mul, map_inv]
|
||||
_ = φ g * 1 * (φ g)⁻¹ := by rw [hh]
|
||||
_ = 1 := by rw [mul_one, mul_inv_cancel]
|
||||
```
|
||||
|
||||
Mathlib kennt diese Aussage als Instanz
|
||||
`MonoidHom.normal_ker : φ.ker.Normal`. Das Skript fährt fort:
|
||||
Untergruppen mit dieser Eigenschaft heißen _normale Untergruppen_
|
||||
oder _Normalteiler_, und die Bedingung ist nicht nur notwendig,
|
||||
sondern auch hinreichend — zu jedem Normalteiler existiert eine
|
||||
Restklassengruppe.
|
||||
|
||||
# Die Restklassengruppe und ihre universelle Eigenschaft
|
||||
|
||||
Das Skript definiert die Restklassengruppe in Kapitel 17.3 über ihre
|
||||
universelle Eigenschaft. Mathlib stellt beides bereit: den
|
||||
Quotienten `G ⧸ N` mit der Quotientenabbildung
|
||||
`QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle Eigenschaft
|
||||
als `QuotientGroup.lift` — gegeben ein Morphismus `α : G →* H` mit
|
||||
`N ≤ α.ker` erhält man den induzierten Morphismus auf dem
|
||||
Quotienten:
|
||||
|
||||
```lean
|
||||
example {G H : Type*} [Group G] [Group H] (N : Subgroup G)
|
||||
[N.Normal] (α : G →* H) (hα : N ≤ α.ker) :
|
||||
G ⧸ N →* H :=
|
||||
QuotientGroup.lift N α
|
||||
fun _g hg => MonoidHom.mem_ker.mp (hα hg)
|
||||
```
|
||||
|
||||
# Die Beobachtung: U·N ist eine Untergruppe
|
||||
|
||||
Beobachtung aus Kapitel 17.3 des Skripts:
|
||||
|
||||
> Es sei `G` eine Gruppe und es sei `N ⊂ G` eine normale
|
||||
> Untergruppe. Weiter sei `U ⊂ G` irgendeine Untergruppe. Dann ist
|
||||
> `U·N = {u·n : u ∈ U, n ∈ N}` wieder eine Untergruppe. Zum Beweis
|
||||
> müssen wir lediglich zeigen, dass `U·N` abgeschlossen unter der
|
||||
> Gruppenoperation ist. … Wir wissen, dass `N` normal ist. Also
|
||||
> ist `ñ₁ := u₂⁻¹·n₁·u₂ ∈ N` und es gilt `n₁·u₂ = u₂·ñ₁`. Demnach
|
||||
> ist `u₁n₁u₂n₂ = u₁u₂·ñ₁n₂ ∈ U·N`. Fertig ist der Beweis.
|
||||
|
||||
Neu ist hier die Taktik `group`: Sie verrechnet Ausdrücke, die
|
||||
allein mit den Gruppenaxiomen ineinander umgeformt werden können.
|
||||
(Das `ñ₁` des Skripts heißt im Code `n₁'`.)
|
||||
|
||||
```lean
|
||||
theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
|
||||
(hN : N.Normal) {u₁ n₁ u₂ n₂ : G}
|
||||
(hu₁ : u₁ ∈ U) (hn₁ : n₁ ∈ N)
|
||||
(hu₂ : u₂ ∈ U) (hn₂ : n₂ ∈ N) :
|
||||
∃ u ∈ U, ∃ n ∈ N, u₁ * n₁ * (u₂ * n₂) = u * n := by
|
||||
-- „Wir wissen, dass N normal ist. Also ist
|
||||
-- ñ₁ := u₂⁻¹·n₁·u₂ ∈ N …“
|
||||
set n₁' := u₂⁻¹ * n₁ * u₂ with hn₁'_def
|
||||
have hn₁' : n₁' ∈ N := hN.conj_mem' n₁ hn₁ u₂
|
||||
-- „… und es gilt n₁·u₂ = u₂·ñ₁.“
|
||||
have hswap : n₁ * u₂ = u₂ * n₁' := by
|
||||
rw [hn₁'_def]; group
|
||||
-- „Demnach ist u₁n₁u₂n₂ = u₁u₂·ñ₁n₂ ∈ U·N.“
|
||||
refine ⟨u₁ * u₂, U.mul_mem hu₁ hu₂,
|
||||
n₁' * n₂, N.mul_mem hn₁' hn₂, ?_⟩
|
||||
calc u₁ * n₁ * (u₂ * n₂)
|
||||
= u₁ * (n₁ * u₂) * n₂ := by group
|
||||
_ = u₁ * (u₂ * n₁') * n₂ := by rw [hswap]
|
||||
_ = u₁ * u₂ * (n₁' * n₂) := by group
|
||||
```
|
||||
|
||||
# Übungsaufgabe
|
||||
|
||||
Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit unter der
|
||||
Verknüpfung zu zeigen — prüfen Sie den verschwiegenen Teil selbst
|
||||
nach: `U·N` ist auch abgeschlossen unter Inversen. Tipp:
|
||||
`(u·n)⁻¹ = u⁻¹·(u·n⁻¹·u⁻¹)`, und der zweite Faktor liegt nach
|
||||
`conj_mem` in `N`. Öffnen Sie `AlgebraInLean/Quotients.lean` und
|
||||
ersetzen Sie das `sorry` durch einen Beweis.
|
||||
|
||||
```lean
|
||||
theorem inv_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
|
||||
(hN : N.Normal) {u n : G} (hu : u ∈ U) (hn : n ∈ N) :
|
||||
∃ u' ∈ U, ∃ n' ∈ N, (u * n)⁻¹ = u' * n' := by
|
||||
sorry
|
||||
```
|
||||
@@ -0,0 +1,67 @@
|
||||
import Book
|
||||
import Manual.Meta
|
||||
|
||||
open Verso.Genre Manual
|
||||
open Verso.Genre.Manual
|
||||
|
||||
-- The static assets (theme, fonts, KaTeX) follow the setup of
|
||||
-- Peter Pfaffelhuber's course notes, https://github.com/pfaffelh/leancourse.
|
||||
|
||||
open Verso.Output.Html in
|
||||
def staticCss := {{
|
||||
<link rel="stylesheet" href="/static/colors.css" />
|
||||
<link rel="stylesheet" href="/static/theme.css" />
|
||||
<link rel="stylesheet" href="/static/print.css" />
|
||||
<link rel="stylesheet" href="/static/fonts/source-serif/source-serif-text.css" />
|
||||
<link rel="stylesheet" href="/static/fonts/source-code-pro/source-code-pro.css" />
|
||||
<link rel="stylesheet" href="/static/katex/katex.min.css" />
|
||||
}}
|
||||
|
||||
open Verso.Output.Html in
|
||||
def staticJs := {{
|
||||
<script src="/static/katex/katex.min.js"></script>
|
||||
<script src="/static/math.js"></script>
|
||||
<script src="/static/print.js"></script>
|
||||
}}
|
||||
|
||||
def KaTeXLicense : LicenseInfo where
|
||||
identifier := "MIT"
|
||||
dependency := "KaTeX"
|
||||
howUsed := "KaTeX is used to render mathematical notation."
|
||||
link := "https://katex.org/"
|
||||
text := #[(some "The MIT License", text)]
|
||||
where
|
||||
text := r#"
|
||||
Copyright (c) 2013-2020 Khan Academy and other contributors
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all
|
||||
copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
SOFTWARE.
|
||||
"#
|
||||
|
||||
def main :=
|
||||
manualMain (%doc Book) (config := config)
|
||||
where
|
||||
config := {
|
||||
extraFiles := [("static", "static")],
|
||||
extraHead := #[staticCss, staticJs],
|
||||
emitTeX := false,
|
||||
-- Deployt wird nur die Multi-Page-Ausgabe; die
|
||||
-- Single-Page-Ausgabe wäre doppelte Generierungsarbeit.
|
||||
emitHtmlSingle := .no,
|
||||
emitHtmlMulti := .immediately,
|
||||
}
|
||||
@@ -32,9 +32,29 @@ Lean/Mathlib.
|
||||
|
||||
| File | Lecture notes | Topic |
|
||||
|------|---------------|-------|
|
||||
| `AlgebraInLean/Basics.lean` | Kapitel 2 | First steps: tactics, groups in Mathlib |
|
||||
| `AlgebraInLean/Quotients.lean` | Kapitel 2, 17 | Kernels, normal subgroups, quotient groups |
|
||||
| `AlgebraInLean/LittleFermat.lean` | Kapitel 17 | Fermat's little theorem via Lagrange |
|
||||
| `AlgebraInLean/Cauchy.lean` | Kapitel 18 | The key lemma on fixed points and Cauchy's theorem |
|
||||
|
||||
## The rendered course notes
|
||||
|
||||
The folder `Book/` contains the same material as a
|
||||
[Verso](https://github.com/leanprover/verso) book (the technical setup
|
||||
follows Peter Pfaffelhuber's
|
||||
[leancourse](https://github.com/pfaffelh/leancourse)). To render it:
|
||||
|
||||
```bash
|
||||
lake build
|
||||
lake exe algebrainlean --output _out
|
||||
python3 -m http.server 8000 -d _out/html-multi # then open http://localhost:8000
|
||||
```
|
||||
|
||||
All Lean code in the book is elaborated during the build, so the
|
||||
rendered proofs are guaranteed to compile. `./deploy.sh` builds the
|
||||
site and copies it to `public/`, which is synced to the CPLX web
|
||||
server as for the lecture notes.
|
||||
|
||||
## License
|
||||
|
||||
CC-BY 4.0, like the lecture notes.
|
||||
@@ -0,0 +1,10 @@
|
||||
#!/bin/bash
|
||||
# Baut die Kursnotizen und legt sie in public/ ab — analog zum
|
||||
# deploy.sh des Vorlesungsskripts. Der Abgleich von public/ mit dem
|
||||
# CPLX-Server läuft wie dort.
|
||||
set -e
|
||||
|
||||
lake build
|
||||
lake exe algebrainlean --output _out
|
||||
mkdir -p public
|
||||
rsync -a --delete _out/html-multi/ public/
|
||||
+61
-1
@@ -11,6 +11,16 @@
|
||||
"inputRev": "87adeaebd370a3b6a41ac4f044fddd4bf81803ad",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/reference-manual.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "527c864cfd8da8b3d119ee09382749b6b6204eb4",
|
||||
"name": "«verso-manual»",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.33.0-rc2",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover-community/plausible",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
@@ -81,6 +91,36 @@
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/leanprover/verso.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "f62e380bcf8e11a2df70697916c8333bafdf3540",
|
||||
"name": "verso",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "nightly-testing",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/illuminate",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "006dc1d1db18c5dc73d637c926cf132e88df05b5",
|
||||
"name": "illuminate",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/verso-web-components",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "61182a9187f497946b1a9170018e241c9500e6da",
|
||||
"name": "versowebcomponents",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/lean4-cli",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
@@ -90,7 +130,27 @@
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.33.0-rc2",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"}],
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/acmepjz/md4lean",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
|
||||
"name": "MD4Lean",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/subverso",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "859ab80c32c5851151919a7d757d7c0c0b6e39d2",
|
||||
"name": "subverso",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "AlgebraInLean",
|
||||
"lakeDir": ".lake",
|
||||
"fixedToolchain": false}
|
||||
@@ -0,0 +1,39 @@
|
||||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
-- The manual genre of the Lean reference manual is pinned to the tag
|
||||
-- matching the toolchain; verso is NOT required explicitly but resolved
|
||||
-- through the reference manual's own pin (its v4.33.0-rc2 tag needs a
|
||||
-- verso nightly, not the verso tag of the same name). Mathlib is
|
||||
-- pinned to the same commit as before (a master snapshot on toolchain
|
||||
-- v4.33.0-rc2). Mathlib comes LAST so that its pins of shared
|
||||
-- dependencies (batteries, …) take precedence — otherwise
|
||||
-- `lake exe cache get` refuses to work.
|
||||
require «verso-manual» from git
|
||||
"https://github.com/leanprover/reference-manual.git"@"v4.33.0-rc2"
|
||||
require mathlib from git
|
||||
"https://github.com/leanprover-community/mathlib4"@"87adeaebd370a3b6a41ac4f044fddd4bf81803ad"
|
||||
|
||||
package «AlgebraInLean» where
|
||||
-- building the C code costs much more than the optimizations save
|
||||
moreLeancArgs := #["-O0"]
|
||||
-- work around clang emitting invalid linker optimization hints that lld rejects
|
||||
moreLinkArgs :=
|
||||
if System.Platform.isOSX then
|
||||
#["-Wl,-ignore_optimization_hints"]
|
||||
else #[]
|
||||
|
||||
/-- The exercise files that students open in VS Code. -/
|
||||
@[default_target]
|
||||
lean_lib «AlgebraInLean» where
|
||||
|
||||
/-- The Verso sources of the course notes. -/
|
||||
@[default_target]
|
||||
lean_lib «Book» where
|
||||
|
||||
/-- The generator executable: `lake exe algebrainlean --output _out`
|
||||
renders the course notes to `_out/html-multi`. -/
|
||||
@[default_target]
|
||||
lean_exe «algebrainlean» where
|
||||
srcDir := "./"
|
||||
root := `Main
|
||||
@@ -1,10 +0,0 @@
|
||||
name = "AlgebraInLean"
|
||||
defaultTargets = ["AlgebraInLean"]
|
||||
|
||||
[[require]]
|
||||
name = "mathlib"
|
||||
git = "https://github.com/leanprover-community/mathlib4"
|
||||
rev = "87adeaebd370a3b6a41ac4f044fddd4bf81803ad"
|
||||
|
||||
[[lean_lib]]
|
||||
name = "AlgebraInLean"
|
||||
@@ -0,0 +1 @@
|
||||
The directory `katex` contains KaTeX v0.16.11 (MIT license)
|
||||
@@ -0,0 +1,32 @@
|
||||
/* CSS variables for each Lean branding color */
|
||||
:root {
|
||||
/* Main color palette */
|
||||
--lean-black: #000000;
|
||||
--lean-white: #ffffff;
|
||||
--lean-blue: #0073a3;
|
||||
|
||||
/* Accent color palette */
|
||||
/* This light blue should only be used as a background, and any text
|
||||
on it should be black to ensure sufficient contrast. */
|
||||
--lean-accent-light-blue: #b0c5cd;
|
||||
/* This orange should be used only as an accent in small amounts. No
|
||||
small type. Bold subhead or larger for typography.*/
|
||||
--lean-accent-orange: #f15732;
|
||||
|
||||
/* Non-branding colors */
|
||||
/* These colors should never be used as actual brand colors, but they
|
||||
are complementary to our colors and can be used for elements in
|
||||
presentations or charts or other peripheral materials. They are
|
||||
only to be used as an accent or a complementary design element,
|
||||
never as Lean branding. */
|
||||
--lean-compl-orangered: #F15732;
|
||||
--lean-compl-yellow: #FDC05F;
|
||||
--lean-compl-green: #699E88;
|
||||
--lean-compl-bluegray: #A9C7C9;
|
||||
--lean-compl-darkgray: #354140;
|
||||
--lean-compl-gray: #96A0A5;
|
||||
--lean-compl-pink: #F05665;
|
||||
--lean-compl-lightpink: #F7A8B0;
|
||||
--lean-compl-darkblue: #005E7D;
|
||||
--lean-compl-turquoise: #48C6E2;
|
||||
}
|
||||
@@ -0,0 +1,93 @@
|
||||
© 2023 Adobe (http://www.adobe.com/), with Reserved Font Name 'Source'. All Rights Reserved. Source is a trademark of Adobe in the United States and/or other countries.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
|
||||
This license is copied below, and is also available with a FAQ at: http://scripts.sil.org/OFL
|
||||
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Loaded 100 of 269 files, more files were not shown because too many files have changed in this diff.
Show more
Reference in new issue
Block a user