The canonical continuous-cohomology system over the open normal subgroups #
Let G be a topological group acting on a discrete module M. For every open normal
subgroup U, the fixed points M^U are a discrete module over G ⧸ U, and hence have canonical
continuous cohomology in every degree. If V ≤ U, compatible-pair functoriality along
G ⧸ V → G ⧸ U and M^U → M^V gives a transition map
Hⁿ(G ⧸ U, M^U) ⟶ Hⁿ(G ⧸ V, M^V).
This file assembles those maps into a functor on (OpenNormalSubgroup G)ᵒᵖ and constructs the
canonical cocone whose legs are inflation followed by inclusion of fixed points. The assertion that
this cocone is colimiting, TauCeti.ContCohomology.continuousFiniteQuotientColimit in
FiniteQuotient.AllDegreeColimit, needs compactness of G, continuity of the action and the
all-degree descent argument; it is deliberately separate from the construction here, which needs
neither.
Nothing below assumes that the quotients G ⧸ U are finite, and none of them need be: for an open
normal subgroup U the quotient G ⧸ U is discrete, so it is finite when G is compact, but
without compactness it may be finite or infinite.
The declarations nevertheless carry finiteQuotient in their names, after the tower of quotients
they are indexed by and in step with the explicit low-degree systems of FiniteQuotient.Explicit,
which are built under these same hypotheses.
The construction is the canonical, all-degree counterpart of the explicit systems in degrees zero,
one and two in FiniteQuotient.Explicit. It follows the finite-quotient system of Neukirch–Schmidt–
Wingberg, Cohomology of Number Fields, (1.2.5), and Ribes–Zalesskii, Profinite Groups,
Corollary 6.5.6(a).
Main definitions #
TauCeti.ContCohomology.continuousFiniteQuotientTransition: the canonical transition map in every degree.TauCeti.ContCohomology.continuousFiniteQuotientSystem: the resulting system on(OpenNormalSubgroup G)ᵒᵖ.TauCeti.ContCohomology.continuousFiniteQuotientComparison: the inflation-and-inclusion legs.TauCeti.ContCohomology.continuousFiniteQuotientCocone: those legs as a cocone with apexHⁿ(G, M).
Main statements #
TauCeti.ContCohomology.continuousFiniteQuotientTransition_eq_mapandTauCeti.ContCohomology.continuousFiniteQuotientComparisonApp_eq_map: the characteristic equations of the two maps, identifying each with the compatible-pair pullbackContinuousCohomology.mapit is built from, so that no consumer unfolds either body.TauCeti.ContCohomology.continuousFiniteQuotientTransition_reflandcontinuousFiniteQuotientTransition_comp: the two functor laws.TauCeti.ContCohomology.continuousFiniteQuotientTransition_comp_comparisonApp: comparison through a deeper quotient agrees with direct comparison, which is the cocone condition.
Implementation notes #
The comparison legs are defined as the existing all-degree inflation map
TauCeti.ContinuousCohomology.infl after the coefficient dictionary
TauCeti.ofDiscreteModuleQuotient, rather than rebuilt from a compatible pair;
TauCeti.ContCohomology.coeffMap_ofDiscreteModuleQuotient_comp_infl supplies the compatible-pair
presentation, which is what continuousFiniteQuotientComparisonApp_eq_map records.
Every definition keeps its body sealed and is characterized by lemmas. As for
explicitFiniteQuotientSystem0_map in FiniteQuotient.Explicit, the characteristic lemmas of the
system's arrows, the comparison legs and the cocone legs are stated across the eqToHom
transports given by the object and point equations, since with the bodies sealed a morphism out
of F.obj U (or into c.pt) does not have the type of the map it is built from.
The coefficient morphism in the canonical transition from the U-level to the V-level, for
V ≤ U. Its underlying map is the inclusion M^U → M^V.
Instances For
The coefficient pair acts as the inclusion M^U → M^V on underlying elements.
The coefficient pair is the dictionary image of the inclusion of fixed points.
The canonical continuous-cohomology transition
Hⁿ(G ⧸ U, M^U) ⟶ Hⁿ(G ⧸ V, M^V) for V ≤ U.
Instances For
The characteristic equation of the canonical transition: it is the compatible-pair pullback
along the quotient homomorphism G ⧸ V → G ⧸ U and the inclusion M^U → M^V.
The canonical transition from a level to itself is the identity.
For W ≤ V ≤ U, the canonical transition from the U-level to the W-level is the
composite through the V-level.
For W ≤ V ≤ U, the canonical transition from the U-level to the W-level is the
composite through the V-level.
The canonical system over the open normal subgroups of G in degree n. It sends U to
Hⁿ(G ⧸ U, M^U) and an inclusion V ≤ U to compatible-pair pullback from the U-level to
the V-level.
Instances For
The object at U of the canonical system is Hⁿ(G ⧸ U, M^U).
Under the object identifications above, every arrow of the canonical system is the compatible-pair transition.
The comparison map from the U-level into Hⁿ(G, M): the coefficient dictionary
TauCeti.ofDiscreteModuleQuotient, which reads M^U as the canonical U-invariants of M,
followed by canonical inflation along G → G ⧸ U.
Instances For
The characteristic equation of the comparison map: in every degree it is the
compatible-pair pullback along the quotient homomorphism G → G ⧸ U and the inclusion
M^U → M.
Passing from the U-level through a deeper V-level and then comparing with Hⁿ(G, M)
is the direct comparison from the U-level.
Passing from the U-level through a deeper V-level and then comparing with Hⁿ(G, M)
is the direct comparison from the U-level.
The inflation-and-inclusion comparison maps from every level into Hⁿ(G, M), assembled as a
natural transformation to the constant functor.
Instances For
Under the object identification at U, the comparison natural transformation at U is
canonical inflation and inclusion from the U-level.
The canonical cocone over the open-normal-subgroup system in degree n, with point Hⁿ(G, M)
and legs the inflation-and-inclusion comparisons.
Instances For
The point of the canonical cocone is Hⁿ(G, M).
Under the object and point identifications, the leg of the canonical cocone at U is canonical
inflation and inclusion from the U-level.