Profinite extensions by a compact kernel are twisted products #
A group extension 1 → M → E → G → 1 is an extension of topological groups when its inclusion
and its projection are continuous. This file proves that, when E is profinite and the kernel M
is compact — in the application of the extension dictionary, finite and discrete — such an
extension is the twisted product of G by M built from a continuous factor set:
- the projection has a continuous normalized set-theoretic section
(
TauCeti.GroupExtension.exists_continuous_section); - the factor set that section measures is continuous
(
TauCeti.GroupExtension.continuous_factorSet); - the comparison map from the twisted product back to
Eis a multiplicative equivalence and a homeomorphism (TauCeti.GroupExtension.factorSetContinuousMulEquiv), assembled intoTauCeti.GroupExtension.exists_continuous_factorSet.
In the other direction TauCeti.GroupExtension.factorSet_canonicalSection reads a factor set back
off the twisted product it builds, through the canonical section, which is continuous by
TauCeti.FactorSet.continuous_canonicalSection. So the two constructions are mutually inverse up
to equivalence of extensions.
The continuous section is the only step that uses the topology of E in an essential way. It comes
from the continuous section of a profinite group over the quotient by a closed subgroup, applied to
the kernel, which is closed because it is compact and E, being profinite, is Hausdorff. Nothing
asks the kernel to be open: an open kernel would force G to be discrete, whereas the extensions
this dictionary is used on have infinite G.
Bundling the data, TauCeti.ProfiniteGroupExtension G M is an extension of G by M with
profinite total group, continuous inclusion and projection, inducing the given action of G on
M. When G and M are both profinite the twisted product of a continuous factor set is one
(TauCeti.ProfiniteGroupExtension.ofFactorSet); compactness of M alone would not do, the
twisted product being M × G as a space. The continuous cohomology classifying these bundled
extensions is the subject of TauCeti/Topology/Algebra/GroupExtension/Cohomology.lean.
Main definitions #
TauCeti.ProfiniteGroupExtension: an extension ofGbyMwith profinite total group, continuous inclusion and projection, inducing the given action, bundled with its total group, andTauCeti.ProfiniteGroupExtension.ofFactorSet, the twisted product of a continuous factor set whenGandMare profinite.TauCeti.GroupExtension.continuousMulEquivOfEquiv: an equivalence of extensions with compact total group is a homeomorphism as soon as it is continuous, hence aContinuousMulEquiv, andTauCeti.GroupExtension.continuousMulEquivOfMonoidHomis its form for a bare morphism. Neither assumes the group operations continuous, so neither is stated as an isomorphism of topological groups.TauCeti.GroupExtension.factorSetContinuousMulEquiv: the extension is the twisted product built from the factor set of a continuous normalized section, by a multiplicative equivalence that is a homeomorphism.
Main results #
TauCeti.GroupExtension.isClosed_ker_rightHom: a compact kernel is a closed subgroup of a Hausdorff extension.TauCeti.GroupExtension.exists_continuous_section: the projection of a profinite extension with compact kernel has a continuous normalized section.TauCeti.GroupExtension.continuous_factorSet: the factor set of a continuous normalized section is continuous whenever the inclusion of the kernel is an embedding, as a compact kernel of a Hausdorff extension is.TauCeti.GroupExtension.exists_continuous_factorSet: a profinite extension with compact kernel is the twisted product of a continuous factor set.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2.
- L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., Prop. 2.2.2 for the continuous section over an arbitrary closed subgroup, of which the compact-kernel case used here is a special case.
Continuous morphisms of extensions #
A continuous equivalence of extensions with compact total group is a homeomorphism, so it
is a multiplicative equivalence that is a homeomorphism. Only continuity in one direction has to be
checked: a continuous bijection from a compact space onto a Hausdorff space is a homeomorphism. No
compatibility between the group operations and the topologies is assumed, so the conclusion is a
ContinuousMulEquiv and not, on its own, an isomorphism of topological groups.
Equations
- TauCeti.GroupExtension.continuousMulEquivOfEquiv e he = { toMulEquiv := e.toMulEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Every continuous morphism between extensions with compact total group is a multiplicative
equivalence and a homeomorphism. Algebraically this is the five lemma,
GroupExtension.Equiv.ofMonoidHom; as in
TauCeti.GroupExtension.continuousMulEquivOfEquiv, nothing ties the group operations to the
topologies, so the conclusion is a ContinuousMulEquiv.
Equations
- TauCeti.GroupExtension.continuousMulEquivOfMonoidHom f hf comp_inl rightHom_comp = TauCeti.GroupExtension.continuousMulEquivOfEquiv (GroupExtension.Equiv.ofMonoidHom f comp_inl rightHom_comp) hf
Instances For
The continuous section and its factor set #
A compact kernel is a closed subgroup of a Hausdorff extension. It is the continuous image of a compact space in a Hausdorff space, so the finite kernels of the extension dictionary are covered without a separate argument.
The projection of a profinite extension with compact kernel has a continuous normalized set-theoretic section. The kernel is compact, hence closed, so the continuous section of a profinite group over the quotient by a closed subgroup applies; the base is identified with that quotient because the projection is a continuous bijection out of a compact space.
The factor set of a continuous normalized section is continuous as soon as the kernel
carries the subspace topology of its image: the factor set is continuous exactly because its image
under the inclusion, the failure σ g * σ h * (σ (g * h))⁻¹ of the section to be a homomorphism, is
continuous. In the profinite dictionary the hypothesis comes for free, the kernel being compact and
the extension Hausdorff: a continuous inclusion is then a closed embedding by
Continuous.isClosedEmbedding. Of E only the multiplication and the inversion are asked to be
continuous.
The comparison map ⟨a, g⟩ ↦ inl a * σ g out of the twisted product is continuous when the
section is. Only the multiplication of E has to be continuous: the map is a product of two
continuous maps, so nothing is asked of inversion.
The inverse of the comparison map is continuous when the projection and the section are
continuous and the kernel is embedded: it sends y to
⟨inl⁻¹ (y * (σ (rightHom y))⁻¹), rightHom y⟩, and the first coordinate is continuous because its
image under the embedding inl is. Together with
TauCeti.GroupExtension.continuous_factorSetToGroupExtensionEquiv this makes the comparison a
homeomorphism with no compactness assumption.
The difference of two continuous sections is continuous when the kernel carries the
subspace topology of its image: the image of the difference under the inclusion is
σ g * (σ' g)⁻¹.
A Hausdorff extension with compact kernel over a compact base is the twisted product built
from the factor set of a continuous normalized section: the comparison map of
TauCeti.GroupExtension.factorSetToGroupExtensionEquiv is a multiplicative equivalence and a
homeomorphism. Compactness is asked of the base rather than of the extension because it is the
twisted product, the source of the comparison map, that has to be compact; a compact extension with
continuous projection has compact base by Function.Surjective.compactSpace. As for the comparison
map itself, only the multiplication of E is asked to be continuous.
Equations
Instances For
A profinite extension with compact kernel is the twisted product of a continuous factor
set, by an equivalence of extensions that is continuous, hence a homeomorphism through
TauCeti.GroupExtension.continuousMulEquivOfEquiv. This is the direction of the extension
dictionary that reads a cocycle off an extension;
TauCeti.GroupExtension.factorSet_canonicalSection is the other one.
Bundled profinite extensions #
An extension of G by M with profinite total group inducing the given action: a
profinite group E together with an extension 1 → M → E → G → 1 of abstract groups whose
inclusion and projection are continuous and whose conjugation action on M is the given one.
Only the total group is required to be profinite; G and M carry just their topologies and the
action. The classification in TauCeti/Topology/Algebra/GroupExtension/Cohomology.lean adds what
it needs: for the class and the equivalence criterion, G Hausdorff with continuous multiplication
acting continuously on a compact M; for realizing every class, G and M both profinite. The
total group is taken in the universe of M × G, where the twisted products of the factor sets
live; under those hypotheses every such extension is, up to continuous equivalence, one of those
(TauCeti.ProfiniteGroupExtension.ofFactorSet), and the classification
TauCeti.ProfiniteGroupExtension.contCohomologyClassEquiv is stated at this universe for that
reason.
- E : Type (max u v)
The total group of the extension.
- instTopologicalSpace : TopologicalSpace self.E
- instIsTopologicalGroup : IsTopologicalGroup self.E
- instCompactSpace : CompactSpace self.E
- instTotallyDisconnectedSpace : TotallyDisconnectedSpace self.E
- toGroupExtension : GroupExtension M self.E G
The extension
1 → M → E → G → 1of abstract groups. - continuous_inl : Continuous ⇑self.toGroupExtension.inl
- continuous_rightHom : Continuous ⇑self.toGroupExtension.rightHom
- inducesAction : GroupExtension.InducesAction self.toGroupExtension
Instances For
The twisted product of a continuous factor set is a profinite extension when G and M
are profinite: it is M × G as a space, TauCeti.FactorSet.Extension.isTopologicalGroup makes
it a topological group, and its inclusion and projection are the coordinate maps. Compactness of
M alone would not do: the twisted product of the trivial factor set over the trivial group is M
itself. The realization is an abbreviation so that its total group and group structure remain
definitionally those of α.Extension; the underlying extension is given by
TauCeti.ProfiniteGroupExtension.ofFactorSet_toGroupExtension.
Equations
- One or more equations did not get rendered due to their size.