FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 3 definitions, 14 theorems, 1 proposition, 7 lemmas, 7 corollaries and 1 example.
Of the 33 statements checked against Lean, 4 are formalized somewhere and 29 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 29 | 88% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 4 | 12% | Mathlib states and proves it. |
| checked in total | 33 |
- Canonical source block: FC10 Serre Chapter 9, “Theorems of Tate and Nakayama”,
FC10-C09-U001–FC10-C09-U033, 33 units, in exact canonical order from Foundational corpus units FC10 Serre Local Fields. - Project code baseline:
A=3b2239e161592472b34e02ad3b7da308f9ce7280. The live repository moved only documentation/coordination files after A during this audit; no Lean source changed, so A is the semantic project baseline. - Pinned Mathlib:
P=db584cd6d46c92f209a44c0f1c829460d327499d; current Mathlib checked atH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Strict bundle semantics were used: partial ingredients never earn a route. - External CFT reference where cited:
ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509(Apache-2.0). Open Mathlib class-formation reference where cited: PR #42687 ata40561e249ebf45d2870f5d9d45bc2eb4d80b242(Apache-2.0). - Current Mathlib still marks higher ramification groups in lower numbering as TODO. Open/current local class-field-theory work does not supply a finished reciprocity/existence layer; unresolved/sorry-tainted downstream claims were not credited.
- Route totals for C09:
mathlib4,project-existing0,package-import0,reference-port0,unmatched29.
Definition / construction
Let \(p\) be a prime number. Recall that a finite group \(\textbf { G }\) is called a p-group if its order Card(G)is a power of \(p\)
Formalized. Mathlib/GroupTheory/PGroup.lean::IsPGroup — This is the p-group definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 1
Lemma 1. Suppose \(\mathbf { G }\) isa \(p\) group acting on a finite set E,and let E be the subset of elements fixed byG.Then \[ \operatorname { C a r d } ( { \mathrm { E } } ^ { \mathrm { G } } ) \equiv \operatorname { C a r d } ( { \mathrm { E } } ) \mod . p . \]
Formalized. Mathlib/GroupTheory/PGroup.lean::IsPGroup.card_modEq_card_fixedPoints — The fixed-point cardinality congruence is exactly Serre’s lemma.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 2
Lemma 2. 1f \(a p .\) group acts on a \(p\) group of order \(> \mathfrak { k }\) ,then the fixed points formasubgroupoforder \(> \mathfrak { k }\)
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 1
Theorem1.The center of a p-groupof order \(> \ddagger\) has order \(> 1\)
Formalized. Mathlib/GroupTheory/PGroup.lean::IsPGroup.center_nontrivial — This is the nontrivial-center theorem for a nontrivial p-group.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary: Corollary
Corollary. \(\pmb { A }\) group \(\mathbf { G }\) of order \(p ^ { \ast }\) admits a composition series \[ \{ 1 \} = \mathbf { G } _ { n } \subset \mathbf { G } _ { n - 1 } \subset \cdot \cdot \cdot \subset \mathbf { G } _ { 0 } = \mathbf { G } \]
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 2
Theorem 2.Every linear representation \(\neq 0\) ofa \(\pmb { p }\) groupoverafieldof characteristic \(\pmb { p }\) contains theunit representation.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Corollary: Corollary
Corollary. Let \(\pmb { G }\) bea \(p\) group,and let \(k\) bea field of characteristic \(p\) The kernel \({ \bf J } _ { G }\) ofthe augmentation homomorphism \(k [ \ G ] k\) is the radical of \(k [ G ]\) whichisanilpotent ideal.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 3
Theorem3(Sylow).Let G be a group of order \(n = p ^ { m } q\) with \(p\) prime and \(( p , q ) = 1\) .Then there exist subgroups of \(\mathbf { G }\) having order \(p ^ { m }\) (called Sylow \(p -\) subgroups); they are all conjugate to one another,and every \(\pmb { p }\) -group contained i \(\pmb { G }\) is contained in one of them.
Formalized. Mathlib/GroupTheory/Sylow.lean::Sylow, IsPGroup.exists_le_sylow, Sylow.isPretransitive_of_finite — Mathlib proves existence, conjugacy, and containment of p-subgroups in Sylow subgroups.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma 3
Lemma 3. 1f \(n = p ^ { m } q\) with \(\{ p , q \} = 1\) then \[ { \binom { n } { p ^ { n } } } \equiv q \mod p . \]
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Definition / construction
LetG be a finite group and Aa G-module.A is called cohomologically tricial if,for every subgroup H ofG and every \(\mathfrak { s a s } \mathbf { Z }\) \(\hat { \mathbb { H } } ^ { n } ( \mathbb { H } , \mathbb { A } ) = \mathbb { 0 }\)
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Example / comparison
EXAMPLEs.Every induced module is cohomologically trivial:indeed, such a module is also induced for every subgroup \(\mathbf { H }\) of \(\mathbf { G }\) ,and we saw in Chap.VIII, \(\ S 1\) that the cohomology vanishes.The same holds for relatively projective modules,since they are direct factors of induced modules.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Definition / construction
Let \(\mathcal { C }\) be the category of abelian groups, \(\mathbb { T } : \mathcal { C } \times \mathcal { C } \to \mathcal { C }\) anadditive bifunctor that we take to be bicovariant (to fix ideas).If A and B are \(\textbf { G }\) modules,define a \(\mathbf { G }\) -module structure on T(A,B) as follows:each \(s \in \mathbf { G }\) defines an element \(\mathbf { \Delta } _ { \mathbf { S } _ { A } } \in \mathrm { H o m } \{ \mathrm { A } , \mathrm { A } \}\) and an element \(s _ \mathbf \hat { \mathbf { \mathbf { \mathbf { \mathbf { \mathbf { \mathbf } { \mathbf } { \mathbf { \mathbf } { \mathbf \mathbf { \mathbf { \mathbf } \mathbf { \mathbf } { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf } { \mathbf \mathbf { \mathbf \mathbf } { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf } { \mathbf \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf } { \mathbf \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf } { \mathbf \mathbf \mathbf { \mathbf } \mathbf { \mathbf \mathbf } \mathbf { \mathbf \mathbf } { \mathbf \mathbf \mathbf { \mathbf } \mathbf \mathbf { \mathbf \mathbf } { \mathbf \mathbf \mathbf { \mathbf } \mathbf \mathbf { \mathbf \mathbf } \mathbf { \mathbf \mathbf } } } } } } } } } } } } } } } } } } } } } } } \mathbf { \mathbf { \mathbf \Delta \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \mathbf { \mathbf \Lambda } } } } } } } } } } } }\) hence an element \(\mathbb { T } ( s _ { \mathrm { A } } , s _ { \mathrm { B } } ) \in \mathbb { H } \mathrm { o m } \{ \mathbb { T } ( \mathrm { A } , \mathrm { B } ) , \mathbb { T } ( \mathrm { A } , \mathrm { B } ) \}\) ：thisis the automorphism of T(A,B) associated to s.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Proposition 1
Proposition1. If A is induced (resp.relatively projectire),then \(\mathrm { T } \{ \mathbb { A } , \mathbb { B } \}\) is induced (resp.relatively projective),hence cohomologically trivial.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Corollary: Corollary.Suppose one of the G-modules A,B is relatitely projective
Corollary.Suppose one of the G-modules A,B is relatitely projective. Then theG-modules below are relatively projective (hence cohomologically trivial): \[ \begin{array} { r } { \boldsymbol { \mathrm { A } } \otimes \boldsymbol { \mathrm { B } } , \quad \boldsymbol { \mathrm { H o m } } ( \boldsymbol { \mathrm { A } } , \boldsymbol { \mathrm { B } } ) , \quad \boldsymbol { \mathrm { T o r } } ( \boldsymbol { \mathrm { A } } , \boldsymbol { \mathrm { B } } ) , \quad \boldsymbol { \mathrm { E x t } } ( \boldsymbol { \mathrm { A } } , \boldsymbol { \mathrm { B } } ) . } \end{array} \]
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 4
Theorem 4. Let G be a finite group, \(p\) a prime number,and \(\mathbf { G } _ { p }\) a Sylow \(p \cdot\) subgroup of G.Then for every \(\mathbf { G }\) moduleAandevery \({ \mathfrak { n } } \in { \mathfrak { L } }\) ,therestriction homomorphism \[ \operatorname { \mathrm { R e s } } ; \widehat { \mathrm { H } } ^ { \pi } ( \mathrm { G } , \mathrm { A } ) \to \widehat { \mathrm { H } } ^ { \pi } ( \mathrm { G } _ { p } , \mathrm { A } ) \] is injective on the \(p\) primary component of \(\hat { \mathbf { H } } ^ { \prime } \{ \mathbf { G } , \mathbf { A } \}\)
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Corollary: Corollary.Let G bea finite group,Aa G-module,nan integer.Suppose that for…
Corollary.Let G bea finite group,Aa G-module,nan integer.Suppose that for every prime number \(p .\) \(\widehat { \mathbf { H } } ^ { n } ( \mathbf { G } _ { p } , \mathbf { A } ) = \boldsymbol { \mathfrak { 0 } }\) where \(\mathbf { G } _ { p }\) is a Sylow \(\pmb { p }\) -subgroup of G.Then \(\hat { \mathrm { H } } ^ { n } \{ \mathrm { G } , \mathrm { A } \} = 0 .\)
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Lemma 4
Lemma 4. Let \(\mathbf { G }\) hea \(p\) -groupand Aa G-module such that \(p _ { i } \mathbf { A } 0\) Then thethree following conditions are equivalent: i） \(\mathbf { A } \simeq \mathbb { 0 }\) i） \({ \displaystyle { \bf H } ^ { 0 } } \{ { \bf G } , { \bf A } \} = 0 .\) i） \(\mathrm { { \bf H } } _ { 0 } ( \mathrm { { \bf G } } , \mathrm { { \bf A } } ) = 0 .\)
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Lemma 5
Lemma 5.With the hypothesesof lemma \(\pmb { \ 4 }\) suppose that \({ \cal H } _ { \mathrm { \scriptsize ~ \{ ~ G , ~ A \} = ~ 0 , ~ } }\) Then Ais \(a\) free module over the algebra \(\varLambda = \mathbb { F } _ { p } [ \mathrm { G } ]\)
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 5
Theorem 5. Let \(\mathbf { G }\) bea \(p\) groupand A a G-module annihilated by \(p\) The following conditions are equivalent: i) There exists an integerq such that \(\widehat { { \bf H } } ^ { q } \{ { \bf G } , { \bf A } \} = 0\) ii）Ais cohomologically trivial, iii)Ais an induced G-module, iv) Aisa free \(\mathbf { F } _ { p } \mathbf { f } \mathbf { G } \mathbf \}\) module.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 6
Theorem 6. Let \(\textbf { G }\) be a \(p\) groupand letAbeaG-modulewithout \(p\) -torsion. Thefollowing conditionsare equivalent: i \(\hat { \bf H } ^ { q } ( { \bf G } , { \bf A } ) = 0\) for two consecutive values of \({ \mathfrak { q } } .\) ii）Aiscohomologically trivial, iii） the \(\mathbf { F } _ { p } \mathbf { f } \mathbf { G } ]\) -module \(A / p A\) isfree.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Corollary: Corollary.Let A bea Z-free G-module satisfying the equivalent conditions…
Corollary.Let A bea Z-free G-module satisfying the equivalent conditions oftheorem6.Then for every torsion-free G-module B,the G-module \(N =\) \(\mathbf { H o m } _ { \mathbf { Z } } ( . . \mathbf { \vec { A } } , \mathbf { \vec { B } } )\) iscohomologically trivial.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 7
Theorem 7.Let G bea finite group,A a Z-free G-module,and \(\mathbf { G } _ { p }\) a Sylow \(p\) subgroupofG,for each \(p\) The following conditions are equivalent： i) For every prime number \(p\) the \(\mathbf { G } _ { p }\) moduleAsatisfies theequivalent conditions of theorem6, iAis \(\mathbf { Z } \{ \ G \}\) -projective.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Lemma 6
Lemma 6. Let \(\mathbf { 0 } \to \mathbf { X } _ { 1 } \to \mathbf { X } _ { 2 } \to \cdots \to \mathbf { X } _ { n } \to 0\) be an exact sequence of Gmodules.If allbut oneofthe \(\mathbf { X } _ { \mathrm { i } }\) are cohomologically trivial,then that one also is.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 8
Theorem 8.Let A be any \(\textbf { G }\) module.The followingareequivalent: i） For every prime \(p\) \(\hat { \mathbf { H } } ^ { q } \{ \mathbf { G } _ { p } , \mathbf { A } \} = 0\) for two consecutive values of \(q\) (that may depend on p), ii）Aiscohomologically trivial, ii）Thereexists anexact sequence \(\Uparrow \ P _ { k } \ P _ { k - 1 } \cdot \cdot \cdot \ P _ { 0 } \mathrm { A } 0 ,\) where the \(p _ { i }\) are projective \(\mathbf { Z } [ \mathbf { G } ]\) -modules, iv) There exists an exact sequence \(\theta \mathbb { P } _ { 1 } \mathbb { P } _ { 0 } \mathbb { A } \mathbb { 0 }\) where the \(\mathfrak { P } _ { i }\) are Z[G]-projective.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 9
Theorem9.Let A,B be G-modules,with A cohomologically trivial.In order thatA \(\otimes \mathbf { B }\) (resp.Hom(A,B),resp.Hom(B,A))be cohomologically trivial,it is necessaryand suffcient that Tor(A,B) (resp.Ext(A,B),resp.Ext(B,A)) be.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Corollary: Corollary.If A iscohomologically trivial,and \(i f\) AorBis torsion-free,then…
Corollary.If A iscohomologically trivial,and \(i f\) AorBis torsion-free,then A \(\circledtimes\) Biscohomologically trivial.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Lemma 7
Lemma 7.Let G bea finite group,and let A be an injective Z[G]-module Then Ais \(\mathbf { z }\) injective,i.e.,divisible.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 10
Theorem 10 (Dual to Theorem 7).Let \(\mathbf { G }\) be a finite group,and let A be a Zinjective G-module.Inorder that Abecohomologically trivial,it is necessary and sufficient that A be \(\mathbf { Z } [ \mathbb { G } ]\) -injective.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 11
Theorem 11 (Dual to Theorem 8).In order that \(a\) G-module A be cohomologically trivial,it is necessary and sufficient that there bean exact sequence \(0 \to \mathbb { A } \to \mathbb { I } _ { 0 } \to \mathbb { I } _ { \mathrm { ~ t ~ } } \to 0 .\) where the \(\mathbf { l } _ { i }\) are injective \(\mathbf { Z } [ \mathbf { G } ]\) -modules.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 12
Theorem 12. Let \(\textbf { G }\) be \(a\) finite group,Aand \(\mathbf { A } ^ { * } \textbf { G }\) modules,and \(f \colon \mathbf { A } ^ { \prime } \mathbf { A } ~ a\) G-homomorphism.For each prime number \(\pmb { p } .\) let \(\mathbf { G } _ { p }\) be a Sylow \(p\) subgroup ofG,and suppose there is an integer \(n _ { \ p }\) such that the homomorphism \[ f _ { i } ^ { * } \colon \hat { \mathbf { H } } ^ { i } ( \mathbf { G } _ { p } , \mathbf { A } ^ { \prime } ) \hat { \mathbf { H } } ^ { i } ( \mathbf { G } _ { p } , \mathbf { A } ) \] is surjective for \(j = n _ { p }\) bijective for \(\mathfrak { i } = \mathfrak { n } _ { p } + 1\) ,injective for \(i = n _ { p } + 2\) IfB is \(^ a\) G-module such that Tor \(\mathbf { A } , \mathbf { B } \} = 0 = \operatorname { T o r } \{ \mathbf { A } ^ { \prime } , \mathbf { B } \}\) then the homomorphism \[ \hat { \mathbf { H } } ^ { i } ( g , \mathbf { A } ^ { \prime } \otimes \mathbf { B } ) \to \hat { \mathbf { H } } ^ { i } ( g , \mathbf { A } \otimes \mathbf { B } ) \] is bijective for every subgroup \(\pmb { \mathscr { g } }\) f \(\mathbf { G }\) and every integer i. In particular, \(\hat { \mathbf { H } } ^ { i } ( g , \mathbf { A } ^ { \prime } ) \to \hat { \mathbf { H } } ^ { i } ( g , \mathbf { A } )\) is bijective for all i.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 13
Theorem 13. Let \(\mathbf { G }\) be a finite group、A,B,C three G-modules,and let \(\varphi ; \mathrm { A } \times \mathrm { B } \mathrm { C }\) be a G-invariant bilinear map.Let \(q \in \mathbb { Z }\) \(a \in \hat { H } ^ { q } \{ \mathbf { G } , \mathbf { A } \}\) Given any subgroup \(g\) of \(\textbf { G }\) andany G-moduleD,denote by \[ f \{ n , g , \mathbf { D } \} \colon \widehat { \mathbf { H } } ^ { n } ( g , \mathbf { B } \otimes \mathbf { D } ) \widehat { \mathbf { H } } ^ { n + q } ( g , \mathbf { C } \otimes \mathbf { D } ) \]
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Theorem 14
Theorem 14.Let G bea finite group,Aa G-module,and \(a \in { \bf H } ^ { 2 } \{ { \bf G } , { \bf A } \}\) Let \(G _ { p }\) be aSylow \(p\) subgroupofG,foreach prime \({ p } ;\) and suppose that 1） \(\tilde { \bf H } ^ { 1 } ( { \bf G } _ { p } , { \sf A } ) = \tilde { \bf 0 } .\) 2） \(H ^ { 2 } ( G _ { p } , A )\) is generated by \({ \tt R e s } _ { { \tt G } ; { \tt G } _ { p } } \{ a \} ,\) and has order equal to that of \(\mathbf { G } _ { p }\) Then for any G-module \(\mathbf { p }\) such that \(\mathrm { T o r } ( { \bf A } , { \bf D } ) = 0 ,\) the cup product with \({ a _ { g } } = \operatorname { R e s } _ { G / g } ( a )\) inducesisomorphisms \[ \hat { \mathrm { H } } ^ { n } ( g , \mathrm { D } ) \hat { \mathrm { H } } ^ { n + 2 } ( g , \mathrm { A } \otimes \mathrm { D } ) \] for every integer nand every subgroup \(g\) ofG.
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.
Corollary
Corollary (Tate [63]).For every integer n and every subgroup \(g\) of \(\mathbf { G }\) the cup product with \(a _ { g }\) definesan isomorphism \[ \widehat { \bf H } ^ { n } \{ g , { \bf Z } \} \widehat { \bf H } ^ { n + 2 } \{ g , { \bf A } \} . \]
Not formalized. Mathlib has p-groups and Sylow theory, but this full cohomologically-trivial/projective criterion is not available as a checked theorem.