The finite tame layer attached to a finite Galois quotient

For an open normal subgroup U of the absolute Galois group of a perfect nonarchimedean local field K, let L be the fixed field of P_K U, where P_K is wild inertia. This is a finite Galois, tamely ramified extension. Its Galois group is canonically G_K / (P_K U) and admits a generating pair whose second element has order prime to the residue characteristic.

The exact fixing-subgroup equation identifies this arithmetic layer with the subgroup used in the pro-p class-module extension. The generating pair permits the tame-frame relation-module construction to be applied to this layer of any finite Galois quotient. The local-field structures on L may be any structures compatible with K. Its canonical embedding into the separable closure identifies the arithmetic fixing subgroup with the same product P_K U in the algebraic-closure model.

The quotient comparison specializes TauCeti.absoluteGaloisGroupQuotientEquivOfEq, and the pair is the image of the frame supplied by TauCeti.exists_tameFrame_quotient.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).

noncomputable def TauCeti.tameLayerSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : OpenNormalSubgroup (Field.absoluteGaloisGroup K)

The open normal subgroup P_K U associated with a finite Galois quotient.

@[simp]

theorem TauCeti.tameLayerSubgroup_toSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : ↑(tameLayerSubgroup K U).toOpenSubgroup = wildInertiaSubgroup K ⊔ ↑U.toOpenSubgroup

The subgroup defining the tame layer is the product of wild inertia and U.

noncomputable def TauCeti.tameLayer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : IntermediateField K (AlgebraicClosure K)

The fixed field of P_K U inside the algebraic closure of K. Over a perfect local field it is a finite tame Galois layer.

theorem TauCeti.tameLayer_def (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : tameLayer K U = IntermediateField.fixedField (wildInertiaSubgroup K ⊔ ↑U.toOpenSubgroup)

The tame layer is the fixed field of the product of wild inertia and U.

@[simp]

theorem TauCeti.mem_tameLayer_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (x : AlgebraicClosure K) : x ∈ tameLayer K U ↔ (∀ σ ∈ wildInertiaSubgroup K, σ x = x) ∧ ∀ σ ∈ U, σ x = x

Membership in the tame layer means being fixed by both wild inertia and U.

@[simp]

theorem TauCeti.fixingSubgroup_tameLayer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : (tameLayer K U).fixingSubgroup = wildInertiaSubgroup K ⊔ ↑U.toOpenSubgroup

The automorphisms fixing the tame layer are exactly P_K U.

instance TauCeti.finiteDimensional_tameLayer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : FiniteDimensional K ↥(tameLayer K U)

The tame layer is finite over K, since P_K U is open.

instance TauCeti.isGalois_tameLayer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : IsGalois K ↥(tameLayer K U)

The tame layer is Galois over K, since P_K U is normal.

noncomputable def TauCeti.tameLayerEmbedding (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : ↥(tameLayer K U) →ₐ[K] SeparableClosure K

The canonical inclusion of the finite tame layer into the separable closure.

@[simp]

theorem TauCeti.coe_tameLayerEmbedding (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (x : ↥(tameLayer K U)) : ↑((tameLayerEmbedding K U) x) = ↑x

The separable-closure inclusion preserves the original algebraic-closure coordinates.

@[simp]

theorem TauCeti.tameLayerEmbedding_restrictNormalHom (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (σ : Field.absoluteGaloisGroup K) : (tameLayerEmbedding K U).restrictNormalHom ((absoluteGaloisGroupRestrictEquiv K) σ) = (AlgEquiv.restrictNormalHom ↥(tameLayer K U)) σ

Restriction to the tame layer agrees in the algebraic and separable closure models.

@[simp]

theorem TauCeti.galoisSubgroup_tameLayerEmbedding_comap (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : Subgroup.comap (absoluteGaloisGroupRestrictEquiv K).toMonoidHom ↑(galoisSubgroup K (↥(tameLayer K U)) (tameLayerEmbedding K U)) = wildInertiaSubgroup K ⊔ ↑U.toOpenSubgroup

The subgroup fixing the embedded tame layer pulls back to the product of wild inertia and the prescribed open normal subgroup.

noncomputable def TauCeti.quotientTameLayerEquiv (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : Field.absoluteGaloisGroup K ⧸ ↑(tameLayerSubgroup K U).toOpenSubgroup ≃ₜ* Gal(↥(tameLayer K U)/K)

The finite quotient by P_K U is the Galois group of the associated tame layer.

@[simp]

theorem TauCeti.quotientTameLayerEquiv_mk (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (σ : Field.absoluteGaloisGroup K) : (quotientTameLayerEquiv K U) ↑σ = (AlgEquiv.restrictNormalHom ↥(tameLayer K U)) σ

The quotient identification is restriction of automorphisms to the tame layer.

@[simp]

theorem TauCeti.quotientTameLayerEquiv_symm_restrictNormalHom (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (σ : Field.absoluteGaloisGroup K) : (quotientTameLayerEquiv K U).symm ((AlgEquiv.restrictNormalHom ↥(tameLayer K U)) σ) = ↑σ

The inverse quotient identification sends a restricted automorphism back to its class.

theorem TauCeti.isTamelyRamified_tameLayer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) [ValuativeRel ↥(tameLayer K U)] [TopologicalSpace ↥(tameLayer K U)] [IsNonarchimedeanLocalField ↥(tameLayer K U)] [ValuativeExtension K ↥(tameLayer K U)] : IsTamelyRamified K ↥(tameLayer K U)

The layer fixed by P_K U is tamely ramified for any compatible local-field structures.

theorem TauCeti.exists_tameFrame_tameLayer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [PerfectField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) : ∃ (σ : Gal(↥(tameLayer K U)/K)) (τ : Gal(↥(tameLayer K U)/K)), Subgroup.closure {σ, τ} = ⊤ ∧ ¬p ∣ orderOf τ

The Galois group of the tame layer has a generating pair with second element of order prime to the residue characteristic. This is the frame for the integral relation module.