Isomorphisms 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 isomorphism LayerEquiv F L F' L' is an isomorphism of
Galois groups e : U/V ≃* U'/V' together with an isomorphism of coefficient modules
φ : A^V ≃ A'^{V'} that intertwines the two Galois actions along e. This is purely
group- and module-theoretic data, not a field isomorphism; in field notation, an isomorphism of a
Galois extension K/E with a Galois extension K'/E' (living in a different separable closure,
or over a different base field) induces a layer isomorphism once the coefficient modules attached
to the two extensions are identified compatibly. The motivating example is a finite extension
L/K of local fields, whose absolute Galois group G_L is an open subgroup of G_K, so that each
finite Galois extension of L is a layer both of the formation of L and of that of K.
Conjugation of a layer by an element of G is another example
(NormalLayer.conjugateLayerEquiv).
A layer isomorphism is in particular a layer morphism (LayerEquiv.toLayerHom), so everything a
layer morphism acts on is transported by it, and here the transports are isomorphisms: ordinary
and Tate cohomology in the coefficient module (LayerEquiv.cohomologyIso,
LayerEquiv.tateCohomologyIso), the ground level (LayerEquiv.groundEquiv) and the norm quotient
(LayerEquiv.normQuotientEquiv). Tate cohomology with trivial integral coefficients is
transported by the isomorphism LayerHom.trivialTateCohomologyIso of the underlying morphism. The
transports are compatible with the norm, with cup product, and with the low-degree
identifications of Tate cohomology.
If F and F' carry class formations whose invariant maps correspond under the isomorphism of
H², then the isomorphism carries the fundamental class to the fundamental class
(ClassFormation.fundamentalClass_layerEquiv), so Tate's isomorphism, the Nakayama map, Artin
reciprocity and the Artin map are all transported by the statements for the underlying layer
morphism (ClassFormation.tateIso_layerHom, ClassFormation.nakayamaNegTwo_layerHom,
ClassFormation.artinEquiv_layerHom, ClassFormation.artinMap_layerHom). The last is restated for
layer isomorphisms as ClassFormation.artinMap_layerEquiv. This is how the Artin map of one class
formation is read as an Artin map of another: for a finite extension of local fields it identifies
the local Artin map of the extension with an abstract Artin map of the formation of the base, once
the two invariant maps are compared.
Main definitions #
TauCeti.ClassFieldTheory.LayerEquiv: an isomorphism between a layer of one formation and a layer of another.TauCeti.ClassFieldTheory.LayerEquiv.toLayerHom: the layer morphism underlying a layer isomorphism.TauCeti.ClassFieldTheory.LayerEquiv.cohomologyIso,TauCeti.ClassFieldTheory.LayerEquiv.tateCohomologyIso: the induced isomorphisms of ordinary and of Tate cohomology.TauCeti.ClassFieldTheory.LayerEquiv.groundEquiv,TauCeti.ClassFieldTheory.LayerEquiv.normQuotientEquiv: the induced isomorphisms of ground levels and of norm quotients.TauCeti.ClassFieldTheory.NormalLayer.conjugateLayerEquiv: conjugation bygas a layer isomorphism.
Main statements #
TauCeti.ClassFieldTheory.LayerEquiv.norm_coeffEquiv: the isomorphism commutes with the norms.TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_layerEquiv: an isomorphism matching the invariant maps matches the fundamental classes.TauCeti.ClassFieldTheory.ClassFormation.artinMap_layerEquiv: it then 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.
An isomorphism from the layer L of the formation F to the layer L' of the formation
F': an isomorphism of Galois groups and an isomorphism of coefficient modules that intertwines
the Galois actions along it.
The isomorphism
U/V ≃* U'/V'of Galois groups.The isomorphism
A^V ≃ A'^{V'}of coefficient modules.- isIntertwiningMap : (L.rep F).ρ.IsIntertwiningMap (MonoidHom.comp (L'.rep F').ρ ↑self.galEquiv) ↑self.coeffEquiv
The coefficient isomorphism intertwines the Galois actions along
galEquiv.
Instances For
The coefficient isomorphism of a layer isomorphism intertwines the Galois actions.
The layer morphism underlying a layer isomorphism: the same isomorphism of Galois groups, with the coefficient isomorphism regarded as a homomorphism.
Instances For
The Galois-group isomorphism of the underlying layer morphism is that of the isomorphism.
The coefficient homomorphism of the underlying layer morphism is the coefficient isomorphism.
Cohomology #
The isomorphism H^n(U/V, A^V) ≅ H^n(U'/V', A'^{V'}) of ordinary cohomology induced by a layer
isomorphism.
Instances For
The isomorphism of ordinary cohomology induced by a layer isomorphism is Mathlib's
groupCohomology.mapIso.
The isomorphism of ordinary cohomology induced by a layer isomorphism is the map induced by its underlying layer morphism.
The image of the class of a cocycle c under the isomorphism of second cohomology induced by a
layer isomorphism E is the class of the cocycle
(γ, δ) ↦ E.coeffEquiv (c (E.galEquiv.symm γ, E.galEquiv.symm δ)).
The isomorphism H^r(U/V, A^V) ≅ H^r(U'/V', A'^{V'}) of Tate cohomology induced by a layer
isomorphism, in every integer degree.
Instances For
The isomorphism of Tate cohomology induced by a layer isomorphism is the map induced by its underlying layer morphism.
The ground level and the norm #
The isomorphism A^U ≃ A'^{U'} of ground levels induced by a layer isomorphism: an element of
the ground level is an invariant of the coefficient module, and its image is the image of that
invariant (groundEquiv_apply_coe).
Instances For
The isomorphism of ground levels is the coefficient isomorphism, applied to the ground level as a submodule of the top level.
The inverse isomorphism of ground levels is the inverse coefficient isomorphism, applied to the ground level as a submodule of the top level.
On ground levels, the underlying layer morphism acts as the isomorphism of ground levels.
A layer isomorphism commutes with the norms N_{U/V} and N_{U'/V'}.
A layer isomorphism carries the norm subgroup of L onto the norm subgroup of L'.
The isomorphism A^U / N_{U/V}(A^V) ≃ A'^{U'} / N_{U'/V'}(A'^{V'}) of norm quotients induced
by a layer isomorphism.
Instances For
The isomorphism of norm quotients sends the class of a to the class of its image.
The inverse isomorphism of norm quotients sends the class of b to the class of its inverse
image.
On norm quotients, the underlying layer morphism acts as the isomorphism of norm quotients.
In degree zero the Tate transport is the transport of norm quotients, through the
identifications tateHZeroEquivNormQuotient of the two layers.
Conjugation #
Conjugation by g as a layer isomorphism from V ◁ U to gVg⁻¹ ◁ gUg⁻¹, within one
formation.
Instances For
On ordinary cohomology, conjugation as a layer isomorphism is conjugateCohomologyIso.
Class formations #
A layer isomorphism matching the invariant maps matches the fundamental classes.
The Artin map is transported by a layer isomorphism matching the invariant maps: 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.