FC10 — Jean-Pierre Serre, Local Fields (1979)
FC10 — Serre, Local Fields.
This chapter contains 16 definitions, 11 propositions, 1 lemma, 6 corollaries, 9 examples and 3 conventions.
Of the 46 statements checked against Lean, 4 are formalized somewhere and 42 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 42 | 91% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 3 | 7% | Mathlib states and proves it. |
| in another Lean project | 1 | 2% | Some other Lean development has it; using it means porting that code. |
| checked in total | 46 |
- Canonical source block: FC10 Serre Chapter 10, “Galois Cohomology”,
FC10-C10-U001–FC10-C10-U046, 46 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 C10:
mathlib3,project-existing0,package-import0,reference-port1,unmatched42.
Proposition 1
Proposition 1. For every integer \(\eta , \hat { \mathsf { H } } ^ { \eta } ( \mathbf { G } , \mathbf { K } ) = 0 .\)
Formalized. ClassFieldTheory/Cohomology/IndCoind/Finite.lean::iso_ind₁; ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean::trivialTateCohomology_ind₁ — Normal-basis identification makes the additive Galois module induced; the external Tate-Shapiro layer proves vanishing in every Tate degree.
Searched: RCFT=ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0)
Proposition 2
Proposition 2. \(\mathbb { H } ^ { 1 } \{ \mathbf { G } , \mathbb { K } ^ { * } \} = 0\)
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean::H1ofAutOnUnitsUnique — This is multiplicative Hilbert 90: H¹(G,Kˣ) is trivial.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary
Corollary.If G is cyclic,and s isa generator,and if \(x \in \mathbb { K } ^ { * }\) has norm 1,then there exists \(y \in \mathbb { K } ^ { * }\) such that \({ x } = { y } / { s } ( { y } )\)
Formalized. Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean::exists_div_of_norm_eq_one — This is the cyclic norm-one equation x=y/s(y).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Prop.2 generalises as follows (cf.Speiser [60]): let \(\mathbf { G L } ( n , \mathbf { K } )\) be the group of invertible matrices of degreenwith entries from \(\mathbf { \delta K }\) ; the group \(\mathbf { G }\) acts in an obvious way on \(\mathbf { G L } ( n , \mathbb { K } )\) ,which allows us to define the cohomology set \(\mathbb { H } ^ { 1 } \{ \mathbf { G } , \mathbf { G L } ( n , \mathbb { K } ) \}\) –cf.Chap.VII,appendix.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 3
Proposition 3. \(\mathbf { H } ^ { 1 } ( \mathbf { G } , \mathbf { G L } ( n , \mathbf { K } ) ) = \{ 1 \} .\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Corollary: Corollary
Corollary. \(\mathbf { H } ^ { 1 } ( \mathbf { G } , \mathbf { S L } ( n , \mathbf { K } ) ) = \{ 1 \} .\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
Evidently \(p _ { s } \in A _ { \kappa }\) ;furthermore,a simple computation shows that \({ \mathfrak { s } } \mapsto { \mathfrak { p } } _ { s }\) is a 1-cocycle,and that changing \(f\) has the effect ofreplacing \({ p } _ { s }\) with an equivalent cocycle.Thus the class of \(\ p _ { s }\) in \(\mathbb { H } ^ { 1 } \{ \mathbb { G } , \mathbb { A } _ { \mathbb { K } } \}\) iswell-determined,and we have defined a map \[ \theta \colon E(K/k) \to H^{1}(G, A_{K}). \]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 4
Proposition 4.The map \(\boldsymbol { \theta }\) justdefinedisbijective.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
For a non-degenerate quadratic form \(\phi\), the descent set \(E(K/k)\) is the set of classes of quadratic \(k\)-forms that become \(K\)-isomorphic to \(\phi\), and the relevant automorphism group is the orthogonal group \(O_K(\phi)\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Corollary 1
Corollary 1. The set \(\mathbb { H } ^ { 1 } ( \mathbb { G } , \mathbb { O } _ { \mathbb { K } } ( \mathcal { P } ) )\) is in bijective correspondence with the set of classes of quadratic \(k\) formsthat are \(\pmb { \kappa }\) -isomorphicto \(\pmb { \phi }\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Convention / notation
Remark.Let A bea group scheme over \(k\) (or,in the terminology of Weil, a”group variety defined over \(k ^ { \dag \dag }\) .Foranycommutative \(k\) -algebra \(\mathbf { K }\) whatever, the set \(\mathsf { A } _ { \mathbb { X } }\) of points ofA withvalues in \(\pmb { \ K }\) isa group,depending functorially on K.In particular,if \({ \bf K } / k\) isa finite Galois extension with Galois group \(\textbf { G }\) ,then \(\mathbf { G }\) acts on \(\mathbf { A } _ { \mathbf { K } }\) ,and the cohomology \(\mathbf { H } ^ { q } ( \mathbf { G } , \mathbf { A } _ { \mathbf { K } } )\) is defined (if A is non-abelian,only \(\mathbf { H } ^ { 0 }\) and \(\sharp ^ { \tt t }\) are defined,and \(\mathbf { H } ^ { 1 }\) ismerelya“pointed set”).There is a simple geometric interpretation for \(\mathbf { H } ^ { \mathbf { i } } \{ \mathbf { G } , \mathbf { A } _ { \mathbf { k } } \}\) it is the set of classes of principal homogeneous spaces for A,defined over \(k ,\) which have a rational point in K (cf.[41],[113]).The cases treated above are \(\mathsf { A } = \mathsf { G } _ { \alpha }\) \(\mathbb { G } _ { m }\) ,GL(n), \({ \bf S L } ( n )\) ；in \(\ S 2\) we will examine the orthogonal and symplectic groups.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
Let \(\mathbf { V }\) be a vector space over \(k\) provided with a fixed tensor \(x\) of type \(( p , q )\) (i.e., \(x \in \bigotimes ^ { p } \mathbb { V } \otimes \bigotimes ^ { q } \mathbb { V } ^ { * }\) where \(\mathbf { V } ^ { * }\) is thedual ofV).Two pairs \(( \mathbb { V } , x )\) and \(( \mathbf { V } ^ { \prime } , x ^ { \prime } )\) are called \(k\) -isomorphicifthere isa \(k\) -linearisomorphism \(f \colon V \to V'\) with \(f^{*}(x) = x'\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
Now let \({ \bf K } / k\) be a finite Galois extension with group G.Let \(\mathbf { V _ { K } } = \mathbf { V } \otimes _ { \mathbf { k } } \mathbf { k }\) be the vector space over \(\mathbf { K }\) obtained by extending scalars；the tensor \(x\) defines a tensor \(x _ { \kappa }\) on \({ \bf { \cal V } } _ { \bf { \tilde { x } } }\) in the obvious way,and we will often denote it simply as \(x\) We say that \(( \mathbb { V } , x )\) and \(( \mathbf { V } ^ { \prime } , x ^ { \prime } )\) are \(\kappa\) -isomorphic(or”become isomorphic over \({ \bf K } ^ { \mathbf { \pi } ^ { \mathbf { \pi } } } .\) if \(\{ \mathbb { V } _ { \mathbb { K } } , \mathbb { x } _ { \mathbb { K } } \}\) and \(( \mathbb { V } _ { \mathbb { K } } ^ { \prime } , x _ { \mathbb { K } } ^ { \prime } )\) are isomorphic.Denote by \(\mathbb { E } _ { \mathbb { V } _ { s } \pmb { \imath } } \{ \mathbf { K } / k \}\) the set of \(\pmb { k }\) -isomorphismclasses of pairs \(( \boldsymbol { \nabla } ^ { \prime } , \boldsymbol { x } ^ { \prime } )\) that are K-isomorphic to \(( \mathbb { V } , x ) .\) We propose to interpret \(\mathbf { E } _ { \mathbf { V } , \mathbf { x } } { \left( \mathbf { K } / k \right) }\) as an \(\mathbf { H } ^ { \downarrow }\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Corollary
Corollary \(2 . \mathrm { H } ^ { 1 } ( \mathrm { G } , \mathrm { S p } ( n , \mathrm { K } ) ) = \{ \{ \} \} .\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
A \(G\)-module \(A\) for a profinite Galois group is called topological when every element has open stabilizer; equivalently, \(A=\bigcup_H A^H\) over the open normal subgroups \(H\triangleleft G\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
IfA is a topological \(\mathbf { G }\) module,define \(\mathbb { H } ^ { q } \{ \mathbf { G } , \mathbf { A } \}\) by the formula \[ H^{q}(G,A) = \varinjlim_{H} H^{q}(G/H, A^{H}), \] the limit being over the open normal subgroups \(H\) of \(G\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
In other words,the group \(\mathbf { H o m } ( \mathbf { G } , \mathbf { Z } / p \mathbf { Z } )\) ofcontinuous homomorphisms of \(\mathbf { G }\) into \(\mathbf { Z } / p \mathbf { Z }\) isisomorphic to \(k / \wp \{ k \}\) The isomorphism assigns to \(a \in k\) the homomorphism \(\varphi _ { a } \colon { \mathrm { G } } \to { \mathbf { Z } } / p { \mathbf { Z } }\) defined by solving the equation \(x ^ { p } - x = a\) and setting \({ \varphi } _ { a } \{ s \} = s ( x ) - x\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
Denote by \(k _ { p }\) the composite of all the abelian extensions of type \(( p , \ldots , p )\) of \(k\) ；thenwe see that the Galois group \(\mathbb { G } \{ k _ { p } / k \}\) is isomorphic to the compact dual \(( k / \xi ) \{ k \} \hat { \ }\) of the discrete group \(k / \wp \{ k \}\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
with \(\mu ( x ) = x ^ { n }\) Applying proposition 2,we deduce an isomorphism \(k ^ { \ast } / k ^ { \ast \pi } \mapsto\) \({ \mathrm { H o m } } \{ \mathbf { G } , \mu _ { n } \}\) This isomorphism assigns to an element \(a \in k ^ { * }\) the homomorphism \(\varphi _ { \alpha } \colon \mathrm { G } \to \mu _ { n }\) defined by solving the equation \(x ^ { n } = a\) and seting \(\varphi _ { a } \{ s \} =\) \(s \{ x \} , x ^ { - 1 }\) Denote by \(k _ { n }\) the composite of all the abelian extensions of \(k\) whose Galois group is annihilated by \(\pmb { n }\) ;then we see that the Galois group \(\operatorname { G } \{ k _ { n } / k \}\) is isomorphic to \(\mu _ { n } \otimes ( k ^ { * } / k ^ { * \eta } ) ^ { * }\) ,which is itself isomorphic （noncanonically) to \(( k ^ { * } / k ^ { * } ) ^ { * } )\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Convention / notation
For a finite or infinite Galois extension \(K/k\) with group \(G\), write \(H^q(K/k)=H^q(G,K^*)\); these groups are functorial in morphisms of Galois extensions.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 5
Proposition 5.The homomorphisms \(f _ { q }\) are independent of the choice of \(f\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
The Brauer group \(B_k\) is \(H^2(k_s/k)\) for a separable closure \(k_s\); equivalently, it is the direct limit of \(H^2(K/k)\) over finite Galois extensions \(K/k\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 6
Proposition 6. Let \(L / k\) bea Galois extension containing the Galois extension \({ \mathrm { \bf K } } / k .\) Then there is an exact sequence \[ 0 \to \mathbb { H } ^ { 2 } ( \mathbb { K } / k ) \to \mathbb { H } ^ { 2 } ( \mathbb { L } / k ) \to \mathbb { H } ^ { 2 } ( \mathbb { L } / \mathbb { K } ) . \]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Corollary: Corollary
Corollary. There is an exact sequence \[ \begin{array} { r } { { \boldsymbol { 0 } } { \mathbf { H } } ^ { 2 } ( { \mathbf { K } } / k ) { \mathbf { B } } _ { k } { \mathbf { B } } _ { \ k } . } \end{array} \]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 7
Proposition7.Let k bea field and A a finite dimensional \(k\) -algebra.The ollowing conditions are equivalent: a)Ahasno non-trivial two-sided ideal,and its center is \(\pmb { k }\) b) IfK is the algebraic closure of \(k _ { i }\) thentheextendedalgebrais isomorphic to a matrix algebra over K. 5）There exists a finite Galois extension \({ \bf K } / k\) such that \(\mathbf { A } _ { \mathbf { K } }\) is isomorphic to a matrix algebra over K. c)A is isomorphic to a matrix algebra over a division algebra with center \(k .\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
A finite-dimensional \(k\)-algebra that is simple and has center \(k\) is central simple over \(k\); two central simple algebras are equivalent when their associated division algebras are isomorphic.
Formalized. Mathlib/Algebra/BrauerGroup/Defs.lean::CSA, IsBrauerEquivalent, BrauerGroup; Mathlib/Algebra/Central/Defs.lean::Algebra.IsCentral — Mathlib has central simple algebras and the Brauer-equivalence quotient; no group law is credited to the following source row.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Let \(A _ { k }\) be the set of classes of central simple algebras (for the equivalence :elation just defined)；the tensor product defines by passage to the quotient 1structure of abelian group on \(\mathsf { A } _ { \star }\) .Thisis the group known classicially as :he“Brauer group”(cf.Bourbaki, loc.cit., \(\ S _ { \mathbf { I 0 } } )\) .It isa covariant functor of ifK is an extension of \(k\) ,then extension of scalars from \(k\) to \(\mathbf { K }\) defines a 1omomorphism
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Convention / notation
Denote by \(\mathbb { A } \{ \mathbb { K } / k \}\) thekernel ofthis homomorphism.Proposition 7implies hat \(A _ { k }\) is the union of the \(\mathbf { A } \{ \mathbf { K } / \hbar \}\) as \(\mathbf { K }\) runsthrough the set of finite Galois xtensions of \(k\) To show that \(\mathsf { A } _ { \pmb { k } }\) is isomorphic to \(\mathbf { B } _ { \star }\) itis enough to contruct isomorphisms \(\mathrm { A } \{ \mathrm { K } / k \} \to \mathrm { H } ^ { 2 } \{ \mathrm { K } / k \}\) compatible with the injections \[ A(K/k) \to A(K'/k) \qquad\text{and}\qquad H^{2}(K/k) \to H^{2}(K'/k). \]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
Let \(\mathsf { A } ( n , \mathsf { K } / k )\) be the set of classes of \(k\) -algebrasAsuch that \(A _ { \emptyset _ { k } } \subset\) is isomorphictothe matrixalgebra \(\mathbf { M } _ { n } ( \mathbf { K } )\) The group \(\mathsf { A } ( \mathbb { K } / k )\) is the union of the subsets \(\mathrm { A } ( n , \mathbb { K } / \tilde { \kappa } )\) for all positive \(\pmb { n }\) The procedure of \(\ S 2\) applies to \(\mathbb { A } \{ n , \mathbb { K } / k \}\) :an element of \(\mathbb { A } \{ n , \mathbb { K } / k \}\) can be considered as a pair \(( \mathbb { V } , x )\) ,where \(\mathbf { V }\) is a vector space of dimension \(n ^ { 2 }\) and where \(\pmb { x }\) is a tensor of type(1,2) (the law of composition),this pair being K-isomorphic to the standard pair defined by the matrix algebra \(\mathbf { M } _ { \pi }\) .If \(\mathbf { G }\) is the Galois group of \({ \mathbf { \tilde { K } } } / k .\) and \(C _ { K }\) denotes the group of \(\mathbf { K }\) -automorphisms of \(\mathbf { M } _ { \mathbf { r } } ( \mathbf { K } )\) we conclude that the map \[ \theta \colon A(n, K/k) \to H^{2}(G, C_{K}) \] defined in §2 is a bijection.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 8
Proposition 8.There isa canonical bijection \[ \theta \colon \mathsf { A } ( n , \mathsf { K } / k ) \to \mathsf { H } ^ { 1 } ( G , \mathsf { P G L } ( n , \mathsf { K } ) ) . \]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
The connecting map for \(1\to K^*\to GL_n(K)\to PGL_n(K)\to1\), composed with descent, gives compatible maps \(\delta_n:A(n,K/k)\to H^2(K/k)\) and hence a homomorphism \(\delta:A(K/k)\to H^2(K/k)\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 9
Proposition 9.The homomorphism \(\delta : \mathrm { A } \{ \mathrm { K } / k \} \mathrm { H } ^ { 2 } ( \mathrm { K } / k )\) is bijective.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Lemma 1
Lemma 1. 1f \(n = [ \mathbb { K } : \mathbb { k } ] .\) then themap \(\hat { \delta } _ { \pi } \colon \mathrm { A } \{ n , \mathrm { K } / k \} \mathrm { H } ^ { 2 } \{ \mathrm { K } / k \}\) is surjective.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
A field \(k\) is called quasi-algebraically closed (or \(\mathbf { C _ { 1 } }\) if it satisfies the following condition：
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 10
Proposition 10.1f the field \(k\) has property \(\mathbf { C _ { 1 } }\) ,then the Brauer group of every finiteextension K of \(k\) is zero.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Proposition 11
Proposition 11. For a given field \(k _ { \mathrm { { \ell } } }\) the following are equivalent: 1）The Brauer group of every finite separable extension of \(k\) is zero. 2）IfKis finite separable over \(k ,\) and \(L / \kappa\) isafinite Galois extension,then the \(\mathbb { G } \{ { \bf L } / \mathbb { K } \} .\) -module \({ \sf L } ^ { * }\) is cohomologically trivial. 3）With the same hypotheses as in2),the norm homomorphism \(\Nu _ { \tt L / \tt K } : \mathbb { L } ^ { \ast } \to \mathbb { K } ^ { \ast }\) is surjective.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Definition / construction
Let \(k\) be a ground field,and let \(\mathbf { p _ { \mathfrak { s } - \mathfrak { t } } }\) be the projective space of dimension \(n - 1\) ,considered asa scheme over \(k ,\) if \(\mathbf { v }\) is any scheme over \(k , \mathrm { \Delta V }\) is called a Severi-Brauer variety if there exists a separable algebraic extension \({ \tt K } / k\) such that V is isomorphic to \({ \bf P } _ { n - 1 }\) over \(\mathbf { K } ,\) for some \(\pmb { n }\) (i.e., \(\mathbf { V } \otimes _ { \mathbf { k } }\) K and \(\mathbf { P } _ { n - \textrm { f } } \bigotimes _ { \textrm { h } } \mathbf { K }\) are isomorphic K-schemes).This notion is due to Chatelet[15],[16].
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
EXAMPLEs.1 A non-singular conic in the projective plane is a Severi-Brauer variety of dimension 1:it is \(\mathbf { \check { K } }\) -isomorphic to \(\mathbf { p _ { i } }\) if and only if it has a rational point in K.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Corollary: Corollary.Let \(L / \mathbb { K }\) be anextension satisfying conditions…
Corollary.Let \(L / \mathbb { K }\) be anextension satisfying conditions 2).IfE isa torsionfree \(\mathrm { G } \{ { \bf E } / \mathrm { K } \}\) -module,then the \(\mathrm { G } \{ { \bf L } / \Re \}\) module \({ \mathbb { L } } ^ { * } \otimes { \mathbb { E } }\) is cohomologically trivial.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
a)Afinite field.Indeed,in this case, \(\mathbb { H } ^ { 1 } \{ \mathbb { G } , \mathbb { K } ^ { * } \}\) and \(\mathbb { H } ^ { 2 } \{ \mathbb { G } , \mathbb { K } ^ { * } \}\) have the same order (cf. Chap.VII, prop. 8),and as the first group is zero (prop. 2), so is the second. [One could just as well obtain this result by proving the stronger result that a finite field is \(\mathbf { C _ { 1 } }\) ; cf.[82],[115].]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
b)Themaximal unramified extension \({ \mathbf { K } } _ { n r }\) ofa field K complete under a discrete valuation and having perfect residue.field. Indeed,condition 3)of prop.11 holds (cf. Chap.V, \(\ S 4 .\) prop.7).This applies in particular to the casewhere theresidue field is algebraically closed. [Again the fields \({ \bf K } _ { n r }\) are actually \(\mathbf { C _ { 1 } }\) ；the proof (which is far from trivial) can be found in Lang’s thesis [38].]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
c)Anextension of transcendence degree l of an algebraically closed field In fact,such a field is \(\mathbf { C _ { j } }\) (“Tsen’s theorem”,cf.Lang, loc.cit.).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
d）An algebraic extension of \(\mathbf { Q }\) containing all the roots of unity. This follows,by passage to the limit,from the determination of the Brauer group ofa number field.[It has been conjectured by Artin that such a field is \(\mathbb { C } _ { 1 } . \mathbb { J }\)
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
e)The field R.Its Brauer group is equal to \(\mathbb { H } ^ { 2 } ( \mathbf { G } , \mathbf { C } ^ { * } )\) where \(\mathbf { G } = \mathbf { G } \{ \mathbf { C } / \mathbf { R } \}\) is cyclic of order 2.Hence(Chap.VIII, $4) \[ { \sf B } _ { \mathtt { R } } = { \sf C } ^ { \ast \mathrm { G } } / \mathrm { N C } ^ { \ast } = { \sf R } ^ { \ast } / { \sf R } _ { + } ^ { \ast } = { \sf Z } / 2 { \sf Z } . \] The non-zero element of \(\mathfrak { B } _ { \mathtt { R } }\) corresponds to the quaternions \(\mathbf { H }\) The corresponding Severi-Brauer variety is the conic \[ x ^ { 2 } + y ^ { 2 } + z ^ { 2 } = 0 . \]
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
A field complete under a discrete valuation with finite residue field has Brauer group isomorphic to \(\mathbf Q/\mathbf Z\).
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.
Example / comparison
For an algebraic number field \(k\), the local Brauer groups fit into the exact sequence \(0\to B_k\to\bigoplus_i B_{k_i}\to\mathbf Q/\mathbf Z\to0\), where the last map sums the local invariants.
Not formalized. The checked libraries have Hilbert 90, Kummer/Artin–Schreier ingredients and Brauer definitions, but not this full descent/cohomological-Brauer assertion.