Compatibility of local-field structures in towers

For a tower M/L/K, where K and L are nonarchimedean local fields and M/K is algebraic, the valuative relation and topology constructed on M do not depend on whether the construction starts from K or from L. Thus constructions on algebraic subextensions can be compared without postulating compatible structures on the top field.

The norms themselves are not asserted equal: the normalized absolute values on K and L can have different normalizations. Uniqueness of the extended valuative relation identifies their orders, and hence their topologies.

Main results

• TauCeti.algebraicExtensionValuativeRel_tower: equality of the constructed valuative relations.
• TauCeti.algebraicExtensionNormedFieldTopology_tower: equality of the constructed topologies.
• TauCeti.algebraicExtension_valuativeExtension_tower: the construction over K also extends the valuative relation on L.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §4 (uniqueness of extended valuations).

theorem TauCeti.algebraicExtensionValuativeRel_tower (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Algebra.IsAlgebraic K M] : algebraicExtensionValuativeRel K M = algebraicExtensionValuativeRel L M

Extending the valuative relation through an intermediate local field agrees with extending it directly from the base field. No valuative relation on M is assumed.

theorem TauCeti.algebraicExtensionNormedFieldTopology_tower (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Algebra.IsAlgebraic K M] : algebraicExtensionNormedFieldTopology K M = algebraicExtensionNormedFieldTopology L M

The spectral-norm topology on an algebraic extension is unchanged when constructed through an intermediate local field. No topology on M is assumed.

theorem TauCeti.algebraicExtension_valuativeExtension_tower (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Algebra.IsAlgebraic K M] : have x := algebraicExtensionValuativeRel K M; ValuativeExtension L M

With the valuative relation constructed directly over K, the top field of an algebraic tower is a valuative extension of the intermediate field as well.