The local class formation of a finite extension inside that of the base

Let K be a nonarchimedean local field and E/K a finite extension, embedded in Kˢ by iota : E →ₐ[K] Kˢ. The embedding identifies G_E with the open subgroup of G_K fixing iota(E) (TauCeti.ClassFieldTheory.localFormationHom), and the units formation of E with the restriction of that of K to this subgroup (TauCeti.ClassFieldTheory.localFormationRestrict), so every finite normal layer of the formation of E is isomorphic to a finite normal layer of the formation of K (TauCeti.ClassFieldTheory.localFormationLayerEquiv).

This file proves that this isomorphism matches the invariant maps of the two local class formations (localClassFormation_inv_localFormationLayerEquiv): the invariant of a class in the formation of E is the invariant of its image in the formation of K. Consequently the Artin map of a finite normal layer V ◁ U of the formation of E (the local Artin map of the extension of the fixed field of U cut out by V) is the abstract Artin map of the corresponding layer of the formation of K (artinMap_localFormationLayerEquiv). Combined with the Artin–Tate diagram TauCeti.ClassFieldTheory.ClassFormation.artinMap_groundNorm inside the formation of K, this is what relates the local Artin map of E to that of K through the norm N_{E/K}. The two ground-level facts this needs are also here: the isomorphism sends y ∈ Eˣ to iota y (groundEquiv_localFormationLayerEquiv_localGroundEquiv), and the ground-level norm of the corresponding restriction inside the formation of K is N_{E/K} (groundNorm_layerRestriction_localFormationMap).

The comparison is first made for the local invariant TauCeti.ClassFieldTheory.subgroupInvMap of an open subgroup U ≤ G_E and its image U' ≤ G_K (subgroupInvMap_explicitMap2_localFormationHomInv), and for inflation from a layer to its ground subgroup (explicitInfl2_localFormationLayerEquiv).

Main results

• TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2_localFormationHomInv: the local invariant of an open subgroup of G_E is that of its image in G_K.
• TauCeti.ClassFieldTheory.localClassFormation_inv_localFormationLayerEquiv: the layer isomorphism localFormationLayerEquiv matches the invariant maps of the local class formations.
• TauCeti.ClassFieldTheory.artinMap_localFormationLayerEquiv: it carries the Artin map of a layer of the formation of E to the Artin map of the corresponding layer of the formation of K.
• TauCeti.ClassFieldTheory.groundEquiv_localFormationLayerEquiv_localGroundEquiv: on ground levels, localFormationLayerEquiv sends y ∈ Eˣ to the unit iota y of the level of Gal(Kˢ/iota(E)).
• TauCeti.ClassFieldTheory.groundNorm_layerRestriction_localFormationMap: for an open normal subgroup V ≤ Gal(Kˢ/iota(E)) of G_K, the ground-level norm of the restriction of V ◁ G_K to Gal(Kˢ/iota(E)) is the field norm N_{E/K}.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1 and 6.
• J.-P. Serre, Local Fields, Chapter XI, §3.

Inflation from corresponding layers

@[simp]

theorem TauCeti.ClassFieldTheory.unitsCoeffMapSymm_localFormationHomInv_smul (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) {U : Subgroup (AbsoluteGaloisGroup E)} {U' : Subgroup (AbsoluteGaloisGroup K)} (h : U' ≤ Subgroup.map (localFormationHom K E iota) U) (u : ↥U') (y : UnitsCoeff E) : (unitsCoeffMapSymm K E iota) ((localFormationHomInv K E iota h) u • y) = u • (unitsCoeffMapSymm K E iota) y

The units of Eˢ as units of Kˢ form a compatible pair with localFormationHomInv.

@[simp]

theorem TauCeti.ClassFieldTheory.localFormationCoeffEquiv_symm_apply (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] (iota : E →ₐ[K] SeparableClosure K) (y : UnitsCoeff E) : (localFormationCoeffEquiv K E iota).symm y = (unitsCoeffMapSymm K E iota) y

The inverse of the coefficient equivalence of localFormationRestrict is the coefficient map unitsCoeffMapSymm of Kummer theory: both send a unit of Eˢ to its image in Kˢ under the identification Eˢ ≃ Kˢ extending iota.

theorem TauCeti.ClassFieldTheory.explicitInfl2_localFormationLayerEquiv (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) (x : ↑(L.H (unitsFormation E) 2)) : ((NormalLayer.localFormationMap K E iota L).explicitInfl2 (unitsCoeffEquivUnitsFormation K) ⋯) ((CategoryTheory.ConcreteCategory.hom ((localFormationLayerEquiv K E iota L).cohomologyIso 2).hom) x) = (ContCohomology.explicitMap2 (↥↑L.ground) (UnitsCoeff E) (↥↑(NormalLayer.localFormationMap K E iota L).ground) (UnitsCoeff K) (localFormationHomInv K E iota ⋯) (unitsCoeffMapSymm K E iota) ⋯ ⋯) ((L.explicitInfl2 (unitsCoeffEquivUnitsFormation E) ⋯) x)

Inflation commutes with the layer isomorphism localFormationLayerEquiv: inflating the image of a class of a layer V ◁ U over E to the ground subgroup U' of the corresponding layer over K is transporting its inflation to U along U' ≃ U and (Eˢ)ˣ ≃ (Kˢ)ˣ.

theorem TauCeti.ClassFieldTheory.groundEquiv_localFormationLayerEquiv_localGroundEquiv (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup E)) (y : Additive Eˣ) : (localFormationLayerEquiv K E iota (NormalLayer.ofOpenNormal V)).groundEquiv ((localGroundEquiv E V) y) = (unitsLevelEquiv iota ⋯) y

The unit y ∈ Eˣ, read in the ground level ((Eˢ)ˣ)^{G_E} of a layer V ◁ G_E and carried to the corresponding layer over K, is the unit iota y of the level of Gal(Kˢ/iota(E)).

theorem TauCeti.ClassFieldTheory.groundNorm_layerRestriction_localFormationMap (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (hV : ↑V.toOpenSubgroup ≤ ↑(galoisSubgroup K E iota)) (x : Additive Eˣ) : (⋯.groundNorm (unitsFormation K)) ((unitsLevelEquiv iota ⋯) x) = (localGroundEquiv K V) (Additive.ofMul ((Algebra.normUnits K) (Additive.toMul x)))

For an open normal subgroup V ≤ Gal(Kˢ/iota(E)) of G_K, the norm from the ground level Gal(Kˢ/iota(E)) to the ground level G_K of the restriction layerRestriction_localFormationMap sends iota x to N_{E/K} x.

The local invariant of an open subgroup of G_E

theorem TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2_localFormationHomInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : Type) [Field E] [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Algebra K E] [ValuativeExtension K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) {U : Subgroup (AbsoluteGaloisGroup E)} [U.FiniteIndex] (hU : IsOpen ↑U) {U' : Subgroup (AbsoluteGaloisGroup K)} [U'.FiniteIndex] (hU' : IsOpen ↑U') (hUU' : Subgroup.map (localFormationHom K E iota) U = U') (y : ContCohomology.H2 (↥U) (UnitsCoeff E)) : (subgroupInvMap K U' hU') ((ContCohomology.explicitMap2 (↥U) (UnitsCoeff E) (↥U') (UnitsCoeff K) (localFormationHomInv K E iota ⋯) (unitsCoeffMapSymm K E iota) ⋯ ⋯) y) = (subgroupInvMap E U hU) y

The local invariant of an open subgroup of G_E is that of its image in G_K: for an open subgroup U ≤ G_E with image U' under the embedding G_E → G_K, a class of H²(U, (Eˢ)ˣ) transported to H²(U', (Kˢ)ˣ) along U' ≃ U and (Eˢ)ˣ ≃ (Kˢ)ˣ has the same invariant. For U = G_E this is subgroupInvMap_explicitMap2.

The local class formations of E and of K

theorem TauCeti.ClassFieldTheory.localClassFormation_inv_localFormationLayerEquiv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : Type) [Field E] [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Algebra K E] [ValuativeExtension K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) (x : ↑(L.H (unitsFormation E) 2)) : ((localClassFormation K).inv (NormalLayer.localFormationMap K E iota L)) ((CategoryTheory.ConcreteCategory.hom ((localFormationLayerEquiv K E iota L).cohomologyIso 2).hom) x) = ((localClassFormation E).inv L) x

The local class formation of E is that of K on corresponding layers: the layer isomorphism localFormationLayerEquiv from a finite normal layer of the units formation of E to the corresponding layer of the units formation of K matches the invariant maps of the two local class formations.

theorem TauCeti.ClassFieldTheory.artinMap_localFormationLayerEquiv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : Type) [Field E] [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Algebra K E] [ValuativeExtension K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) (a : ↥((unitsFormation E).level L.ground)) : ((localClassFormation K).artinMap (NormalLayer.localFormationMap K E iota L)) ((localFormationLayerEquiv K E iota L).groundEquiv a) = (MulEquiv.toAdditive (localFormationLayerEquiv K E iota L).galEquiv.abelianizationCongr) (((localClassFormation E).artinMap L) a)

The Artin map of a layer over E is the Artin map of the corresponding layer over K: for a finite normal layer V ◁ U of the units formation of E, the Artin symbol of the image of a ∈ ((Eˢ)ˣ)^U in the corresponding layer of the units formation of K is the image of the Artin symbol of a under the induced isomorphism of abelianized Galois groups.