Local-field structures on finite intermediate fields

A finite intermediate field of an extension of a nonarchimedean local field need not inherit a topology or a valuative relation from its ambient field. This file packages the spectral-norm construction for such an intermediate field directly. The resulting named normed-field, valuative-relation, and topology structures can be installed locally without placing any structure on the ambient field and without introducing global instance diamonds.

The three accompanying theorems give the closed construction chain needed by consumers: the new valuative relation extends the one on the base, the new topology is valuative, and together they make the intermediate field a nonarchimedean local field.

Main definitions

• TauCeti.finiteIntermediateFieldNormedField: the spectral-norm structure on a finite intermediate field.
• TauCeti.finiteIntermediateFieldValuativeRel: its valuative relation.
• TauCeti.finiteIntermediateFieldTopology: its topology.

Main results

• TauCeti.finiteIntermediateField_valuativeExtension: the valuation extends the base valuation.
• TauCeti.finiteIntermediateField_isValuativeTopology: the topology is induced by the valuation.
• TauCeti.finiteIntermediateField_isNonarchimedeanLocalField: the intermediate field is a nonarchimedean local field.
• IntermediateField.valuativeExtension: if the ambient field carries a valuative relation extending that of K, it is a valuative extension of every finite intermediate field whose valuative relation extends that of K.
• IntermediateField.valuativeExtension_of_isNonarchimedeanLocalField: when the ambient field is itself a nonarchimedean local field extending K, this holds for every compatible intermediate field, and is an instance.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §6.
• J.-P. Serre, Corps Locaux, Chapter II, §2.

@[implicit_reducible]

noncomputable def TauCeti.finiteIntermediateFieldNormedField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (M : IntermediateField K Ω) [Module.Finite K ↥M] : NormedField ↥M

The spectral-norm structure on a finite intermediate field M/K, constructed without requiring a norm, topology, or valuative relation on the ambient field.

Equations

• TauCeti.finiteIntermediateFieldNormedField K Ω M = TauCeti.finiteExtensionNormedField K ↥M

@[implicit_reducible]

noncomputable def TauCeti.finiteIntermediateFieldValuativeRel (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (M : IntermediateField K Ω) [Module.Finite K ↥M] : ValuativeRel ↥M

The valuative relation defined by the spectral norm on a finite intermediate field M/K. It is a named structure so consumers can install it locally without creating instance diamonds.

Equations

• TauCeti.finiteIntermediateFieldValuativeRel K Ω M = TauCeti.finiteExtensionValuativeRel K ↥M

@[implicit_reducible]

noncomputable def TauCeti.finiteIntermediateFieldTopology (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (M : IntermediateField K Ω) [Module.Finite K ↥M] : TopologicalSpace ↥M

The topology defined by the spectral norm on a finite intermediate field M/K.

Equations

• TauCeti.finiteIntermediateFieldTopology K Ω M = TauCeti.finiteExtensionNormedFieldTopology K ↥M

theorem TauCeti.finiteIntermediateField_valuativeExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (M : IntermediateField K Ω) [Module.Finite K ↥M] : ValuativeExtension K ↥M

The valuative relation constructed on a finite intermediate field extends the valuative relation of the base field.

theorem TauCeti.finiteIntermediateField_isValuativeTopology (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (M : IntermediateField K Ω) [Module.Finite K ↥M] : IsValuativeTopology ↥M

The spectral-norm topology and valuative relation constructed on a finite intermediate field are compatible.

theorem TauCeti.finiteIntermediateField_isNonarchimedeanLocalField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (M : IntermediateField K Ω) [Module.Finite K ↥M] : IsNonarchimedeanLocalField ↥M

A finite intermediate field, equipped with its spectral-norm topology and valuative relation, is a nonarchimedean local field.

theorem IntermediateField.valuativeExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [ValuativeRel Ω] [ValuativeExtension K Ω] (E : IntermediateField K Ω) [Module.Finite K ↥E] [ValuativeRel ↥E] [ValuativeExtension K ↥E] : ValuativeExtension (↥E) Ω

The ambient field is a valuative extension of a compatible intermediate field. If Ω carries a valuative relation extending that of K, and a finite intermediate field E of Ω / K carries one as well, then Ω is a valuative extension of E: both relations restrict to the valuation class of K, and the extension of that class to E is unique.

instance IntermediateField.valuativeExtension_of_isNonarchimedeanLocalField {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [ValuativeRel Ω] [TopologicalSpace Ω] [IsNonarchimedeanLocalField Ω] [ValuativeExtension K Ω] (E : IntermediateField K Ω) [ValuativeRel ↥E] [ValuativeExtension K ↥E] : ValuativeExtension (↥E) Ω

A local field is a valuative extension of its compatible intermediate fields. For an extension Ω / K of nonarchimedean local fields and an intermediate field E carrying a valuative relation extending that of K, the valuative relation of Ω extends that of E. The finiteness of Ω / K needed by IntermediateField.valuativeExtension is automatic here, so this is an instance.