FC10 — Jean-Pierre Serre, Local Fields (1979)

FC10 — Serre, Local Fields.

This chapter contains 30 definitions, 10 propositions, 2 corollaries, 1 example and 2 conventions.

Of the 45 statements checked against Lean, 22 are formalized somewhere and 23 are not.

Status	Statements	Share	What it means
not formalized	23	51%	A documented search found no Lean statement of it anywhere.
in Mathlib	18	40%	Mathlib states and proves it.
in another Lean project	4	9%	Some other Lean development has it; using it means porting that code.
checked in total	45

Which versions of Lean and Mathlib were searched

Canonical source block: FC10 Serre Chapter 7, “Basic Facts”, FC10-C07-U001–FC10-C07-U045, 45 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 at H=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 at a40561e249ebf45d2870f5d9d45bc2eb4d80b242 (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 C07: mathlib 18, project-existing 0, package-import 0, reference-port 4, unmatched 23.

Definition / construction

FC10-C07-U001 · Chapter VII, source L3797 · in Mathlib

Let $G$ be a group, written multiplicatively, and $A$ an abelian group, written additively. $G$ acts on the left on $A$ if a homomorphism $G \to \operatorname{Aut}(A)$ is given; equivalently, if a map $(s,a) \mapsto s.a$ from $G \times A$ to $A$ is given satisfying \[ 1.a = a, \qquad s.(a + a') = s.a + s.a', \qquad (s.t).a = s.(t.a). \]

Formalized. Mathlib/RepresentationTheory/Basic.lean::Representation; Mathlib/RepresentationTheory/Rep/Basic.lean::Rep — A G-module is represented by the corresponding group action/representation.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U002 · Chapter VII, source L3811 · after FC10-C07-U001 · in Mathlib

A $G$-homomorphism is a homomorphism of $G$-modules. A $G$-module $A$ is projective (respectively injective) when $\operatorname{Hom}_G(A,-)$ (respectively $\operatorname{Hom}_G(-,A)$) is exact.

Formalized. Mathlib/RepresentationTheory/Rep/Basic.lean::Rep; Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean::Projective; Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean::Injective — Morphisms in Rep are G-linear maps, and projective/injective objects are defined by exactness/lifting in the abelian category.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U003 · Chapter VII, source L3813 · after FC10-C07-U001 · not formalized

A $G$-module $A$ is induced if it has the form $\mathbb{Z}[G] \otimes X$ for an abelian group $X$, the tensor product taken over $\mathbb{Z}$; equivalently, if $A$ contains a subgroup $X$ with $A = \bigoplus_{s \in G} s.X$. Every $G$-module is a quotient of an induced one: writing $A_{0}$ for the abelian group underlying $A$, every element of $\mathbb{Z}[G] \otimes A_{0}$ is a sum of elements $s \otimes x$ with $x \in A_{0}$, $s \in G$, and sending such an element to $s.x \in A$ defines a homomorphism \[ \pi \colon \mathbb{Z}[G] \otimes A_{0} \to A, \] which is a surjective $G$-homomorphism.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U004 · Chapter VII, source L3819 · after FC10-C07-U003 · not formalized

Clearly $\mathfrak { F }$ isasurjective G-homomorphism;furthermore,if we set $\wp \left\{ a \right\} =$ $1 \otimes a .$ then $\pi \circ \varphi = 1$ (but,of course, $\varphi$ is not a G-homomorphism if $\textsf { A } \neq \mathbb { 0 }$ Thus we have a canonical way of writinga G-module as a quotient of an induced $\mathbf { G }$ -module. If $\pmb { \pi }$ mapsa direct factor of $A \otimes \mathbf { A } _ { \mathfrak { d } }$ (asa G-module) isomorphically onto A,we will say that $\mathbf { A }$ isrelatively projective (called “weakly projective”in Cartan-Eilenberg [13],Chap.X, $\ S 8$ ; these are the $\left. A , Z \right.$ -projective modules in the relative theory of Hochschild [35]).The relatively projective modules can also be characterised as the direct factors ofinduced modules.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U005 · Chapter VII, source L3829 · after FC10-C07-U001 · in Mathlib

A $G$-module is co-induced if it has the form $\operatorname{Hom}_{\mathbf Z}(\mathbf Z[G],X)$.

Formalized. Mathlib/RepresentationTheory/Coinduced.lean::coindV, coind, resCoindHomEquiv — This is the co-induced module Hom(Z[G],X), with its adjunction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U006 · Chapter VII, source L3829 · after FC10-C07-U005 · not formalized

A $G$-module is relatively injective if it is a direct factor of a co-induced module.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U007 · Chapter VII, source L3851 · after FC10-C07-U001, FC10-C07-U002 · in Mathlib

The cohomology groups $H^q(G,A)$ are the right derived functors of invariants $A\mapsto A^G$; equivalently, if $P_\bullet\to\mathbf Z$ is a projective $G$-resolution, then $H^q(G,A)=H^q(\operatorname{Hom}_G(P_\bullet,A))$.

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::groupCohomology, groupCohomologyIsoExt, groupCohomologyIso — Group cohomology is implemented as the derived invariants/Ext construction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U008 · Chapter VII, source L3891-L3895 · after FC10-C07-U007 · in Mathlib

of $\kappa ^ { i }$ as“inhomogeneous cochains”,i.e.,as functions $f \{ g _ { 0 } , \ldots , g _ { i } \}$ of $i$ arguments,with values in A,whose coboundary is given by: \[ \begin{array} { l } { d f ( g _ { 1 } , \dots , g _ { i + 1 } ) = g _ { 1 } . f ( g _ { 2 } , \dots , g _ { i + 1 } ) } \\ { \qquad + \displaystyle \sum _ { j = 1 } ^ { j * i } ( - 1 ) ^ { j } f ( g _ { 1 } , \dots , g _ { j } g _ { j + 1 } , \dots , g _ { i + 1 } ) } \\ { \qquad + ( - 1 ) ^ { i + 1 } f ( g _ { 1 } , \dots , g _ { i } ) . } \end{array} \]

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::inhomogeneousCochains, d — The native inhomogeneous cochain complex uses the standard Serre differential.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U009 · Chapter VII, source L3905 · after FC10-C07-U008 · in Mathlib

It iscalled alsoa crossed homqmorphism.Itisa coboundary ifthere exists $a \in A$ such that $\overbrace { \left| f ( g ) = g \cdot a - a \right| } ^ { }$ forall ${ \mathfrak { g } } \in { \mathbf { G } }$

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean::IsCocycle₁, IsCoboundary₁, IsCocycle₂, IsCoboundary₂, cocycles₁, cocycles₂ — The low-degree API is exactly crossed homomorphisms/coboundaries and factor sets.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U010 · Chapter VII, source L3917 · after FC10-C07-U008 · in Mathlib

It is also called a factor set.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition 1

FC10-C07-U011 · Chapter VII, source L3939 · after FC10-C07-U006, FC10-C07-U007 · not formalized

Proposition 1.If A isrelatively injective, $\mathbf { H } ^ { q } ( \mathbf { G } , \mathbf { A } ) = 0$ for all $q \geq 1$

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Corollary: Corollary

FC10-C07-U012 · Chapter VII, source L3949-L3953 · not formalized

Corollary. If $0 \to \mathrm { A } \to \mathrm { A } ^ { * } \to \mathrm { A } ^ { \prime } \to 0$ is an exact sequence of G-modules, with $A ^ { * }$ co-induced,then \[ \mathrm { H } ^ { q } ( \mathrm { G } , \mathrm { A } ^ { \prime } ) = \mathrm { H } ^ { q + 1 } \{ \mathrm { G } , \mathrm { A } \} \quad f o r q \geq 1 . \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U013 · Chapter VII, source L3961-L3975 · after FC10-C07-U007 · in Mathlib

A free resolution of $\mathbf { z }$ can be obtained by taking $\mathbf { P } _ { i }$ to be the free $\mathbf { Z }$ -module $\mathbf { L } _ { i }$ having basis the systems $( g _ { 0 } , \ldots , g _ { i } )$ of $i + 1$ elements of $\mathbf { G }$ and making $\mathbf { G }$ operate on $\mathbf { L } _ { i }$ by translations: \[ S \cdot \{ g _ { 0 } , . . . , g _ { i } \} = \{ s g _ { 0 } , . . . , s g _ { i } \} . \] The homomorphism $d \colon { \mathrm { L } } _ { i } \to { \mathrm { L } } _ { i - 1 }$ is defined by the formula \[ d ( g _ { 0 } , \dotsc , g _ { i } ) = \sum _ { j = 0 } ^ { j = i } ( - 1 ) ^ { j } ( g _ { 0 } , \dotsc , \hat { g } _ { j } , \dotsc , g _ { i } ) \] where the symbol ^means that the letter under it should be omitted. The homomorphism $\bf { L } _ { 0 } \bf { Z }$ is defined by mapping each $\{ g _ { 0 } \}$ onto $\yen 6$ The fact that the sequence $\mathbf { \partial } \cdot \cdot \cdot \mathbf { L _ { 1 } } \mathbf { L _ { 0 } } \mathbf { Z } 0$ so obtained is exact is well-known (a simplex is acyclic).

Formalized. Mathlib/RepresentationTheory/Homological/Resolution.lean::Rep.standardResolution, standardComplex; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean::inhomogeneousCochains, d — Mathlib supplies the standard free group resolution and its cochain differential.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U014 · Chapter VII, source L3983 · in Mathlib

The coboundary of $f$ is defined by the transpose of formula $f ( \ast )$ (left to the reader).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U015 · Chapter VII, source L3991 · after FC10-C07-U001 · in Mathlib

Let A bea G-module,and let DA be the subgroup of A generated by the $s , a - a , a \in \mathsf { A }$ $s \in \mathbb { G }$ The quotient $\mathbf { A } / \mathbf { D } \mathbf { A }$ will be denoted $\mathbf { A } _ { \mathbb { G } }$ ；it is the largest quotient module of A on which $\mathbf { G }$ actstrivially(whereas $A ^ { G }$ is the largest submodule enjoying the same property).

Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean::coinvariants, H0Iso; Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean::groupHomology, groupHomologyIsoTor — Coinvariants are H_0 and the higher groups are the derived/Tor group homology functors.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U016 · Chapter VII, source L3993 · after FC10-C07-U002, FC10-C07-U015 · in Mathlib

The functor $\mathbf { A } _ { \mathbb { G } }$ is additive and right exact. Its left derived functors are, bydefinition,the homology groups of $\textbf { G }$ with coefficients in A,denoted $H _ { q } { { , } $ They form a“homological functor”.We have $\mathbb { H } _ { 0 } ( \mathbb { G } , \mathbb { A } ) = \mathbb { A } _ { \mathbb { G } } \cong$ $\mathbf { Z } \otimes _ { A } \mathbf { A }$ and $\mathbb { H } _ { q } ( \mathbf { G } , \mathbf { A } ) = \mathbb { T } \mathrm { o r } _ { q } ^ { \boldsymbol { \ A } } ( \mathbf { Z } , \mathbf { A } )$ f $\{ \pmb { \mathrm { P } } _ { i j } \}$ is a projective resolution of $\mathbf { Z }$ the $\mathbb { H } _ { q } ( \mathbf { G } , \mathbb { A } )$ are the homology groups of the complex formed by the $p _ { j } \otimes _ { i } A$

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC10-C07-U017 · Chapter VII, source L3995 · not formalized

[In a tensor product $\mathbf { \delta B } \otimes _ { A }$ A,we consider B as a right $\pmb { \cal A }$ -module by setting ${ \mathfrak { h } } . s = s ^ { - 1 } . b . ]$

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 2

FC10-C07-U018 · Chapter VII, source L4001 · after FC10-C07-U004, FC10-C07-U016 · not formalized

Proposition 2.If A is relatively projectice, $ _ { q } ( , ) = $ for all $q \geq 1$

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U019 · Chapter VII, source L4013 · after FC10-C07-U016 · in Mathlib

For the trivial $G$-module $\mathbf Z$, there is a canonical identification $H_1(G,\mathbf Z)\cong G/G^{\prime}$.

Formalized. Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean::H1AddEquivOfIsTrivial — Specializing the native H₁ calculation to the trivial Z-module gives the abelianization G/G′.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U020 · Chapter VII, source L4015-L4017 · not formalized

Let $\pi : A \to \mathbf { Z }$ be the augmentation of the group algebra $A = \mathbb { Z } [ G ]$ ie., the homomorphism that maps $\sum n _ { s } s \in A$ onto $\sum n _ { s } \in Z$ Let $\mathbf { l _ { G } }$ be the kernel of $\pi$ ; it is the subgroup of $\boldsymbol { A }$ generated by the elements $i _ { s } = s - 1$ ,assruns through G.A beingany G-module,we have by definition $\mathrm { H } _ { 0 } ( \mathrm { G } , \mathrm { A } ) = \mathrm { A } / \mathrm { J } _ { \mathrm { c } _ { 1 } } \mathrm { A }$ Consider the exact sequence \[ 0 \to I_{G} \to \mathbb{Z}[G] \xrightarrow{\ \pi\ } \mathbb{Z} \to 0. \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Convention / notation

FC10-C07-U021 · Chapter VII, source L4029 · after FC10-C07-U019, FC10-C07-U020 · not formalized

Henceforth $H_1(G,\mathbf Z)$ is identified with $G/G^{\prime}$ via the augmentation-ideal construction recalled above.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U022 · Chapter VII, source L4033 · after FC10-C07-U001, FC10-C07-U007 · in Mathlib

For a homomorphism $f:G^{\prime}\to G$ and a $G$-module $A$, restriction of the action gives the $G^{\prime}$-module $f^*A$; functoriality of derived cohomology gives maps $f_q^*:H^q(G,A)\to H^q(G^{\prime},f^*A)$ for every $q\ge0$.

Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean::groupCohomology.map; Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean — Functoriality in a compatible group/module map supplies the source maps; subgroup inclusion specializes to restriction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U023 · Chapter VII, source L4039 · in Mathlib

then A is provided with a structure of $\mathbf { G } ^ { \prime }$ -module,which we denote $f ^ { \ast } A$ (orsimply Aif that does not lead to confusion).Clearly $\mathsf { A } ^ { \mathsf { G } }$ is a subgroup of $( f ^ { \ast } \mathbf { A } ) ^ { 0 }$ This defines a morphism of the functor $\mathbb { H } ^ { \mathfrak { o } } \{ \mathbb { G } , \mathbb { A } \}$ into the functor $\mathrm { H } ^ { 0 } \{ \mathrm { G } ^ { \prime } , f ^ { * } \mathrm { A } \}$ ;as the $H ^ { q } \{ \mathbf { G } ^ { \prime } , f ^ { * } \mathbf { A } \}$ form acohomological functor (with respect to A).the universal property of derived functors (cf.Grothendieck [26]) shows that the morphism above extends toamorphism of the cohomological functor $\{ \bar { \mathsf { H } } ^ { q } ( \mathsf { G } , \mathrm { ~ ~ \lambda ~ } ) , \delta _ { \downarrow } ^ { \uparrow }$ into the cohomological functor $\{H^{q}(G', f^{*}A), \delta'\}$.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U024 · Chapter VII, source L4053 · after FC10-C07-U022 · in Mathlib

More generally,consider a $\mathbf { G } ^ { \prime }$ -module A’and anadditive map $g : { \mathsf { A } } { \mathsf { A } } ^ { \prime }$ We say that $f$ and $\mathfrak { g }$ are compatible when $g ( f ( s ^ { \prime } ) , a ) = s ^ { \prime } . g ( a )$ forall $\underline { s } ^ { \prime } \in \underline { G } ^ { \prime } ,$ $\square \in \square$ thisamounts to saying that $\pmb q$ isa $\mathbf { g } ^ { \prime }$ homomorphismof $f ^ { \ast } A$ intoA The map ${ \pmb g }$ thus defines a homomorphism \[ H^{q}(G', f^{*}A) \to H^{q}(G', A'). \]

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U025 · Chapter VII, source L4065 · after FC10-C07-U024 · in Mathlib

which is said to be associated to the pair $\left\{ f , g \right\}$ : the expression of this homomorphism in terms of standard cochains is left to the reader.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Example / comparison

FC10-C07-U026 · Chapter VII, source L4109-L4113 · in Mathlib

ExAMPLEs.1) If $\mathbf { H }$ is a subgroup of $\mathbf { G }$ and $f$ is the inclusion of $\mathbf { H }$ into $\textbf { G }$ we get homomorphisms \[ \mathbb { H } ^ { q } ( \mathbb { G } , \mathbb { A } ) \to \mathbb { H } ^ { q } \{ \mathbb { H } , \mathbb { A } \} \]

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U027 · Chapter VII, source L4115 · after FC10-C07-U022 · in Mathlib

which are called restriction homomorphisms,denoted Res.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC10-C07-U028 · Chapter VII, source L4123 · after FC10-C07-U022 · in another Lean project

which are called inflation,denoted Inf.

Formalized. ClassFieldTheory/Cohomology/Functors/Inflation.lean::cochain_infl, infl, infl_δ_naturality — The external CFT development packages the quotient-group inflation map and its compatibility with connecting morphisms.

Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)

Definition / construction

FC10-C07-U029 · Chapter VII, source L4139 · after FC10-C07-U022 · not formalized

For an inner automorphism $s\mapsto tst^{-1}$ of $G$ and the compatible map $a\mapsto t^{-1}a$ on a $G$-module, denote the induced automorphism of $H^q(G,A)$ by $\sigma_t$.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 3

FC10-C07-U030 · Chapter VII, source L4141 · not formalized

Proposition 3.The automorphisms $\pmb { \sigma } _ { \pmb { \xi } }$ areequal to the identity.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 4

FC10-C07-U031 · Chapter VII, source L4083-L4087 · not formalized

Proposition4. The sequence below is exact: \[ \begin{array} { r } { 0 \to \mathbb { H } ^ { 1 } ( { \mathrm { G } } / \mathbb { H } , { \mathrm { A } } ^ { \mathbb { H } } ) \xrightarrow { \operatorname* { l n f } } \mathbb { H } ^ { 1 } ( { \mathrm { G } } , { \mathrm { A } } ) \xrightarrow { \mathbb { R } \mathbb { e } \mathbb { s } } \mathbb { H } ^ { 1 } ( \mathbb { H } , { \mathrm { A } } ) . } \end{array} \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 5

FC10-C07-U032 · Chapter VII, source L4097-L4101 · not formalized

Proposition 5.Given a positive integer q.Suppose that $\mathbf { H } ^ { i } ( \mathbf { H } , \mathbf { A } ) = \mathbf { 0 }$ for \[ 1 \leq i \leq q - 1 . \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Corollary: Corollary.Inf

FC10-C07-U033 · Chapter VII, source L4157 · not formalized

Corollary.Inf: $\mathrm { H } ^ { i } \{ \mathrm { G / H , A ^ { H } } \} \mathrm { H } ^ { i } \{ \mathrm { G , A } \}$ is an isomorphism for $i \leq q - 1$ ，

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U034 · Chapter VII, source L4197-L4203 · after FC10-C07-U007 · in another Lean project

Suppose now that $\mathbf { H }$ has finite index in G.We will define homomorphisms in the opposite direction \[ \mathrm { C o r } : \mathbb { H } ^ { q } ( \mathbb { H } , \mathbf { A } ) \to \mathbb { H } ^ { q } ( \mathbb { G } , \mathbf { A } ) \] called corestriction.

Formalized. ClassFieldTheory/Cohomology/Functors/Corestriction.lean::cores₀, coresNatTrans, cores_res₀, cores_res — The compiled corestriction construction has the degree-zero norm and proves Cor∘Res=[G:H] in every nonnegative degree.

Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)

Definition / construction

FC10-C07-U035 · Chapter VII, source L4211-L4215 · after FC10-C07-U034 · in another Lean project

For a subgroup $H\subset G$ of finite index and $a\in A^H$, define the norm $N_{G/H}(a)=\sum_{s\in G/H}sa\in A^G$; this gives the degree-zero corestriction $H^0(H,A)\to H^0(G,A)$.

Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)

Proposition 6

FC10-C07-U036 · Chapter VII, source L4225 · after FC10-C07-U027, FC10-C07-U034 · in another Lean project

Proposition 6. 1f $\boldsymbol { n } = \mathbf { C } \mathbf { a r d } ( \mathbf { G } / \mathbf { H } )$ then CorRes=n.

Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)

Proposition 7

FC10-C07-U037 · Chapter VII, source L4261-L4265 · not formalized

Proposition 7. Let $\theta : \mathbb { H } \backslash \mathbb { G } \mathbb { G }$ beasystem of representations for the homogeneous space $H \backslash G$ of right cosets of $\mathbf { G }$ mod.H.For every $\pmb { \mathscr { s } } \in \mathbb { G }$ and $\pmb { \mathscr { t } } \in \mathbb { H } \backslash \mathbb { G }$ let $x _ { \uparrow , \uparrow }$ be the element of $\mathbf { H }$ givenbytheformula \[ \theta ( t ) , s = x _ { t , s } , \theta ( t , s ) , \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 8

FC10-C07-U038 · Chapter VII, source L4283-L4287 · not formalized

Proposition 8.Let $\pmb { x _ { i } }$ be a system of representatives of the double cosets $\mathbf { H } \mathbf { x } \bar { \mathbf { S } }$ andforeachi,define $f _ { i } = f _ { x _ { i } }$ as above.Then \[ \begin{array} { r } { \mathrm { V e r } ( s ) = \displaystyle \prod _ { i } x _ { i } . s ^ { f _ { i } } . x _ { i } ^ { - 1 } \mod . } \end{array} \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U039 · Chapter VII, source L4361 · not formalized

WriteAmultiplicatively. $\mathbf { H } ^ { 0 } \mathbf { ( G , A ) }$ is defined again as the group $A ^ { G }$ of elements ofA fixed by $\pmb { G }$ (i.e., $s ( a ) = a$ for all $s \in \mathbf { G }$ Bya cocycle will bemeant amap $\mathbb { S } \mapsto \mathbb { a } _ { s }$ of $\pmb { \ G }$ into A such that $a _ { s t } = a _ { s } \mathrm { . } s \{ a _ { \ast } \} .$ we say that ${ \mathfrak { a } } _ { s }$ and $b _ { s }$ are cohomologous if there exists $a \in A$ such that $\dot { b } _ { s } = a ^ { - 1 }$ $\pmb { a } _ { \textup { \pmb { s } } }$ $s ( a )$ forall $\mathfrak { s } \in \mathbb { G }$ This defines an equivalence relation for the set of cocycles,and the quotient set,provided with the structure of a distinguished element equal to the class of the unit cocycle $a _ { s } \simeq \mathfrak { f }$ (structure of“pointed set”),will be called the cohomology setof $\textbf { G }$ with values inA,and denoted $\mathbf { H } ^ { 1 } \mathbf { ( G , A ) }$ This definition coincides with the habitual definition when A is abelian,except that we onty retain from the group structure of $\mathbb { H } ^ { 1 } ( \mathbb { G } , \mathbf { A } )$ its underlying structure of pointed set.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U040 · Chapter VII, source L4363 · after FC10-C07-U039 · not formalized

A $G$-homomorphism $f:A\to B$ of possibly non-abelian $G$-groups induces maps $f_0:H^0(G,A)\to H^0(G,B)$ and $f_1:H^1(G,A)\to H^1(G,B)$, the latter a morphism of pointed sets.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 1

FC10-C07-U041 · Chapter VII, source L4387-L4391 · after FC10-C07-U039, FC10-C07-U040 · not formalized

Proposition 1. Let $1 \mathrm { A } \stackrel { i } { } \mathrm { B } \stackrel { \circ } { } \mathrm { C } 1$ be an exact sequence of non-abelian G-modules.Then the sequence of pointed sets below is exact: \[ 1 \to \mathbb { H } ^ { 0 } ( \mathbb { G } , \mathbb { A } ) { \overset { i _ { 0 } } { \to } } \mathbb { H } ^ { 0 } ( \mathbb { G } , \mathbb { B } ) { \overset { p _ { 0 } } { \to } } \mathbb { H } ^ { 0 } ( \mathbb { G } , C ) { \overset { \delta } { \to } } \mathbb { H } ^ { 1 } ( \mathbb { G } , \mathbb { A } ) { \overset { i _ { 1 } } { \to } } \mathbb { H } ^ { 1 } ( \mathbb { G } , \mathbb { B } ) { \overset { p _ { 1 } } { \to } } \mathbb { H } ^ { 1 } ( \mathbb { G } , \mathbb { C } ) . \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Proposition 2

FC10-C07-U042 · Chapter VII, source L4393-L4397 · after FC10-C07-U041 · not formalized

Proposition 2. In addition to the hypothesis of prop.1,assume that Ais in the center of B. Then the sequence of pointed sets below is exact: \[ \begin{array} { r l } & { 1 \mathrm { H } ^ { 9 } ( \mathbf { G } , \mathbf { A } ) \overset { i _ { 0 } } { } \mathrm { H } ^ { 0 } ( \mathbf { G } , \mathbf { B } ) \overset { p _ { 0 } } { } \mathrm { H } ^ { 0 } ( \mathbf { G } , \mathbf { C } ) \overset { \delta } { } \mathrm { H } ^ { 1 } ( \mathbf { G } , \mathbf { A } ) } \\ & { \qquad \overset { i _ { 1 } } { } \mathrm { H } ^ { 1 } ( \mathbf { G } , \mathbf { B } ) \overset { p _ { 1 } } { } \mathrm { H } ^ { 1 } ( \mathbf { G } , \mathbf { C } ) \overset { d } { } \mathrm { H } ^ { 2 } ( \mathbf { G } , \mathbf { A } ) } \end{array} \]

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U043 · Chapter VII, source L4413 · after FC10-C07-U039 · not formalized

By the kernel of a morphism of pointed sets we mean the pre-image of the distinguished element of the target set.This allows us to speak of an exact sequence of pointed sets.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U044 · Chapter VII, source L4415 · after FC10-C07-U039, FC10-C07-U043 · not formalized

For an exact sequence $1\to A\to B\to C\to1$ of non-abelian $G$-groups, define $\delta:H^0(G,C)\to H^1(G,A)$ by lifting $c\in C^G$ to $b\in B$ and taking the class of the cocycle $a_s=b^{-1}s(b)$.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.

Definition / construction

FC10-C07-U045 · Chapter VII, source L4433 · after FC10-C07-U010, FC10-C07-U044 · not formalized

If in addition $A$ is central in $B$, define $\Delta:H^1(G,C)\to H^2(G,A)$ by lifting a cocycle $c_s$ to $b_s\in B$ and taking the class of $a_{s,t}=b_s s(b_t)b_{st}^{-1}$.

Not formalized. Ordinary group (co)homology is formalized, but this full functorial/exact/nonabelian statement is not packaged by the checked APIs.