Inflation from a finite normal layer to its ground subgroup #
Let F be a formation on a profinite group G whose coefficient module is read, through an
equivariant additive equivalence e : M ≃+ A, on a discrete G-module M, as for the formation
of units of a field K, whose coefficients are read on (Kˢ)ˣ, or the idele formation of a number
field K, whose coefficients are read on the ideles of Kˢ. For a finite normal layer V ◁ U of
open subgroups of G, this file constructs inflation from the second cohomology of the layer
to the continuous second cohomology of its ground subgroup,
NormalLayer.explicitInfl2 L e he : H²(U ⧸ V, M^V) → H²(U, M),
in the explicit inhomogeneous model of TauCeti.ContCohomology. On the class of a layer cocycle
c it is the class of the inflated cocycle (u, v) ↦ c (u V, v V) (explicitInfl2_H2π,
inflCocycle2_apply). It is compatible with the operations on layers: restriction to an
intermediate ground subgroup (explicitInfl2_cohomologyRes), refinement to a smaller top subgroup
(explicitInfl2_cohomologyInfl), conjugation by an element g of G, which it carries to the
conjugation H²(U, M) → H²(gUg⁻¹, M) (explicitInfl2_conjugateCohomologyIso), and every map of
layer cohomologies that pulls inflated cocycles back along a compatible pair
(explicitInfl2_eq_explicitMap2_explicitInfl2), in particular every map of coefficient modules
(explicitInfl2_map_repMap). Restriction to the
top subgroup kills inflated classes (explicitMap2_explicitInfl2_eq_zero), inflation is injective
when H¹(V, M) vanishes (explicitInfl2_injective_of_subsingleton), and every class of
H²(U, M) is inflated from a refinement of a given layer over U (exists_explicitInfl2_eq).
Inflation carries the cohomology of the finite layers into continuous cohomology, where the
local invariants and the local–global maps of a number field (localization at the places,
corestriction from the ground subgroup U to G) are defined.
Main definitions #
TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2 L e he: inflationH²(U ⧸ V, M^V) → H²(U, M).TauCeti.ClassFieldTheory.NormalLayer.inflCocycle2 L e he c: the continuous2-cocycle onUinflated from a layer cocyclec.
Main results #
TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_H2π: inflation sends the class of a layer cocycle to the class of its inflated cocycle.TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_artinCharacterCup: inflation sends the classa ∪ δχof the character formula to the carry class ofχanda.TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_injective_of_subsingleton: inflation is injective whenH¹(V, M)vanishes.TauCeti.ClassFieldTheory.NormalLayer.explicitMap2_explicitInfl2_eq_zero: restriction to the top subgroup kills inflated classes.TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_cohomologyRes,TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_cohomologyInfl: inflation commutes with the restriction and the refinement of layers.TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_conjugateCohomologyIso: inflation commutes with the conjugation of layers.TauCeti.ClassFieldTheory.NormalLayer.exists_explicitInfl2_eq: every class ofH²(U, M)is inflated from a refinement of a given layer overU.TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_eq_explicitMap2_explicitInfl2: inflation is natural along maps of layer cohomology that pull back inflated cocycles along a compatible pair.TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2_map_repMap: inflation is natural in the coefficient module.
Implementation notes #
The continuous cohomology of the ground subgroup is that of its underlying subgroup
L.ground.toSubgroup of G, and the Galois group of the layer is read as the quotient of that
subgroup by L.top.toSubgroup.subgroupOf L.ground.toSubgroup; this quotient is definitionally the
Galois group L.Gal = L.ground ⧸ L.relativeTop of the layer, which is why MulEquiv.refl can
identify the two in the private h2EquivExplicit. The coefficient module A^V of the layer is read
as the fixed points M^V through TauCeti.ClassFieldTheory.NormalLayer.coeffFixedPointsEquiv.
The construction follows that of TauCeti.ClassFieldTheory.layerBrLevelEquiv and
TauCeti.ClassFieldTheory.brInfl in TauCeti.NumberTheory.ClassFieldTheory.Brauer.Formation,
which inflate from a layer V ◁ G_K of the formation of units, whose ground is the whole absolute
Galois group, into Br K = H²(G_K, (Kˢ)ˣ). This file extends it to layers with an arbitrary open
ground subgroup and to an arbitrary coefficient dictionary e; the local invariant of a layer in
TauCeti.NumberTheory.ClassFieldTheory.Brauer.LayerInvariant uses it for the formation of units.
References #
- E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1.
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.1) and (1.6.7).
Inflation from a layer to its ground subgroup: for a finite normal layer V ◁ U of a
formation whose coefficient module is read on the discrete module M through e, the map
H²(U ⧸ V, M^V) → H²(U, M) into the continuous cohomology of U. On the class of a cocycle c
it is the class of inflCocycle2 L e he c (explicitInfl2_H2π).
Instances For
The inflated cocycle of a 2-cocycle c of a layer: the continuous 2-cocycle
(u, v) ↦ c (u V, v V) on the ground subgroup U, with values in M (inflCocycle2_apply).
Its class is explicitInfl2 L e he [c] (explicitInfl2_H2π).
Instances For
The values of the inflated cocycle are the values of the layer cocycle at the classes of the
two arguments, read in M.
Inflation on cocycle classes: explicitInfl2 L e he sends the class of a layer cocycle c
to the class of the inflated cocycle inflCocycle2 L e he c.
The inflated Artin character cup is the carry class. For an element a' of the ground
level A^U of a layer and a character χ' of its abelianized Galois group, read on U as ψ, the
inflation to U of the class a' ∪ δχ' of the character formula is the class of the carry cocycle
of ψ and of a', read as an invariant a of U in M.
Inflation from a layer is injective when H¹(V, M) vanishes: the transgression into
H²(U ⧸ V, M^V) then vanishes. For the formation of units this is Hilbert 90 for V.
Restriction to the top subgroup kills inflated classes: restricting
L.explicitInfl2 e he x from the ground subgroup U to the top subgroup V gives 0.
Inflation commutes with restriction of layers: for a restriction V ◁ U' ≤ U of a layer
V ◁ U to an intermediate ground subgroup, inflating the restricted class to U' is restricting
the inflated class from U to U'.
Inflation commutes with refinement of layers: for a refinement of V ◁ U to V' ◁ U, the
class inflated from V' ◁ U of the refined class is the class inflated from V ◁ U, read along
the identification of the two ground subgroups.
Every class of H²(U, M) is inflated from a refinement of a given layer over U.
For a layer V ◁ U and a class c in the continuous cohomology of its ground subgroup, there is a
layer V' ◁ U with V' ≤ V from whose H² the class c is inflated. The class c is read on the
ground subgroup of the refinement, which is U again.
Inflation is natural along maps that pull back inflated cocycles: let V ◁ U be a layer
of F and V' ◁ U' a layer of a formation F' on G' read on M' through e', and let
(f, φ) be a compatible pair from (U, M) to (U', M'). If a map Ψ of layer cohomologies
sends the class of each layer cocycle c to the class of a layer cocycle whose inflated cocycle is
the inflated cocycle of c pulled back along (f, φ), then inflating Ψ x to U' is pulling back
the inflation of x.
Inflation is natural in the coefficient module: let φ : A → A' be a map of the
coefficient modules of two formations on G, read on the discrete modules M and M' as the
equivariant map f. Inflating to U the image under φ of a class of H²(U ⧸ V, A^V) is
applying f to the inflation of the class.
Inflation and conjugation #
Inflation commutes with conjugation: inflating the conjugate of a class to the ground
subgroup gUg⁻¹ of the conjugate layer is conjugating the inflated class from U to gUg⁻¹, that
is, pulling it back along inverse conjugation and acting by g on the coefficients.