The class of a profinite extension by ๐ฝ_p in Hยฒ(G, ๐ฝ_p) #
The extension dictionary of TauCeti/Topology/Algebra/GroupExtension/Cohomology.lean classifies the
profinite extensions of a topological group G by a compact module M through the explicit
continuous cohomology group Hยฒ(G, M) of TauCeti.ContCohomology. The cohomology every dimension
count of the pro-p theory is stated on is instead Mathlib's continuousCohomology of the trivial
๐ฝ_p-representation, TauCeti.cohomFp p G 2, and the two are identified by
TauCeti.cohomFpAddEquivH2Additive for any trivial action of G on the multiplicatively written
๐ฝ_p. This file reads the class of a profinite extension of G by ๐ฝ_p, on which G acts
trivially, in cohomFp p G 2, so that the extensions by ๐ฝ_p and the cup products of classes of
Hยน(G, ๐ฝ_p) live in one group. The class vanishes exactly when the extension has a continuous
homomorphic section, and two extensions have the same class exactly when they are continuously
equivalent, and for profinite G every class is the class of an extension, so that the class is a
bijection from the extensions modulo continuous equivalence onto cohomFp p G 2; these are the
theorems of the dictionary transported along the identification.
Main declarations #
TauCeti.ProfiniteGroupExtension.cohomFpClass: the class inHยฒ(G, ๐ฝ_p)of a profinite extension ofGby๐ฝ_p.TauCeti.ProfiniteGroupExtension.cohomFpClass_eq_zero_iff: the class vanishes exactly when the extension has a continuous homomorphic section.TauCeti.ProfiniteGroupExtension.exists_equiv_continuous_iff_cohomFpClass_eq: two extensions are continuously equivalent exactly when their classes agree.TauCeti.ProfiniteGroupExtension.exists_cohomFpClass_eqandTauCeti.ProfiniteGroupExtension.cohomFpClassEquiv: for profiniteG, every class is the class of an extension, and the class is a bijection from the extensions modulo continuous equivalence ontocohomFp p G 2.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Ch. I, ยง2.
The class in Hยฒ(G, ๐ฝ_p) of a profinite extension of G by ๐ฝ_p with trivial action:
its class in the explicit continuous cohomology,
TauCeti.ProfiniteGroupExtension.contCohomologyClass, read in Mathlib's continuous cohomology of
the trivial ๐ฝ_p-representation.
Instances For
The class of a profinite extension by ๐ฝ_p in Hยฒ(G, ๐ฝ_p) is its class in the explicit
continuous cohomology, under the identification TauCeti.cohomFpAddEquivH2Additive.
A profinite extension by ๐ฝ_p has a continuous homomorphic section exactly when its class in
Hยฒ(G, ๐ฝ_p) vanishes.
Two profinite extensions by ๐ฝ_p are continuously equivalent exactly when their classes in
Hยฒ(G, ๐ฝ_p) agree.
Every class of Hยฒ(G, ๐ฝ_p) is the class of a profinite extension of G by ๐ฝ_p with
trivial action: TauCeti.ProfiniteGroupExtension.exists_contCohomologyClass_eq read on
cohomFp p G 2.
Hยฒ(G, ๐ฝ_p) classifies the profinite extensions of G by ๐ฝ_p with trivial action: the
class descends to a bijection from those extensions modulo continuous equivalence onto
cohomFp p G 2, the bijection TauCeti.ProfiniteGroupExtension.contCohomologyClassEquiv read on
cohomFp p G 2.