Finite-quotient comparison in degrees zero, one and two #
For a profinite group G acting continuously on a discrete module M, the explicit continuous
cohomology groups in degrees zero, one and two are colimits of the finite-level groups over the open
normal subgroups:
Hⁱ(G, M) = colim_U Hⁱ(G ⧸ U, M^U), i = 0, 1, 2.
This file names the comparison maps into Hⁱ(G, M) for i = 0, 1, 2 and assembles them into
cocones on the systems TauCeti.ContCohomology.explicitFiniteQuotientSystem0,
explicitFiniteQuotientSystem1 and explicitFiniteQuotientSystem2. It proves that all three
cocones are colimiting; those statements are universality of the named maps, not bare
isomorphisms.
Main definitions #
TauCeti.ContCohomology.explicitFiniteQuotientComparison0andexplicitFiniteQuotientCocone0: degree-zero inflation assembled as a cocone.TauCeti.ContCohomology.explicitFiniteQuotientColimit0: that cocone is colimiting.TauCeti.ContCohomology.explicitFiniteQuotientComparison1: the leg family, inflation alongG → G ⧸ U.TauCeti.ContCohomology.explicitFiniteQuotientCocone1: the cocone those legs form, with apexH¹(G, M).TauCeti.ContCohomology.explicitFiniteQuotientColimit1: that cocone is colimiting.TauCeti.ContCohomology.explicitFiniteQuotientComparison2: the degree-two leg family, again given by inflation.TauCeti.ContCohomology.explicitFiniteQuotientCocone2: the degree-two comparison cocone with apexH²(G, M).TauCeti.ContCohomology.explicitFiniteQuotientColimit2: that cocone is colimiting.
Main statements #
TauCeti.ContCohomology.explicitInfl0_comp_explicitFiniteQuotientTransition0: degree-zero inflation is compatible with the finite-level transitions.TauCeti.ContCohomology.explicitFiniteQuotientTransition0_bijective: every degree-zero transition is bijective.TauCeti.ContCohomology.explicitInfl1_comp_explicitFiniteQuotientTransition1and its elementwise formexplicitInfl1_explicitFiniteQuotientTransition1: inflating through a deeper level is inflating directly, which is the cocone condition.TauCeti.ContCohomology.exists_openNormalSubgroup_apply_eq_zero: a continuous1-cocycle of a profinite group with discrete coefficients vanishes on an open normal subgroup.TauCeti.ContCohomology.exists_explicitInfl1_eq: every class inH¹(G, M)is inflated from a finite level.TauCeti.ContCohomology.subsingleton_H1_of_forall_openNormalSubgroup: if every finite layer has trivial first cohomology, so doesH¹(G, M).TauCeti.ContCohomology.explicitInfl2_comp_explicitFiniteQuotientTransition2: degree-two inflation is compatible with the finite-level transitions.TauCeti.ContCohomology.exists_explicitFiniteQuotientTransition2_eq_zero: a finite-level class which inflates to zero vanishes after transition to a sufficiently deep finite level.
Implementation notes #
The comparison map from the U-level is inflation along G → G ⧸ U, already built as
TauCeti.ContCohomology.explicitInfl0, explicitInfl1 or explicitInfl2; they are used under
those names, and the comparison natural transformations assemble the maps rather than introducing
second names for individual legs.
In degree zero every comparison leg is an additive equivalence: being fixed by the quotient on
M^U is exactly being fixed by G on M. Every transition is therefore bijective, so the
degree-zero system is eventually constant in the sense of
CategoryTheory.Functor.IsEventuallyConstantFrom and the colimit statement is Mathlib's
CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitOfIsIso applied at the whole-group
level. Consequently the degree-zero cocone is already colimiting for any topological group; no
compactness or discreteness hypothesis enters that proof.
Surjectivity of the comparison is strict. The zero set of a continuous 1-cocycle is an open
neighbourhood of 1, so ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one puts an open
normal subgroup U inside it, and the cocycle is then the inflation of its descent to G ⧸ U
(TauCeti.ContCohomology.explicitInfl1_descendZ1): no coboundary is subtracted. Injectivity of
each comparison map is TauCeti.ContCohomology.explicitInfl1_injective, which holds for an
arbitrary normal subgroup and needs neither compactness nor discreteness, so the colimit is a
directed union and the descent of an arbitrary cocone is defined by choosing any level a class
comes from.
In the degree-one argument, compactness and total disconnectedness of G are used only to put an
open normal subgroup inside the open zero set supplied by discreteness of M.
In degree two, strict descent supplies surjectivity. For injectivity, a continuous primitive of an inflated coboundary is uniformly constant on right cosets of some open normal subgroup and has finite image. Passing to a still smaller subgroup which fixes that image descends the primitive, so the original finite-level class becomes a coboundary at that deeper level.
The degree-two colimit statement is then read off from
TauCeti.AddCommGrpCat.isColimitOfJointlySurjective: the comparison legs are jointly surjective,
and two finite-level classes with the same inflation already agree after transition to a common
deeper level.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.2.5).
- L. Ribes and P. Zalesskii, Profinite Groups, Cor. 6.5.6(a).
Inflating from the U-level through the V-level, for V ≤ U, is the same as inflating
from the U-level directly.
Inflating a degree-zero class through a deeper finite level does not change it.
The degree-zero comparison maps into H⁰(G, M), assembled from inflation at every open
normal subgroup.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The degree-zero comparison map at U is inflation along G → G ⧸ U.
The degree-zero finite-quotient cocone, whose point is H⁰(G, M).
Equations
Instances For
The apex of the degree-zero finite-quotient cocone is H⁰(G, M).
The legs of the degree-zero finite-quotient cocone are the comparison maps.
Every degree-zero finite-quotient transition is bijective: inflation is an equivalence at both levels, and inflating through the deeper level is inflating directly.
The degree-zero finite-quotient colimit theorem: H⁰(G, M) is the colimit of
H⁰(G ⧸ U, M^U) over the open normal subgroups, through the inflation maps.
Every transition is an isomorphism, so the system is eventually constant and the whole-group
level — where the comparison leg is the equivalence
TauCeti.ContCohomology.explicitInfl0Equiv — already computes the colimit.
Equations
Instances For
Inflating from the U-level through the V-level, for V ≤ U, is inflating from the
U-level directly. This is the cocone condition for
TauCeti.ContCohomology.explicitFiniteQuotientCocone1.
Inflating a class from a level to a deeper one does not change it: the elementwise form of
TauCeti.ContCohomology.explicitInfl1_comp_explicitFiniteQuotientTransition1.
The degree-one comparison maps into H¹(G, M): inflation along G → G ⧸ U, assembled into
the leg family of a cocone. They are named because the colimit theorem below says that these
maps are universal, not that some isomorphism exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The degree-one comparison map at U is inflation along G → G ⧸ U.
The degree-one finite-quotient cocone, whose point is H¹(G, M) itself.
Equations
Instances For
The apex of the degree-one finite-quotient cocone is H¹(G, M).
The legs of the degree-one finite-quotient cocone are the comparison maps.
Degree two #
Inflating from the U-level through the V-level, for V ≤ U, is inflating from the
U-level directly in degree two. This is the cocone condition for
TauCeti.ContCohomology.explicitFiniteQuotientCocone2.
Inflating a degree-two class from a level to a deeper one does not change it: the elementwise
form of TauCeti.ContCohomology.explicitInfl2_comp_explicitFiniteQuotientTransition2.
The degree-two comparison maps into H²(G, M): inflation along G → G ⧸ U, assembled into
the leg family of a cocone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The degree-two comparison map at U is inflation along G → G ⧸ U.
The degree-two finite-quotient cocone, whose point is H²(G, M) itself.
Equations
Instances For
The apex of the degree-two finite-quotient cocone is H²(G, M).
The legs of the degree-two finite-quotient cocone are the comparison maps.
A continuous 1-cocycle of a profinite group with discrete coefficients vanishes on an open
normal subgroup: its zero set is open and contains 1.
Strict surjectivity of the comparison maps: every class in H¹(G, M) is inflated from a
finite level. The representing cocycle itself vanishes on an open normal subgroup U, so it is
the inflation of its descent to G ⧸ U and no coboundary is subtracted.
The degree-one finite-quotient colimit theorem: H¹(G, M) is the colimit of the
finite-level first cohomology groups H¹(G ⧸ U, M^U), through the inflation maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Vanishing descends from the finite levels: if every finite layer has trivial first
cohomology, so does H¹(G, M). Every class comes from a finite level, and two classes are
compared at the intersection of their levels. This is the form in which Hilbert 90 and the Kummer
isomorphism pass from finite Galois layers to the absolute Galois group.
Degree two #
A degree-two class at a finite quotient which inflates to zero becomes zero after transition to a sufficiently deep finite quotient. This is the injectivity half of the degree-two finite-quotient colimit theorem.
The degree-two finite-quotient colimit theorem: H²(G, M) is the colimit of the
finite-level second cohomology groups H²(G ⧸ U, M^U), through the inflation maps.