Morphisms of finite normal layers between formations #
Let F be a formation on G and F' a formation on G', with finite normal layers V ◁ U of
G and V' ◁ U' of G'. A layer morphism LayerHom F L F' L' is an isomorphism of Galois
groups e : U/V ≃* U'/V' together with a homomorphism of coefficient modules
φ : A^V → A'^{V'}, not necessarily bijective, that intertwines the two Galois actions along e.
The motivating example is a place w of a finite Galois extension L/K of number fields, with
decomposition group D_w. Restriction identifies the Galois group of the local extension
L_w/K_v with D_w, the Galois group of the global extension L/L^{D_w}, and the inclusion of
L_wˣ into the idele classes C_L, as the component at w, is equivariant along it; it is not an
isomorphism. The map that an equivariant map of coefficient modules induces on a single layer is
another example (NormalLayer.repMapLayerHom), and so is every layer isomorphism
(LayerEquiv.toLayerHom).
A layer morphism acts on what a layer carries: on ordinary and Tate cohomology in the coefficient
module (LayerHom.cohomologyMap, LayerHom.tateCohomologyMap), on Tate cohomology with trivial
integral coefficients, where it is an isomorphism (LayerHom.trivialTateCohomologyIso), on the
ground level (LayerHom.groundMap) and on the norm quotient (LayerHom.normQuotientMap). These
actions commute with the norm, with cup product, and with the low-degree identifications of Tate
cohomology.
If F and F' carry class formations and the morphism carries the fundamental class of L to the
fundamental class of L', which holds as soon as it matches the invariant maps
(ClassFormation.fundamentalClass_layerHom), then it carries Tate's isomorphism, the Nakayama map,
Artin reciprocity and the Artin map of L to those of L' (ClassFormation.tateIso_layerHom,
ClassFormation.nakayamaNegTwo_layerHom, ClassFormation.artinEquiv_layerHom,
ClassFormation.artinMap_layerHom): the Artin symbol in L' of the image of a is the image of
the Artin symbol of a. This is the functoriality of the reciprocity map along a morphism of class
formations that preserves invariants. For a place of a number field it reduces the compatibility of
the global Artin map with the local one to the compatibility of the global invariant with the local
invariant.
Main definitions #
TauCeti.ClassFieldTheory.LayerHom: a morphism from a layer of one formation to a layer of another.TauCeti.ClassFieldTheory.LayerHom.cohomologyMap,TauCeti.ClassFieldTheory.LayerHom.tateCohomologyMap: the induced maps of ordinary and of Tate cohomology.TauCeti.ClassFieldTheory.LayerHom.trivialTateCohomologyIso: the induced isomorphism of Tate cohomology with trivial integral coefficients.TauCeti.ClassFieldTheory.LayerHom.groundMap,TauCeti.ClassFieldTheory.LayerHom.normQuotientMap: the induced maps of ground levels and of norm quotients.TauCeti.ClassFieldTheory.NormalLayer.repMapLayerHom: the layer morphism induced on one layer by an equivariant map of coefficient modules.
Main statements #
TauCeti.ClassFieldTheory.LayerHom.norm_coeffMap: a layer morphism commutes with the norms.TauCeti.ClassFieldTheory.cupClass_layerHom: cup product with a degree-two class is carried along a layer morphism.TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_layerHom: a layer morphism matching the invariant maps matches the fundamental classes.TauCeti.ClassFieldTheory.ClassFormation.artinMap_layerHom: a layer morphism matching the fundamental classes carries the Artin symbol ofato the Artin symbol of the image ofa.
References #
- E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§4–6.
- J.-P. Serre, Local Fields, Chapter XI, §3.
- J. Tate, Global class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII, §11.
A morphism from the layer L of the formation F to the layer L' of the formation F':
an isomorphism of Galois groups and a homomorphism of coefficient modules that intertwines the
Galois actions along it.
The isomorphism
U/V ≃* U'/V'of Galois groups.The homomorphism
A^V → A'^{V'}of coefficient modules.- isIntertwiningMap : (L.rep F).ρ.IsIntertwiningMap (MonoidHom.comp (L'.rep F').ρ ↑self.galEquiv) self.coeffMap
The coefficient homomorphism intertwines the Galois actions along
galEquiv.
Instances For
The coefficient homomorphism of a layer morphism intertwines the Galois actions.
The two layers of a layer morphism have the same degree.
Cohomology #
The map H^n(U/V, A^V) ⟶ H^n(U'/V', A'^{V'}) of ordinary cohomology induced by a layer
morphism: Mathlib's change-of-group map along the inverse of the isomorphism of Galois groups.
Instances For
The map of ordinary cohomology induced by a layer morphism is Mathlib's groupCohomology.map
of the compatible pair.
The image of the class of a cocycle c under the map of second cohomology induced by a layer
morphism E is the class of the cocycle
(γ, δ) ↦ E.coeffMap (c (E.galEquiv.symm γ, E.galEquiv.symm δ)).
The map H^r(U/V, A^V) ⟶ H^r(U'/V', A'^{V'}) of Tate cohomology induced by a layer morphism,
in every integer degree: the Tate map of its compatible pair.
Instances For
The map of Tate cohomology induced by a layer morphism is the Tate map of its compatible pair.
In positive degrees the Tate and ordinary maps agree, through the identifications
tateHIsoH of the two layers.
The isomorphism H^r(U/V, ℤ) ≅ H^r(U'/V', ℤ) of Tate cohomology with trivial integral
coefficients induced by the isomorphism of Galois groups of a layer morphism.
Instances For
The isomorphism of Tate cohomology with trivial coefficients is the Tate map of the pair formed
by the isomorphism of Galois groups and the identity of ℤ.
In degree -2 the map is the induced isomorphism of abelianized Galois groups, under the
identifications H^{-2}(U/V, ℤ) ≃ (U/V)^ab of the two layers.
The ground level and the norm #
The map A^U → A'^{U'} of ground levels induced by a layer morphism: an element of the ground
level is an invariant of the coefficient module, and its image is the image of that invariant
(groundMap_apply_coe).
Instances For
The map of ground levels is the coefficient homomorphism, applied to the ground level as a submodule of the top level.
On the invariant attached to a ground-level element, the map of ground levels is the induced map of invariants.
A layer morphism commutes with the norms N_{U/V} and N_{U'/V'}.
A layer morphism carries the norm subgroup of L into the norm subgroup of L'.
The map A^U / N_{U/V}(A^V) → A'^{U'} / N_{U'/V'}(A'^{V'}) of norm quotients induced by a
layer morphism.
Instances For
The map of norm quotients sends the class of a to the class of its image.
In degree zero the Tate map is the map of norm quotients, through the identifications
tateHZeroEquivNormQuotient of the two layers.
The character class #
The character class a₀ ∪ δχ is carried along a layer morphism: the image of the class
attached to a and to the character χ ∘ e^ab of U/V is the class attached to the image of a
and to χ.
Cup product with a degree-two class is carried along a layer morphism: the image of
x ∪ u is the cup product of the images of x and of u, in every degree.
Equivariant maps of coefficient modules #
The layer morphism induced on the layer L by an equivariant map φ : A → A' of the
coefficient modules of two formations on G: the identity of the Galois group of L and the map
A^V → A'^V of top levels (NormalLayer.repMap).
Instances For
The Galois-group isomorphism of NormalLayer.repMapLayerHom is the identity.
The coefficient homomorphism of NormalLayer.repMapLayerHom is NormalLayer.repMap.
The layer morphism induced by an equivariant map acts on ordinary cohomology as
groupCohomology.functor applied to NormalLayer.repMap.
Class formations #
A layer morphism matching the invariant maps matches the fundamental classes.
Tate's isomorphism is carried along a layer morphism matching the fundamental classes: the
image of x ∪ u_{U/V} is the cup product of the image of x with u_{U'/V'}.
The Nakayama map is carried along a layer morphism matching the fundamental classes.
Artin reciprocity is carried along a layer morphism matching the fundamental classes.
The Artin map is carried along a layer morphism matching the fundamental classes: the Artin
symbol in L' of the image of a is the image under (U/V)^ab ≃ (U'/V')^ab of the Artin symbol
of a in L.