FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 18 definitions, 2 theorems, 5 propositions, 6 corollaries, 3 conventions and 1 other statements.
Of the 35 statements checked against Lean, 5 are formalized somewhere and 30 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 30 | 86% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 5 | 14% | Mathlib states and proves it. |
| checked in total | 35 |
- Canonical source block: FC10 Serre Chapter 6, “Artin Representation”,
FC10-C06-U001–FC10-C06-U035, 35 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 C06:
mathlib5,project-existing0,package-import0,reference-port0,unmatched30.
Definition / construction
A complex-valued function on a finite group that is constant on conjugacy classes is a class function.
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
A representation of a finite group \(G\) is a homomorphism \(G\to GL(V)\) for a finite-dimensional complex vector space \(V\).
Formalized. Mathlib/RepresentationTheory/Basic.lean::Representation — This is the finite-dimensional linear representation notion used by Serre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The character of a representation \(V\) is the class function \(s\mapsto\operatorname{Tr}(s|V)\).
Formalized. Mathlib/RepresentationTheory/Character.lean::Representation.character, FDRep.character, FDRep.char_one — Characters are traces of the representing linear maps; evaluation at 1 is the dimension/degree.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The degree of a character is its value at the identity, equivalently the dimension of the representation.
Formalized. Mathlib/RepresentationTheory/Character.lean::Representation.character, FDRep.character, FDRep.char_one — Characters are traces of the representing linear maps; evaluation at 1 is the dimension/degree.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The constant function with value 1 will be denoted \({ \bf { i } } _ { \bf { G } }\) or simply 1. It is the character of the unit representation of \(\pmb { G }\) (dim \(\mathbf { V } \neq \mathbf { f }\) and \(\rho \{ s \} = 1\) for all \(s \in \mathbf { G } ;\)
Formalized. Mathlib/RepresentationTheory/Basic.lean::Representation.trivial; Mathlib/RepresentationTheory/Character.lean::FDRep.char_one — The one-dimensional trivial representation has constant character 1.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The character of the regular representation of \(G\) is the regular character.
Formalized. Mathlib/RepresentationTheory/Tannaka.lean::rightRegular, rightFDRep — Mathlib’s right regular representation is equivalent to Serre’s regular representation and determines the same regular character.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The augmentation representation is the quotient of the regular representation by the unit representation; its character is the augmentation character.
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
A character is irreducible when its representation is irreducible. Every class function has a unique expansion \(\varphi=\sum_{\chi}c_{\chi}\chi\) over the irreducible characters.
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
For class functions \(\varphi,\psi\) on a finite group \(G\), set \((\varphi,\psi)=|G|^{-1}\sum_{s\in G}\varphi(s)\overline{\psi(s)}\). The irreducible characters are orthonormal and \(c_{\chi}=(\varphi,\chi)\).
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
Next let \(\alpha : \mathbb { H } \mathbb { G }\) bea homomorphism of a finite group \(\mathbf { H }\) into G. If \(\varphi\) isa class function on \(\mathbf { G }\) the function \(\alpha ^ { * } ( \varphi ) = \varphi \circ \alpha\) is a class function on \(\mathbf { H }\) ；if \(\varphi\) is the character ofa linear representation \(\rho : { \mathrm { G } } \to { \mathrm { G L } } ( \mathbb { V } ) , x ^ { * } ( \varphi )\) is the character of the representation \(\rho \circ \alpha : { \mathrm { H } } { \mathrm { G L } } ( \mathbb { V } )\) Conversely,let \(\psi\) be a class function on H. It can be shown that there is a unique class function \(\alpha _ { * } ( \psi )\) on \(\textbf { G }\) such that the“Frobenius identity”
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Convention / notation
For a subgroup \(H\subset G\), write \(\psi^*\) for the class function induced from \(H\) to \(G\); explicitly \(\psi^*(s)=\sum_{t\in G/H}\psi(tst^{-1})\), with a summand interpreted as \(0\) when \(tst^{-1}\notin H\).
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Convention / notation
For a quotient map \(H\twoheadrightarrow G=H/N\), the push-forward of a class function is \(\psi_*(s)=|N|^{-1}\sum_{t\mapsto s}\psi(t)\).
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Brauer’s Theorem
Brauer’s Theorem.Every character ofa finite groupisaZ-linear combination of characters \(\chi _ { i } ^ { * }\) induced by characters \(\chi _ { j }\) ofdegree1 of subgroups \(\mathbf { H } _ { \mathrm { f } }\) of \(\mathbf { G }\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
Let \(L / \mathbb { X }\) bea finite Galois extension,with Galois group \(\mathbf { G }\) satisfying the hypotheses of Chaps.IV and V.Put \(f = [ { \boldsymbol { \bar { \mathbf { L } } } } : { \boldsymbol { \bar { \mathbf { K } } } } ]\) If \(s\) is an element of \(\mathbf { G }\) distinct from 1,we have defined in Chap. IV, \(\ S \ S\) the positive integer \(i _ { G } \{ s \}\) Set
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Theorem 1
Theorem 1. The function \(a _ { \Game }\) is the character of \(^ { a }\) linear representation of G.
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Theorem 1’
Theorem 1’. \(f ^ { \prime } ( \chi )\) is \(\pmb { a }\) non-negative integer for every character X of G. where \(\bigtriangledown ^ { \vec { \mathbf { u } } _ { i } }\) is the subspace ofV fixed by \(\mathbb { G } _ { i }\) and codim \(\mathbf { V ^ { G _ { i } } } = \dim \mathbf { V } - \dim \mathbf { V ^ { G _ { i } } }\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Corollary 2
Corollary 2.1f \(x\) is a character of \(\mathbf { G }\) then \(f ( \chi )\) is \(\pmb { \alpha }\) non-negative rational number.
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Proposition 3
Proposition 3.1f \(\aleph\) is \(\pmb { a }\) normal subgroup ofG,then \[ a _ { { \scriptscriptstyle { \bf G } } / { \bf N } } = \{ a _ { { \scriptscriptstyle { \bf G } } } \} a _ { \scriptscriptstyle { \bf \cdot } } \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Corollary
Corollary, \(\beta f \phi\) is \(^ a\) class function on \(\mathbf { G } / \mathbf { \mathfrak { N } } _ { \mathrm { : } }\) andif \(\varphi ^ { \prime }\) is the corresponding class function on \(\mathbf { G }\) ,then \(f \{ \varphi \} = f \{ \varphi ^ { \prime } \}\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Proposition 4
Proposition 4. Let \(\mathbf { H }\) be a subgroup of \(\mathbf { G }\) corresponding to the subextension \(\mathbf { K } / \mathbf { K } ,\) ond let \(\mathfrak { d } _ { \mathbf { K } ^ { \prime } ; \mathbf { K } }\) be thediscriminantof \({ \bf K } / { \bf K }\) Then \[ a _ { \mathrm { G } } \lvert \mathrm { H } = \lambda r _ { \mathrm { H } } + f _ { \mathrm { K ^ { \prime } / K } } . a _ { \mathrm { H } } , \quad w i t h \ \lambda = v _ { \mathrm { K } } ( \hat { v } _ { \mathrm { K ^ { \prime } / K } } ) . \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Corollary: Corollary
Corollary. \(1 6 \psi\) is a character of \(\mathbf { H }\) and \(\psi ^ { * }\) the character induced on G,then \[ f ( \psi ^ { * } ) = v _ { \mathrm { K } } ( \mathfrak { d } _ { \mathrm { K } ^ { \prime } / \mathrm { K } } ) \psi ( \mathfrak { t } ) + f _ { \mathrm { K } ^ { \prime } / \mathrm { K } } f ( \psi ) . \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Proposition 5
Proposition 5.Let \(\chi\) bea character of degree 1 on G.Let \(c _ { \chi }\) be the largest integer for which the restriction of \(\chi\) to theramification group \(\mathbf { G } _ { \varepsilon _ { \xi } }\) is not the unit character (if \(\chi = 1 _ { \ G }\) ,take \(c _ { x } \approx - 1 \}\) Then \[ f ( \chi ) = \varphi _ { \mathrm { L } / \kappa } ( c _ { \chi } ) + 1 . \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Corollary: Corollary
Corollary. Let \(\mathbf { H }\) be the kernel of \(\mathbb { X } ,\) let \(\kappa ^ { \prime }\) be the subextension of \(E / K\) corresponding to \(\mathbf { H }\) andlet \(\boldsymbol { c } _ { \boldsymbol { x } } ^ { \prime }\) be the largest integer forwhich \(\{ \mathrm { G } / \mathrm { H } \} _ { \mathrm { c } ^ { \star } \mathrm { x } } \neq 1\) Then \(f ( \chi ) = \varphi _ { \kappa ^ { \prime } ; \kappa } ( c _ { y } ^ { \prime } ) + 1\) and this isan integer \(\geq \emptyset\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
Terminology.The representation given in theorem 1 iscalled the Artin representation of the group G attached to the extension \(L / \mathbb { K }\) Notice that it has only been defined in terms of its character,i.e.,only up to an isomorphism； it would be very intersting to have a direct description of it；we will return to thispoint in \(\ S 4 .\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
if \(\chi\) is a character of \(\pmb { \ G }\) the ideal \(\mathfrak { p } _ { \bf K } ^ { f ( x ) }\) is called the conductor of \(\chi\) and denoted \(\{ \{ \chi \} .\) When \(\mathbb { X }\) has degree 1, corresponding to a cyclic subextension \(\mathbf { K } / \mathbf { K }\) and when \(\pmb { \mathrm { \tt K } }\) is finite, \(\boldsymbol { \mathfrak { f } } ( \boldsymbol { \chi } )\) is actually the conductor of the extension \(\mathbf { K } / \mathbf { K }\) ,in the sense of class field theory (cf. Chap.XV); the same holds when K isalgebraically closed (cf.[59]. \({ \mathfrak { n } } ^ { 0 } ~ 3 . 7 \}\) When \(\pmb { \chi }\) is an irreducible character of degree \(> 1\) ,no such interpretation is known for \(\widetilde { \mathfrak { f } } ( \chi ) .\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
As in §3, extend \(a_{\mathfrak{Q}}\) by zero outside \(D_{2}\) and set \[ a_{\mathfrak{P}} = \sum_{\mathfrak{Q} \to \mathfrak{P}} a_{\mathfrak{Q}} \qquad\text{for all } \mathfrak{P} \in X. \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
If we choose point \(\mathbf Q \in \mathbb Y\) over \(\mathbf { p } _ { \in } \mathbf { X } .\) it can be verified that \(a _ { \mathrm { p } } = \{ { \mathfrak { a } } _ { \mathrm { Q } } \} ^ { \ast }\) ; hence \(a _ { P }\) is the character of a representation of \(\mathbf { G }\) that is called the Artin representationattachedto \(\mathbf { P }\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
For a prime \(\mathfrak p\) and a prime \(\mathfrak P\) above it, the induced Artin character \(a_{\mathfrak p}=a_{\mathfrak P}^{*}\) is independent of the choice of \(\mathfrak P\); for a character \(\chi\) of \(G\), set \(f(\chi,\mathfrak p)=(\chi,a_{\mathfrak p})\).
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
The conductor of a character \(\chi\) is the ideal \(\mathfrak f(\chi)=\prod_{\mathfrak p}\mathfrak p^{f(\chi,\mathfrak p)}\).
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Proposition 6
Proposition 6 a) \(\mathfrak { f } ( \chi + \chi ^ { \prime } ) = \mathfrak { f } ( \chi ) . \mathfrak { f } ( \chi ^ { \prime } ) , \mathfrak { f } ( 1 ) = ( 1 ) .\) b \(J f K ^ { \prime } / K\) is a subextension of \(L / \mathbb { K }\) ,corresponding to the subgroup \(\mathbf { H }\) f \(\mathbf { G } ,\) andif \(\psi\) isa characterof \(\mathbf { H }\) then \[ \mathfrak { f } ( { \psi } ^ { * } , \mathrm { L } / \mathrm { K } ) = \mathfrak { d } _ { \mathrm { K } ^ { \prime } / \mathrm { K } } ^ { \psi ( 1 ) } . \mathrm { N } _ { \mathrm { K } ^ { \prime } / \mathrm { K } } \mathfrak { ( f ( \psi , \mathrm { L } / \mathrm { K } ^ { \prime } ) ) } . \] cIf \(K / \kappa\) is Galois,and if \(\chi\) is \(^ a\) character of \(\mathbf { G } / \mathbf { H } .\) then \[ \displaystyle \mathfrak { f } ( \boldsymbol { \chi } , \mathbf { L } / \mathbf { K } ) = \mathfrak { f } ( \boldsymbol { \chi } , \mathbf { K } ^ { \prime } / \mathbf { K } ) . \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Convention / notation
For \(H\subset G\), the character induced from the unit character of \(H\) is denoted \(s_{G/H}\); it is the permutation character of the action of \(G\) on \(G/H\).
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Corollary 1
Corollary 1 \(\mathfrak { s } _ { \mathsf { K } ^ { \prime } ; \mathsf { K } } = \mathfrak { f } ( \mathfrak { s } _ { \mathbf { G } ; \mathsf { H } } , \mathbf { L } / \mathbf { K } ) ,\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Corollary 2
Corollary 2. \(\mathfrak { d } _ { \mathtt { L } , \mathtt { f K } } = \prod \mathfrak { f } \{ \chi \} ^ { x \ t \mathtt { l } } )\) ，the product being taken over all irreducible characters \(\chi\) ofG.
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Definition / construction
Nextwe will interpret homologically the direct sum of the Artin representationscorresponding to the various points \(\mathbf { p } _ { \in } \mathbf { X }\) LetIbea fixed primenumber distinct from \(p\) Then the l-adic homology groupsof \(\mathbf { Y }\) can be defined (as in Weil [66]；see also \(\left\{ 5 7 \right\} , \ \pi ^ { 6 } \ 5 \}\) ,and one gets \(\mathbb { H } _ { 0 } ( \mathbb { Y } ) = \mathbb { H } _ { 2 } ( \mathbb { Y } ) = \mathbb { Z } _ { i }\) and \(\mathbf { H } _ { \mathfrak { t } } ( \mathbf { Y } ) = \mathbb { T } _ { \mathfrak { t } } ( \mathbf { J } )\) (Tate group of the Jacobian J of Y).These are free \(Z _ { i }\) modules offinite rank,on which the group \(\mathbf { G }\) acts.Therefore they define representations,whose characters will be denoted \(\not \} _ { 1 , ~ i } = 0 , 1 , 2 .\) Put \(h = h _ { 0 } - h _ { 1 } + h _ { 2 }\) The integer \(\operatorname { E } ( \mathbf { Y } ) = \hbar ( \mathbf { f } )\) is the Euler-Poincare characteristic of \(\mathbf { \bar { Y } }\) ：if \(g _ { \textsf { Y } }\) is the genus of \(\mathbf { Y }\) then \(\operatorname { E } \{ \mathrm { Y } \} = 2 - 2 g _ { \mathrm { Y } }\) Define similarly \(E ( \mathbf { X } ) = 2 - 2 g _ { \mathsf { X } }\)
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.
Proposition 7
Proposition 7.With the notation above, \[ \hbar = \operatorname { E } \{ \mathbf { X } \} . r _ { \operatorname { G } } - \sum _ { \mathbb { P } \in \mathbf { X } } a _ { \mathbb { P } } . \]
Not formalized. Generic representation/character theory exists, but this full Artin-character/conductor statement depends on the missing higher ramification layer or Brauer induction package.