FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 12 definitions, 9 propositions, 2 lemmas, 4 corollaries and 2 conventions.
Of the 29 statements checked against Lean, 12 are formalized somewhere and 17 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 17 | 59% | A documented search found no Lean statement of it anywhere. |
| in another Lean project | 7 | 24% | Some other Lean development has it; using it means porting that code. |
| in Mathlib | 5 | 17% | Mathlib states and proves it. |
| checked in total | 29 |
- Canonical source block: FC10 Serre Chapter 8, “Cohomology of Finite Groups”,
FC10-C08-U001–FC10-C08-U029, 29 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 C08:
mathlib5,project-existing0,package-import0,reference-port7,unmatched17.
Definition / construction
Let G be a finite group. In the group algebra \(\mathbf { Z } [ \mathbf { G } ]\) the element \(\sum \sigma \in { \mathfrak { G } } ^ { s }\) will be called the normand be denoted \(\pmb { \mathbb { N } } .\) Forevery \(\mathbf { G }\) module A, \(\aleph\) defines an endomorphism(alsodenoted \(\mathbf { N }\) ofAbytheformula
Formalized. Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::Rep.tateNorm, tateComplexConnectData — The Tate norm is the map from coinvariants to invariants used by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The norm endomorphism induces \(N^*:H_0(G,A)\to H^0(G,A)\).
Formalized. Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::Rep.tateNorm, tateComplexConnectData — The Tate norm is the map from coinvariants to invariants used by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
For a finite group \(G\), define \(\widehat H_0(G,A)=\ker N^*\) and \(\widehat H^0(G,A)=\operatorname{coker}N^*\), where \(N^*:H_0(G,A)\to H^0(G,A)\) is induced by the norm.
Formalized. Mathlib/RepresentationTheory/Basic.lean::Representation.norm; Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::Rep.tateNorm, tateComplexConnectData, tateComplex, tateComplex_d_neg_one, tateCohomology — For an arbitrary finite group, the Tate complex connects coinvariants to invariants by the norm; its degree 0 and -1 homology are exactly coker(N) and ker(N) modulo the adjacent boundaries, i.e. Serre’s two modified degree-zero groups.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition 1
Proposition1. If A is relatively projective, \(\hat { \mathbf { H } } _ { 0 } ( \mathbf { G } , \mathbf { A } ) = 0 = \hat { \mathbf { H } } ^ { \mathfrak { g } } ( \mathbf { G } , \mathbf { A } ) .\)
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Definition / construction
were defined. For \(q = 0 .\) this homomorphism is just the inclusion of \(\mathbf { A } ^ { \mathbf { G } }\) in \(A ^ { H }\) ;as \(\ N _ { \mathbf G } = \ N _ { \mathbf G / \mathbf H } \circ \ N _ { \mathbf H } .\) we have \(\mathbf { N _ { G } A } \subset \mathbf { N _ { H } A } .\) soby passage tothequotient, wegeta homomorphism \[ \operatorname{Res} \colon \widehat{H}^{0}(G,A) \to \widehat{H}^{0}(H,A). \]
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Definition / construction
For every \(q\in\mathbf Z\), restriction gives \(\operatorname{Res}:\widehat H^q(G,A)\to\widehat H^q(H,A)\), using cohomological restriction for \(q\ge0\) and the corresponding homological construction in negative degrees.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Proposition 2
Proposition 2.The restriction maps form a morphism of cohomological functors.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Definition / construction
For a short exact sequence \(0\to A\to B\to C\to0\), the norm diagram defines the connecting homomorphism \(\delta:\widehat H_0(G,C)\to\widehat H^0(G,A)\); this is the missing boundary joining the negative and non-negative Tate degrees.
Formalized. Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::tateComplex, tateCohomology, δ, exact₃, exact₁, isoGroupCohomology, isoGroupHomology — The native Tate complex splices homology and cohomology with the missing norm connecting map, exactly Serre’s all-integer definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
This leads us to define,with Tate,cohomology groups with positive and negative exponentsbythe formulas \[ \widehat{H}^{n}(G,A) = H^{n}(G,A) \ \ (n \geq 1), \qquad \widehat{H}^{0}(G,A) = A^{G}/N_{G}A, \qquad \widehat{H}^{-1}(G,A) = {}_{N}A/I_{G}A, \qquad \widehat{H}^{-n}(G,A) = H_{n-1}(G,A) \ \ (n \geq 2). \]
Formalized. Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean::tateComplex, tateCohomology, δ, exact₃, exact₁, isoGroupCohomology, isoGroupHomology — The native Tate complex splices homology and cohomology with the missing norm connecting map, exactly Serre’s all-integer definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
Corestriction \(\operatorname{Cor}:\widehat H^q(H,A)\to\widehat H^q(G,A)\) is defined in non-negative degrees by cohomological corestriction and in negative degrees by the corresponding homological construction.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Proposition 3
Proposition 3. The corestriction maps form a morphism of cohomological functors.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Proposition 4
Proposition 4.1f \(n = \mathrm { C a r d } \{ \mathrm { G / H } \}\) then CorRes=n
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Corollary 1
Corollary 1. 1f \(g\) is the order of \(\mathbf { G }\) ,then all the:groups \(\hat { { \bf { H } } } ^ { q } \{ { \bf { G } } , \mathbf { A } \}\) are annihilated by g.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Corollary 2
Corollary2.IfAis \(\pmb { \alpha }\) finitely generated abelian group (and isa G-module) then the \(\hat { \mathbb { H } } ^ { q } ( \mathbb { G } , \mathbb { A } )\) are finite groups.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Proposition 5
Proposition 5.1f \(\textbf { G }\) is a finite group,there exists one and only one family of homomorphisms(called cupproduct） \[ \hat { \Pi } ^ { p } ( \operatorname { G } , \operatorname { A } ) \otimes \hat { \Pi } ^ { q } ( \operatorname { G } , \operatorname { B } ) \hat { \Pi } ^ { p + q } ( \operatorname { G } , \operatorname { A } \otimes \operatorname { B } ) \] denoted \(( a , b ) \to a , b .\) which are defined for every pair of integers \(( p , q )\) and erery coupleofG-modules A,B,and which satisfy the following four properties: i)These homomorphism are morphisms of functors,when the two sides of thearrow are considered to be bifunctors covariant in(A,B). iiFor \(p = q \simeq \emptyset ,\) thecup product \(a , b\) is obtained by passage to the quotient of the natural map \(\mathbf { A } ^ { \mathbf { G } } \otimes \mathbf { B } ^ { \mathbf { G } } \{ \mathbf { A } \otimes \mathbf { B } \} ^ { \mathbf { G } }\) iii）if \(0 A A ^ { \prime } A ^ { \prime \prime } 0\) is an exact sequence of \(\textbf { G }\) -modules,and \(i f\) the sequence \[ 0 \to \mathbf { A } \otimes \mathbf { B } \to \mathbf { A } ^ { \prime } \otimes \mathbf { B } \to \mathbf { A } ^ { \prime \prime } \otimes \mathbf { B } \to 0 \] is also exact,then forall \(a ^ { \prime \prime } \in \widehat { \mathbb { H } } ^ { p } \{ { \mathbb G } , { \bf A } ^ { \prime \prime } \}\) and \(\boldsymbol { b } \in \hat { \mathbb { H } } ^ { q } ( \mathbf { G } , \mathbf { B } )\) \[ \{ \delta a ^ { \prime \prime } \} . \dot { b } = \delta \{ a ^ { \prime \prime } . \dot { b } \} , \] where both sides are elements of \(\hat { \mathbf { H } } ^ { p + q + 1 } ( \mathbf { G } , \mathbf { A } \otimes \mathbf { B } )\) iv）1f \(0 \to \mathbb { B } \to \mathbb { B } ^ { \prime } \to \mathbb { B } ^ { \prime \prime } \to 0\) is an exact sequence of \(\mathbf { G }\) -modules,and if the sequence \[ \begin{array} { r } { \mathbb { 0 } \to \mathbf { A } \otimes \mathbb { B } \to \mathbf { A } \otimes \mathbb { B } ^ { \prime } \to \mathbf { A } \otimes \mathbb { B } ^ { \prime \prime } \to \mathbb { 0 } } \end{array} \] is alsoexact,then forall \(a \in \hat { \mathbb { H } } ^ { p } \{ { \bf G } , { \bf A } \}\) and \(\mathbf { \hat { \boldsymbol { b } } } ^ { \prime \prime } \in \hat { \mathbb { H } } ^ { \sigma } \{ \mathbb { G } , \mathbb { B } ^ { \prime \prime } \}\) \[ a . ( \delta b ^ { \prime \prime } ) = ( - 1 ) ^ { p } \delta \{ a , b ^ { \prime \prime } \} , \] where both sides are elements of \(\widehat { { \bf H } } ^ { p + q + 1 } \{ { \bf G } , { \bf A } \otimes { \bf B } \} .\)
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Corollary: Corollary
Corollary. The groups \(\widehat { { \bf H } } ^ { q } ( \widehat { { \bf G } } , { \bf A } )\) depend only on the parity of \(q\)
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::periodicCohomology, periodicTateCohomology — For a finite cyclic group, the external development proves the two-periodicity of Tate cohomology.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Convention / notation
For a finite cyclic group, regard the periodic cochain complex \(K(A)\) as \(\mathbf Z/2\)-graded and write \(H^0(A)\) and \(H^1(A)\) for its two cohomology groups; every short exact sequence of \(G\)-modules yields the associated exact cohomology hexagon.
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean; ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::exact_periodSeq₁, exact_periodSeq₂, periodicTateCohomology — The cyclic two-periodic D/N complex, its exact sequences, and its identification with Tate cohomology are implemented directly.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Definition / construction
iscalled the Herbrand quotient of A.In view of the periodicity of the cohomology,the Herbrand quotient is analogous to an Euler-Poincare characteristic.
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Defs.lean::Representation.herbrandQuotient, Rep.herbrandQuotient — This is the Herbrand quotient defined from the two Tate groups.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Definition / construction
[This analogy can be made precise in the framework of abelian categories. Suppose that A runs through the \(\mathbf { G }\) objectsofanabeliancategory \(\mathscr { C }\) and let \(\textcircled { 9 }\) be a subcategory of \(\mathscr { C }\) ;if we suppose that \(\mathbb { H } ^ { 0 } \{ \mathbb { A } \}\) and \(\mathbf { H } ^ { \mathbf { 1 } } \{ \mathbf { A } \}\) belong to \(\mathcal { D }\) we can define \(h ( A )\) to be \(\mathbf { H } ^ { 0 } \{ \mathbf { A } \} - \mathbf { H } ^ { 1 } \{ \mathbf { A } \} ,\) where this difference makes sense in the Grothendieck group \(\mathbb { K } ( \mathcal { D } )\) associated to \(\mathscr { D } .\)
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Definition / construction
If \(a \in \hat { \mathrm { H } } ^ { p } ( \mathrm { G } , \mathrm { A } ) , b \in \hat { \mathrm { H } } ^ { q } ( \mathrm { G } , \mathrm { B } )\) then \(\mathfrak { z } , b \in \hat { \mathbf { H } } ^ { p + q } \{ \mathbf { G } , \mathbf { A } \otimes \mathbf { B } \} .\) and we can take the image of \(a , b\) by \(\varphi\) It is an element of \(\hat { \mathbf { H } } ^ { p + q } ( \mathbf { G } , \mathbf { C } )\) that will still be called the cup product of \(\pmb { a }\) and \(b\) relative to \({ \pmb \varphi } .\) and will be denoted \(a \mathcal { . } _ { \varphi } b\) (or simply \(a , b\) when there is no ambiguity about \(\varphi\) 1
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Definition / construction
For a cyclic group \(G=\langle s\rangle\) of order \(n\), let \(D=s-1\) and \(N=\sum_{g\in G}g\). The two-periodic complex \(K\) has one copy of \(\mathbf Z[G]\) in each degree with differentials alternating between multiplication by \(D\) and \(N\); for a \(G\)-module \(A\), put \(K(A)=K\otimes_{\mathbf Z[G]}A\).
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean; ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::exact_periodSeq₁, exact_periodSeq₂, periodicTateCohomology — The cyclic two-periodic D/N complex, its exact sequences, and its identification with Tate cohomology are implemented directly.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Proposition 6
Proposition 6. The cohomological functor \(\{ \mathrm { H } ^ { q } \{ \mathrm { K } ( \quad ) , \delta \}\) is isomorphic to the functor \(\big \{ \mathbf { H } ^ { q } \{ \mathbf { G } , \quad \} , \delta \big \}\)
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean; ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean::exact_periodSeq₁, exact_periodSeq₂, periodicTateCohomology — The cyclic two-periodic D/N complex, its exact sequences, and its identification with Tate cohomology are implemented directly.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Proposition 7
Proposition 7.Given an exact sequence \(0 \to \mathbf { A } \to \mathbf { B } \to \mathbf { C } \to 0\) ofG-modules for which at least twoof the three Herbrand quotients \(\beta _ { 1 } \{ \mathrm { A } \} , \beta _ { 2 } ( \mathbb { B } ) , \beta _ { 1 } ( \mathrm { C } )\) are defined. Thenthe third is alsodefined and we have \[ h \{ { \bf B } \} = h \{ { \bf A } \} . h \{ { \bf C } \} . \]
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/SES.lean::herbrandSixTermSequence, herbrandQuotient_eq_of_shortExact — The six-term exact sequence proves multiplicativity of the Herbrand quotient in short exact sequences.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Proposition 8
Proposition 8. If \(A\) is a finite \(G\)-module, then its Herbrand quotient is \(h(A)=1\).
Formalized. ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Finite.lean::herbrandQuotient_of_finite — The external theorem is exactly h(A)=1 for finite cyclic G-modules.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Corollary: Corollary，Let A and B be G-modules, \(f : \mathbf { A } \mathbf { B }\) a…
Corollary，Let A and B be G-modules, \(f : \mathbf { A } \mathbf { B }\) a G-homomorphism with finitekernel and cokernel.Then A and B have the same Herbrand quotient.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Definition / construction
If the groups \(\pmb { p } ^ { \hat { \mathbf { A } } }\) and \(\mathsf { A } _ { p }\) are finite,we can define the“trivial Herbrand quotient of \(\mathbf { A } ^ { * }\) denoted \(\phi \{ \mathbf { A } \} ,\) to be the quotient of the order of \(\mathbf { A } _ { p }\) bythat of \(p ^ { \hat { A } }\) Thenext proposition,due to Tate, generalizes a theorem of Chevalley ([17], th. 10.3).
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Proposition 9
Proposition9.LetA bea G-module forwhich \(\varphi ( \mathsf { A } )\) isdefined(i.e.,the kernel and cokernel of \(p : \mathsf { A } \to \mathsf { A }\) are finite).Then \(\varphi ( \mathbf { A } ^ { \mathbf { G } } ) , \varphi \{ \mathbf { A } _ { \mathbf { Q } } \}\) and \(h ( A )\) are defined, andthey satisfy the equations \[ h ( \boldsymbol { \mathsf { A } } ) ^ { p - 1 } = \varphi \{ \boldsymbol { \mathsf { A } } ^ { G } \} ^ { p } / \varphi ( \boldsymbol { \mathsf { A } } ) = \varphi ( \boldsymbol { \mathsf { A } } _ { G } ) ^ { p } / \varphi ( \boldsymbol { \mathsf { A } } ) . \]
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Lemma 1
Lemma 1. Let \(0 \to \mathbf { A } ^ { \prime } \to \mathbf { A } \to \mathbf { A } ^ { \prime \prime } \to 0\) be anexact sequence of G-modules such that \(\varphi ( \boldsymbol { \mathsf { A } } ^ { \prime } )\) and \(\wp ( \mathsf { A } ^ { \prime \prime } )\) aredefined.Ifprop.9 holdsfor \(\mathbf { A ^ { \prime } }\) and A”,thenit also holds for A.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.
Lemma 2
Lemma 2.Let A be a G-module for which \(\varphi ( \mathsf { A } )\) is defined.Then there isan exact sequence ofG-modules \[ 0 \mathrm { A ^ { \prime } } \mathrm { A } \mathrm { A ^ { \prime \prime } } 0 \] such that \(\mathbf { A ^ { \prime } }\) is a finitely generated abelian group and \(\mathbf { A } ^ { \prime \prime } \equiv p \mathbf { A } ^ { \prime \prime }\) ; moreover \(\varphi \{ \mathsf { A } ^ { \prime } \}\) and \(\varphi ( A ^ { \prime \prime } )\) are defined.
Not formalized. Tate/cohomological infrastructure exists, but this full all-degree restriction/corestriction/cup/Herbrand statement is not proved by the checked compatible interfaces.