Dieses Kapitel übersetzt den Satz über den Frobenius-Endomorphismus
aus Kapitel 14 des Skripts Satz für Satz nach Lean. Es geht um den
„Traum jedes Studienanfängers“: (a+b)^p = a^p + b^p.
„R hat Charakteristik p“ ist die Typklasse CharP R p.
Das entscheidende Lemma ist CharP.cast_eq_zero: Das Bild von
p in R ist Null.
Binomialkoeffizienten heißen Nat.choose; die binomische Formel
ist add_pow, eine Summe über Finset.range. Endliche Summen und
ihre Umformungen sind das Lean-Lernthema dieses Kapitels.
Satz und Definition 14.2.2 (Frobenius-Endomorphismus). Es sei
p eine Primzahl und es sei R ein kommutativer Ring mit Eins
der Charakteristik p. Dann ist die Abbildung
F : R \to R, a \mapsto a^p ein Ringmorphismus.
Beweis. Die Verträglichkeit mit der Multiplikation ist klar,
weil R kommutativ ist: (a \cdot b)^p = a^p \cdot b^p.
Ebenso ist F(1) = 1. Interessant ist nur die Verträglichkeit
mit der Addition. … Die binomische Formel gilt in jedem
kommutativen Ring, also ist
(a+b)^p = \sum_{k=0}^{p} \binom{p}{k} \cdot a^k \cdot b^{p-k}.
Für alle Indizes 0 < k < p ist der Binomialkoeffizient
\binom{p}{k} ein Vielfaches von p …. Weil R die
Charakteristik p hat, ist p = 0 in R, und alle diese
Summanden verschwinden. Übrig bleiben nur die Summanden für
k = 0 und k = p.
theoremfrobenius_mul{R:Type*}[CommRingR](p:ℕ)(ab:R):(a*b)^p=a^p*b^p:=mul_powabptheoremfrobenius_add{R:Type*}[CommRingR](p:ℕ)[Factp.Prime][CharPRp](ab:R):(a+b)^p=a^p+b^p:=R:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:R⊢ (a+b)^p=a^p+b^pR:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:Rhp:Nat.Primep⊢ (a+b)^p=a^p+b^p-- „Die binomische Formel gilt in jedem kommutativen-- Ring, also ist-- (a+b)^p = ∑ₖ (p über k)·a^k·b^{p−k}.“R:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:Rhp:Nat.Primep⊢ ∑m∈Finset.range(p+1),a^m*b^(p-m)*↑(p.choosem)=a^p+b^p-- „Für alle Indizes 0 < k < p ist der-- Binomialkoeffizient (p über k) ein Vielfaches von p-- …. Weil R die Charakteristik p hat, ist p = 0 in-- R, und alle diese Summanden verschwinden.“R:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:Rhp:Nat.Primephmid:∀k∈Finset.Ioo0p,a^k*b^(p-k)*↑(p.choosek)=0⊢ ∑m∈Finset.range(p+1),a^m*b^(p-m)*↑(p.choosem)=a^p+b^p-- „Übrig bleiben nur die Summanden für k = 0 und k = p.“R:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:Rhp:Nat.Primephmid:∀k∈Finset.Ioo0p,a^k*b^(p-k)*↑(p.choosek)=0hsplit:Finset.range(p+1)={0,p}∪Finset.Ioo0p⊢ ∑m∈Finset.range(p+1),a^m*b^(p-m)*↑(p.choosem)=a^p+b^pR:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:Rhp:Nat.Primephmid:∀k∈Finset.Ioo0p,a^k*b^(p-k)*↑(p.choosek)=0hsplit:Finset.range(p+1)={0,p}∪Finset.Ioo0phdisj:Disjoint{0,p}(Finset.Ioo0p)⊢ ∑m∈Finset.range(p+1),a^m*b^(p-m)*↑(p.choosem)=a^p+b^pR:Type u_1inst✝²:CommRingRp:ℕinst✝¹:Fact(Nat.Primep)inst✝:CharPRpa:Rb:Rhp:Nat.Primephmid:∀k∈Finset.Ioo0p,a^k*b^(p-k)*↑(p.choosek)=0hsplit:Finset.range(p+1)={0,p}∪Finset.Ioo0phdisj:Disjoint{0,p}(Finset.Ioo0p)⊢ a^0*b^(p-0)*↑(p.choose0)+a^p*b^(p-p)*↑(p.choosep)=a^p+b^p-- „(a+b)^p = (p über 0)·a⁰·b^p + (p über p)·a^p·b⁰-- = a^p + b^p.“All goals completed! 🐙
Mathlib bündelt die drei Verträglichkeiten zum Ringmorphismus
frobenius R p : R →+* R; die Additivität heißt dort
add_pow_char. Das Skript beobachtet, dass der Frobenius über einem
Integritätsring injektiv und über einem endlichen Körper sogar
bijektiv ist. Das führt zur Klassifikation endlicher Körper:
Zu jeder Primzahlpotenz p^n gibt es genau einen Körper mit
p^n Elementen. In Mathlib heißt er GaloisField p n.
Der Frobenius des Körpers \mathbb{F}_p ist die Identität: Für
jedes a \in \mathbb{F}_p ist a^p = a. Das ist ein alter
Bekannter: der kleine
Satz von Fermat aus unserem dritten Kapitel! In Mathlib heißt er
ZMod.pow_card. Öffnen Sie AlgebraInLean/Frobenius.lean und
ersetzen Sie das sorry durch einen Beweis.