Transporting finite normal layers along open embeddings

An injective open homomorphism of profinite groups carries every finite normal layer in its source to a finite normal layer in its target. If a formation on the source is identified with the restriction of a formation on the target, the two layers are canonically isomorphic in the sense of LayerEquiv.

The motivating example is the open embedding G_L → G_K attached to a finite extension of fields. Together with localFormationRestrict, the construction in this file identifies a finite layer of the units formation over L with its image in the units formation over K. This is the layer comparison needed to apply ClassFormation.artinMap_layerEquiv in the proof of the norm compatibility of the local Artin map.

Main definitions

• TauCeti.ClassFieldTheory.NormalLayer.map: the image of a normal layer under an open homomorphism.
• TauCeti.ClassFieldTheory.NormalLayer.mapGalEquiv: the canonical isomorphism between the Galois group of a layer and that of its image under an injective homomorphism.
• TauCeti.ClassFieldTheory.NormalLayer.mapLayerEquiv: the resulting layer isomorphism when the coefficient formations agree after restriction.
• TauCeti.ClassFieldTheory.localFormationLayerEquiv: the specialization to the units formations of a finite extension of fields.

Main results

• TauCeti.ClassFieldTheory.localFormationMap_ofOpenNormal_ground_toSubgroup: the ground subgroup of the image over K of a layer V ◁ G_E is Gal(Kˢ/iota(E)).
• TauCeti.ClassFieldTheory.fixedField_localFormationMap_ofOpenNormal_ground: the fixed field of that ground subgroup is iota(E).
• TauCeti.ClassFieldTheory.layerRestriction_localFormationMap: for V ≤ Gal(Kˢ/iota(E)) open normal in G_K, the image over K of the layer cut out by the preimage of V in G_E is the restriction of the layer V ◁ G_K to Gal(Kˢ/iota(E)).

def TauCeti.ClassFieldTheory.NormalLayer.map {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) : NormalLayer G'

The image of a finite normal layer under an open group homomorphism. Openness is used only to make the two image subgroups open; normality inside the image of the ground subgroup is preserved by every homomorphism.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.map_ground_toSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) : ↑(L.map f hf).ground = Subgroup.map f ↑L.ground

The ground subgroup of the mapped layer is the image of the original ground subgroup.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.map_top_toSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) : ↑(L.map f hf).top = Subgroup.map f ↑L.top

The top subgroup of the mapped layer is the image of the original top subgroup.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.mapGroundEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) : ↥L.ground ≃* ↥(L.map f hf).ground

An injective homomorphism identifies the ground subgroup of a layer with the ground subgroup of its image.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mapGroundEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) (u : ↥L.ground) : ↑((L.mapGroundEquiv f hf hfi) u) = f ↑u

On underlying group elements, mapGroundEquiv is the original homomorphism.

theorem TauCeti.ClassFieldTheory.NormalLayer.map_relativeTop_mapGroundEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) : Subgroup.map (↑(L.mapGroundEquiv f hf hfi)) L.relativeTop = (L.map f hf).relativeTop

The ground-subgroup equivalence carries the relative top subgroup onto the relative top subgroup of the mapped layer.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.mapGalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) : L.Gal ≃* (L.map f hf).Gal

The canonical isomorphism from the Galois group of a layer to the Galois group of its image under an injective open homomorphism.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mapGalEquiv_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) (u : ↥L.ground) : (L.mapGalEquiv f hf hfi) ↑u = ↑((L.mapGroundEquiv f hf hfi) u)

mapGalEquiv sends the class of a representative to the class of its image.

def TauCeti.ClassFieldTheory.NormalLayer.mapCoeffEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') {F : Formation G} {F' : Formation G'} (hf : IsOpenMap ⇑f) (e : TopRep.res f F'.module ≅ F.module) : ↥(F.level L.top) ≃ₗ[ℤ] ↥(F'.level (L.map f hf).top)

An isomorphism between a formation and the restriction of another formation identifies the top levels of a layer and its image. The direction of e follows TopRep.res: its inverse sends coefficients of F to coefficients of F'.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mapCoeffEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') {F : Formation G} {F' : Formation G'} (hf : IsOpenMap ⇑f) (e : TopRep.res f F'.module ≅ F.module) (x : ↥(F.level L.top)) : ↑((L.mapCoeffEquiv f hf e) x) = (CategoryTheory.ConcreteCategory.hom e.inv) ↑x

On underlying coefficient modules, mapCoeffEquiv is the inverse of the chosen restriction isomorphism.

theorem TauCeti.ClassFieldTheory.NormalLayer.mapCoeffEquiv_rep_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') {F : Formation G} {F' : Formation G'} (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) (e : TopRep.res f F'.module ≅ F.module) (u : ↥L.ground) (x : ↥(F.level L.top)) : (L.mapCoeffEquiv f hf e) (((L.rep F).ρ ↑u) x) = (((L.map f hf).rep F').ρ ↑((L.mapGroundEquiv f hf hfi) u)) ((L.mapCoeffEquiv f hf e) x)

The coefficient equivalence intertwines the action of a ground-subgroup representative with the action of its image.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.mapLayerEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {G' : Type} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [CompactSpace G'] [TotallyDisconnectedSpace G'] (L : NormalLayer G) (f : G →* G') {F : Formation G} {F' : Formation G'} (hf : IsOpenMap ⇑f) (hfi : Function.Injective ⇑f) (e : TopRep.res f F'.module ≅ F.module) : LayerEquiv F L F' (L.map f hf)

Transporting a normal layer along an injective open homomorphism gives a layer isomorphism whenever the source formation is the restriction of the target formation.

Finite extensions of fields

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.localFormationMap (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) : NormalLayer (AbsoluteGaloisGroup K)

A finite normal layer over E regarded as a finite normal layer over K, using the chosen embedding E → Kˢ.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.localFormationMap_ground_toSubgroup (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) : ↑(localFormationMap K E iota L).ground = Subgroup.map (localFormationHom K E iota) ↑L.ground

The ground subgroup of a layer over E, regarded over K, is the image of its ground subgroup under the embedding G_E → G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.localFormationMap_top_toSubgroup (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) : ↑(localFormationMap K E iota L).top = Subgroup.map (localFormationHom K E iota) ↑L.top

The top subgroup of a layer over E, regarded over K, is the image of its top subgroup under the embedding G_E → G_K.

theorem TauCeti.ClassFieldTheory.localFormationMap_ofOpenNormal_ground_toSubgroup (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup E)) : ↑(NormalLayer.localFormationMap K E iota (NormalLayer.ofOpenNormal V)).ground = ↑(galoisSubgroup K E iota)

The ground subgroup of the layer over K corresponding to a layer V ◁ G_E is Gal(Kˢ/iota(E)).

theorem TauCeti.ClassFieldTheory.fixedField_localFormationMap_ofOpenNormal_ground (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup E)) : IntermediateField.fixedField ↑(NormalLayer.localFormationMap K E iota (NormalLayer.ofOpenNormal V)).ground = iota.fieldRange

The ground subgroup Gal(Kˢ/iota(E)) of the layer over K corresponding to a layer V ◁ G_E has fixed field iota(E). This is the hypothesis under which unitsLevelEquiv identifies the ground level of that layer with Eˣ.

theorem TauCeti.ClassFieldTheory.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)) : LayerRestriction (NormalLayer.localFormationMap K E iota (NormalLayer.ofOpenNormal (V.comap (localFormationHom K E iota) ⋯))) (NormalLayer.ofOpenNormal V)

For an open normal subgroup V ≤ Gal(Kˢ/iota(E)) of G_K with preimage V' in G_E, the layer over K corresponding to V' ◁ G_E is the restriction V ◁ Gal(Kˢ/iota(E)) of V ◁ G_K.

noncomputable def TauCeti.ClassFieldTheory.localFormationLayerEquiv (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) : LayerEquiv (unitsFormation E) L (unitsFormation K) (NormalLayer.localFormationMap K E iota L)

A layer over a finite extension as a layer over the base field. Restriction identifies the units formation over E with the restriction of the units formation over K, and hence identifies every finite normal layer over E with its image layer over K.

theorem TauCeti.ClassFieldTheory.localFormationLayerEquiv_galEquiv_mk (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) (u : ↥L.ground) (u' : ↥(NormalLayer.localFormationMap K E iota L).ground) (h : ↑u' = (localFormationHom K E iota) ↑u) : (localFormationLayerEquiv K E iota L).galEquiv ↑u = ↑u'

The Galois-group isomorphism of localFormationLayerEquiv sends the class of u to the class of any representative of its image in G_K.

theorem TauCeti.ClassFieldTheory.localFormationLayerEquiv_coeffEquiv_apply (K : Type) [Field K] (E : Type) [Field E] [Algebra K E] [FiniteDimensional K E] (iota : E →ₐ[K] SeparableClosure K) (L : NormalLayer (AbsoluteGaloisGroup E)) (x : ↥((unitsFormation E).level L.top)) : (unitsCoeffEquivUnitsFormation K).symm ↑((localFormationLayerEquiv K E iota L).coeffEquiv x) = (localFormationCoeffEquiv K E iota).symm ((unitsCoeffEquivUnitsFormation E).symm ↑x)

The coefficient isomorphism of localFormationLayerEquiv, read on (Eˢ)ˣ and (Kˢ)ˣ, is the inverse of the coefficient equivalence localFormationCoeffEquiv of the restriction.