Continuous H² classifies profinite extensions #
Let G be a topological group acting continuously on a commutative topological group M. A
continuous factor set α : FactorSet G M — a normalized multiplicative 2-cocycle that is
continuous as a function on G × G — is a continuous 2-cocycle of the explicit complex of
continuous cochains once it is read additively, so it has a class in the explicit continuous
cohomology group H²(G, M) = Z²/B² of TauCeti.ContCohomology.H2. This file builds that class and
proves that it is a complete invariant of α modulo continuous coboundaries: two continuous
factor sets have the same class exactly when their quotient is the coboundary of a continuous
function (TauCeti.FactorSet.contCohomologyClass_eq_iff), and every class is the class of a
continuous factor set (TauCeti.FactorSet.exists_contCohomologyClass_eq). So the class descends
to a bijection TauCeti.FactorSet.contCohomologyClassEquiv from the continuous factor sets modulo
continuous cohomology onto H²(G, M).
Read through the extension dictionary, this classifies extensions of topological groups. Consider
an extension 1 → M → E → G → 1 of topological groups inducing the given action of G on M,
whose kernel is embedded (S.inl is an embedding) and which has a continuous normalized section.
It has a class, that of the factor set of the section, which does not depend on the section
(TauCeti.GroupExtension.contCohomologyClass_factorSet_eq); two such extensions, both with
continuous projection, are equivalent by a continuous equivalence exactly when their classes agree
(TauCeti.GroupExtension.exists_equiv_continuous_iff_contCohomologyClass_factorSet_eq), and equal
classes even yield a homeomorphic equivalence
(TauCeti.GroupExtension.exists_equiv_isHomeomorph_of_contCohomologyClass_factorSet_eq); and the
class vanishes exactly when the extension has a continuous homomorphic section
(TauCeti.GroupExtension.exists_splitting_continuous_iff_contCohomologyClass_factorSet_eq_zero).
For a profinite extension with compact kernel a continuous normalized section always exists, so
the class is an invariant of the extension itself, GroupExtension.contCohomologyClass, and the
two theorems take their final form
(GroupExtension.exists_equiv_continuous_iff_contCohomologyClass_eq,
GroupExtension.exists_splitting_continuous_iff_contCohomologyClass_eq_zero). When G and M
are both profinite the twisted product of a continuous factor set is such an extension, the bundled
TauCeti.ProfiniteGroupExtension.ofFactorSet of
TauCeti/Topology/Algebra/GroupExtension/Profinite.lean, and its class, read through the canonical
section, is the class of the factor set
(TauCeti.ProfiniteGroupExtension.contCohomologyClass_ofFactorSet), so every class of H²(G, M)
is the class of a profinite extension. On the bundled profinite extensions
TauCeti.ProfiniteGroupExtension of G by M inducing the given action, the class therefore
descends to the bijection TauCeti.ProfiniteGroupExtension.contCohomologyClassEquiv from the
profinite extensions modulo continuous equivalence onto H²(G, M). The trivial class is that of
the trivial factor set (TauCeti.FactorSet.contCohomologyClass_trivial), whose twisted product is
the semidirect product.
The classification is natural in the coefficient module. A continuous G-equivariant homomorphism
f : M →*[G] N of profinite modules pushes a factor set forward (TauCeti.FactorSet.map) and a
profinite extension forward (TauCeti.ProfiniteGroupExtension.map, the twisted product of the
pushforward of the factor set of a continuous section), and in both cases the class of the
pushforward is the image of the class under the coefficient map
TauCeti.ContCohomology.explicitCoeff2 of f, read additively
(TauCeti.FactorSet.contCohomologyClass_map,
TauCeti.ProfiniteGroupExtension.contCohomologyClass_map). So the bijection commutes with
pushforward (MulDistribMulActionHom.profiniteGroupExtensionContCohomologyClassEquiv_map).
Naturality also compares extensions by different kernels (Neukirch–Schmidt–Wingberg, I §5
Exercise 4, at ϕ = id). The extension X maps to its pushforward X.map f hf by a canonical
continuous homomorphism over the identity of G restricting to f on the kernels
(TauCeti.ProfiniteGroupExtension.mapHom). Hence, if f carries the class of X to the class of
an extension Y by N, then f is the restriction to the kernels of a continuous homomorphism
X.E → Y.E over the identity of G
(TauCeti.ProfiniteGroupExtension.exists_continuous_monoidHom_of_contCohomologyClass_map_eq);
conversely such a homomorphism forces f to carry the class of X to the class of Y
(TauCeti.ProfiniteGroupExtension.contCohomologyClass_map_eq_of_continuous_monoidHom). When f
is surjective the lift is surjective too, by GroupExtension.surjective_of_comp_inl_eq.
The coboundaries here are those of the continuous complex, B² being the image of the
continuous 1-cochains; this is what makes the classification a statement about topological
extensions. The abstract classification of TauCeti/GroupTheory/GroupExtension/Cohomology.lean
divides by all coboundaries and classifies abstract extensions. The continuous and the abstract
class of a factor set are different invariants, and it is the continuous one that the cohomology of
a profinite group computes with.
Main definitions #
TauCeti.FactorSet.contCohomologyClass: the class of a continuous factor set inH²(G, M).TauCeti.FactorSet.IsContCohomologous: two factor sets whose quotient is a continuous coboundary, withTauCeti.FactorSet.isContCohomologousSetoidthe equivalence relation it cuts out on continuous factor sets.TauCeti.FactorSet.contCohomologyClassEquiv:H²(G, M)classifies continuous factor sets up to continuous cohomology.GroupExtension.contCohomologyClass: the class of a profinite extension with compact kernel, in the root namespace so that it is available asS.contCohomologyClass.TauCeti.ProfiniteGroupExtension.continuousEquivSetoid: continuous equivalence of bundled profinite extensions, the kernel of the class map.TauCeti.ProfiniteGroupExtension.contCohomologyClassEquiv:H²(G, M)classifies profinite extensions ofGbyMinducing the given action up to continuous equivalence, as a bijection of sets.TauCeti.ProfiniteGroupExtension.continuousSection: a continuous normalized section of a profinite extension with compact kernel, chosen once and for all.TauCeti.ProfiniteGroupExtension.map: the pushforward of a profinite extension along a continuous equivariant homomorphism of profinite coefficient modules, andTauCeti.ProfiniteGroupExtension.mapHom, the canonical continuous homomorphism from the extension to its pushforward.
Main results #
TauCeti.FactorSet.contCohomologyClass_eq_iffandTauCeti.FactorSet.exists_contCohomologyClass_eq: the class is a complete invariant modulo continuous coboundaries, and it takes every value.TauCeti.GroupExtension.contCohomologyClass_factorSet_eq: the class of the factor set of a continuous normalized section does not depend on the section.GroupExtension.exists_equiv_continuous_iff_contCohomologyClass_eq:H²(G, M)classifies profinite extensions ofGbyMinducing the given action, up to continuous equivalence.GroupExtension.exists_splitting_continuous_iff_contCohomologyClass_eq_zero: a profinite extension has a continuous homomorphic section exactly when its class vanishes.TauCeti.ProfiniteGroupExtension.exists_contCohomologyClass_eq: for profiniteGandM, every class ofH²(G, M)is the class of a profinite extension.TauCeti.ProfiniteGroupExtension.subsingleton_H2_of_forall_exists_splitting: for profiniteGandM, if every profinite extension ofGbyMsplits continuously thenH²(G, M) = 0.TauCeti.FactorSet.contCohomologyClass_mapandMulDistribMulActionHom.profiniteGroupExtensionContCohomologyClassEquiv_map: the classification is natural in the coefficient module: the class of a pushforward is the image of the class under the coefficient map.TauCeti.ProfiniteGroupExtension.exists_continuous_monoidHom_of_contCohomologyClass_map_eqandTauCeti.ProfiniteGroupExtension.contCohomologyClass_map_eq_of_continuous_monoidHom: lifting a coefficient map along the class: a continuous equivariantf : M → Nis the restriction to the kernels of a continuous homomorphism of extensions over the identity ofGexactly when it carries the class of the source to the class of the target.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I §2, for the
correspondence between extensions of profinite groups and continuous
2-cocycles, and Ch. I §5 Exercise 4 for lifting a coefficient map along the class. - L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., Ch. 6 §8.
Continuous factor sets as continuous cocycles #
A continuous factor set, read additively, as a continuous 2-cocycle of the explicit complex
of continuous cochains.
Instances For
Continuously cohomologous factor sets: their pointwise quotient, read additively, is the
coboundary of a continuous 1-cochain, that is, it lies in B² of the explicit complex of
continuous cochains.
Equations
- α.IsContCohomologous β = ((fun (p : G × G) => Additive.ofMul (α p / β p)) ∈ TauCeti.ContCohomology.B2 G (Additive M))
Instances For
Being continuously cohomologous, spelled multiplicatively: the quotient of the two factor sets
is the coboundary (g, h) ↦ g • x h / x (g * h) * x g of a continuous x : G → M.
The class of a continuous factor set #
The class of a continuous factor set in the explicit continuous cohomology group
H²(G, M). Two continuous factor sets have the same class exactly when they are continuously
cohomologous (TauCeti.FactorSet.contCohomologyClass_eq_iff), and every class arises this way
(TauCeti.FactorSet.exists_contCohomologyClass_eq).
Equations
- α.contCohomologyClass hα = (TauCeti.ContCohomology.H2pi G (Additive M)) (α.toZ2 hα)
Instances For
The class does not depend on the proof of continuity, so a factor set can be replaced by an equal one underneath it.
Two continuous factor sets have the same class exactly when they are continuously cohomologous.
The class of a continuous factor set vanishes exactly when it is the coboundary of a continuous function.
Every class in H²(G, M) is the class of a continuous factor set. A continuous 2-cocycle
need not be normalized; subtracting the coboundary of the constant 1-cochain at its value at
(1, 1) normalizes it without moving its class.
Being continuously cohomologous is an equivalence relation on continuous factor sets: by
TauCeti.FactorSet.contCohomologyClass_eq_iff it is the kernel of the class map.
Equations
- TauCeti.FactorSet.isContCohomologousSetoid G M = Setoid.ker fun (α : { α : TauCeti.FactorSet G M // Continuous ⇑α }) => (↑α).contCohomologyClass ⋯
Instances For
H²(G, M) classifies continuous factor sets up to continuous cohomology. The class descends
to a bijection from the continuous factor sets of G with values in M, taken modulo the
continuously cohomologous relation, onto the explicit continuous cohomology group.
Equations
- TauCeti.FactorSet.contCohomologyClassEquiv G M = Setoid.quotientKerEquivOfSurjective (fun (α : { α : TauCeti.FactorSet G M // Continuous ⇑α }) => (↑α).contCohomologyClass ⋯) ⋯
Instances For
The class of the twisted product of α, read through its canonical section, is the class of
α, because TauCeti.GroupExtension.factorSet_canonicalSection reads α back off that section.
Naturality in the coefficient module #
The class of a continuous factor set is natural in the coefficient module: the class of the
pushforward α.map f along a continuous equivariant homomorphism f is the image of the class of
α under the coefficient map TauCeti.ContCohomology.explicitCoeff2 of f, read additively.
The class of an extension with a continuous normalized section #
Two continuous normalized sections give continuously cohomologous factor sets: their quotient is the coboundary of the difference of the sections, which is continuous.
The class of the factor set of a continuous normalized section does not depend on the section, so it is an invariant of the extension.
An extension has a continuous homomorphic section exactly when the class of the factor set
of a continuous normalized section vanishes. A continuous homomorphic section is a continuous
normalized section with trivial factor set; conversely a continuous primitive x of the factor set
of σ corrects σ to the homomorphic section g ↦ inl (x g)⁻¹ * σ g.
Equal classes give a homeomorphic equivalence. Two extensions of G by M, both inducing
the ambient action and both with continuous projection, embedded kernel and a continuous
normalized section, whose factor sets have the same class are equivalent by an equivalence that is
a homeomorphism: a continuous primitive of the quotient of the two factor sets rescales one twisted
product onto the other by TauCeti.FactorSet.rescaleEquiv, continuously in both directions, and
the comparison maps TauCeti.GroupExtension.factorSetToGroupExtensionEquiv with the extensions are
homeomorphisms.
Continuous H² classifies extensions with continuous normalized sections. Two extensions of
G by M, both inducing the ambient action and both with continuous projection, embedded kernel
and a continuous normalized section, are equivalent by a continuous equivalence exactly when the
classes of the factor sets of those sections agree.
Forwards, the transported section e ∘ σ is a continuous normalized section of S' with literally
the same factor set as σ, and the class of S' does not depend on the section it is read from.
Backwards, TauCeti.GroupExtension.exists_equiv_isHomeomorph_of_contCohomologyClass_factorSet_eq
even produces a homeomorphic equivalence.
Profinite extensions #
The class of a profinite extension with compact kernel in the explicit continuous
cohomology group H²(G, M): the class of the factor set of any continuous normalized section, of
which TauCeti.GroupExtension.exists_continuous_section provides one. By
GroupExtension.contCohomologyClass_eq the choice of section does not matter.
Equations
- S.contCohomologyClass hinl hrh hact = (TauCeti.GroupExtension.factorSet ⋯.choose ⋯ hact).contCohomologyClass ⋯
Instances For
The class of a profinite extension is the class of the factor set of any continuous normalized section.
Continuous H² classifies profinite extensions. Two profinite extensions of G by the
compact kernel M, both inducing the ambient action, are equivalent by a continuous equivalence
exactly when their classes agree. Such an equivalence is automatically a homeomorphism, the total
groups being compact and Hausdorff (TauCeti.GroupExtension.continuousMulEquivOfEquiv).
A profinite extension has a continuous homomorphic section exactly when its class vanishes.
The bijection #
The class of a profinite extension with compact kernel, GroupExtension.contCohomologyClass,
read on the bundled extension.
Equations
Instances For
Two profinite extensions are continuously equivalent exactly when their classes agree:
GroupExtension.exists_equiv_continuous_iff_contCohomologyClass_eq for bundled extensions.
Continuous equivalence of profinite extensions is an equivalence relation on the profinite
extensions of G by M inducing the given action: by
TauCeti.ProfiniteGroupExtension.exists_equiv_continuous_iff_contCohomologyClass_eq it is the
kernel of the class map, and TauCeti.ProfiniteGroupExtension.continuousEquivSetoid_apply reads
it back as the existence of a continuous equivalence.
Equations
Instances For
The class of the twisted product of α is the class of α: read it through the canonical
section, whose factor set is α.
Every class of H²(G, M) is the class of a profinite extension, namely of the twisted
product of a continuous factor set representing it.
H²(G, M) vanishes when every profinite extension splits: every class is the class of a
profinite extension, and the class of an extension with a continuous homomorphic section is zero.
Continuous H² classifies profinite extensions: the class descends to a bijection from the
profinite extensions of G by M inducing the given action, taken modulo continuous
equivalence, onto H²(G, M).
Equations
Instances For
The chosen section #
A continuous normalized section of a profinite extension with compact kernel, chosen once
and for all from TauCeti.GroupExtension.exists_continuous_section. The pushforwards
TauCeti.ProfiniteGroupExtension.map of X are the twisted products of the pushforwards of the
factor set of this section.
Equations
- X.continuousSection = ⋯.choose
Instances For
Naturality in the coefficient module #
Pushforward of a profinite extension along a continuous equivariant homomorphism f to a
profinite coefficient module: the twisted product of the pushforward along f of the factor set
of the chosen continuous normalized section TauCeti.ProfiniteGroupExtension.continuousSection of
X. Its class is the image of the class of X under the coefficient map of f
(TauCeti.ProfiniteGroupExtension.contCohomologyClass_map), which determines it up to continuous
equivalence, and X maps to it by the continuous homomorphism
TauCeti.ProfiniteGroupExtension.mapHom over the identity of G.
Equations
- X.map f hf = TauCeti.ProfiniteGroupExtension.ofFactorSet ((TauCeti.GroupExtension.factorSet X.continuousSection ⋯ ⋯).map f) ⋯
Instances For
The class of a profinite extension is natural in the coefficient module: the class of the
pushforward X.map f hf is the image of the class of X under the coefficient map
TauCeti.ContCohomology.explicitCoeff2 of f, read additively.
Pushforward respects continuous equivalence, so it descends to the quotient by
TauCeti.ProfiniteGroupExtension.continuousEquivSetoid.
The classification is natural in the coefficient module: the bijection
TauCeti.ProfiniteGroupExtension.contCohomologyClassEquiv commutes with pushforward along f on
the extensions and with the coefficient map of f on H².
Lifting a coefficient map along the class #
The canonical homomorphism from a profinite extension to its pushforward,
X.E → (X.map f hf).E: identify X.E with the twisted product of the factor set of its chosen
section, by the inverse of TauCeti.GroupExtension.factorSetToGroupExtensionEquiv, and apply f
to the M-coordinate (TauCeti.FactorSet.mapExtension). It is continuous
(TauCeti.ProfiniteGroupExtension.continuous_mapHom), covers the identity of G
(TauCeti.ProfiniteGroupExtension.rightHom_mapHom) and restricts to f on the kernels
(TauCeti.ProfiniteGroupExtension.mapHom_inl).
Equations
Instances For
The canonical homomorphism to the pushforward restricts to f on the kernels.
The canonical homomorphism to the pushforward covers the identity of G.
Lifting a coefficient map along the class (Neukirch–Schmidt–Wingberg, I §5 Exercise 4,
at ϕ = id). Let X be a profinite extension of G by M and Y one by N. If the
continuous equivariant f : M → N carries the class of X to the class of Y, then f is the
restriction to the kernels of a continuous homomorphism X.E → Y.E over the identity of G.
The converse is
TauCeti.ProfiniteGroupExtension.contCohomologyClass_map_eq_of_continuous_monoidHom, and the
lift is surjective when f is, by GroupExtension.surjective_of_comp_inl_eq.
The converse of the lifting lemma. A continuous homomorphism φ : X.E → Y.E over the
identity of G that restricts to the continuous equivariant f on the kernels carries the class
of X to the class of Y. The forward direction is
TauCeti.ProfiniteGroupExtension.exists_continuous_monoidHom_of_contCohomologyClass_map_eq.