Continuity and compatibility of valued field homomorphisms

The algebra map of a compatible valued field extension is continuous if nonzero values of the base field are coinitial among the nonzero values of the extension. Algebraic extensions satisfy this condition, with no restriction on the rank of the valuations or completeness of the fields. Compatibility alone does not imply continuity for transcendental extensions.

Let K and L be division rings whose topologies are induced by their valuative relations, with archimedean value groups (that is, of rank at most one), and with the valuation of K nontrivial. This file proves that every continuous ring homomorphism f : K →+* L preserves and reflects the valuative relation: f x ≤ᵥ f y ↔ x ≤ᵥ y. Nonarchimedean local fields satisfy these hypotheses. So a field isomorphism of nonarchimedean local fields that is a homeomorphism is compatible with their valuations, and an algebra between such fields whose structure map is continuous is a ValuativeExtension; this is what allows constructions made from the valuation of a local field to be compared along an isomorphism that is only known to be topological.

The bridge between topology and valuation is topological nilpotence. In a valuative topology the open unit ball {x | v x < 1} is a neighbourhood of 0, so a topologically nilpotent element has valuation < 1 (IsTopologicallyNilpotent.valuation_lt_one); conversely, when the value group is archimedean, the powers of an element of valuation < 1 enter every ball around 0 (isTopologicallyNilpotent_iff_valuation_lt_one, in TauCeti.RingTheory.Valuation.Continuous.TopologicallyNilpotent). Since a continuous homomorphism preserves topological nilpotence, v_K x < 1 implies v_L (f x) < 1. For the reverse implication, let v_K x ≥ 1 and pick π with 0 < v_K π < 1. Then v_K (π / xⁿ) < 1 for every n, so v_L (f π) < v_L (f x) ^ n for every n, which, the value group of L being archimedean, forces v_L (f x) ≥ 1. Two valuations on a division ring with the same open unit ball are equivalent (Valuation.isEquiv_iff_val_lt_one). This is the argument of Neukirch, Chapter II, Proposition (3.3), for absolute values.

Main results

• TauCeti.continuous_algebraMap_of_coinitial: coinitiality of nonzero base-field values implies continuity of the algebra map of a compatible extension.
• TauCeti.continuous_algebraMap_of_valuativeExtension: the algebra map of an algebraic compatible extension is continuous.
• TauCeti.continuous_algebraMap_integerRing: so is its restriction to the rings of integers.
• RingHom.isEquiv_comap_valuation_of_continuous: the pullback of the valuation of L along a continuous f : K →+* L is equivalent to the valuation of K.
• RingHom.map_vle_map_iff_of_continuous: a continuous f : K →+* L satisfies f x ≤ᵥ f y ↔ x ≤ᵥ y.
• ValuativeExtension.of_continuous_algebraMap: an algebra whose structure map is continuous is a valuative extension.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition (3.3).

theorem TauCeti.continuous_algebraMap_of_coinitial (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [DivisionRing L] [ValuativeRel L] [TopologicalSpace L] [IsValuativeTopology L] [Algebra K L] [ValuativeExtension K L] (h : ∀ (y : L), y ≠ 0 → ∃ (x : K), x ≠ 0 ∧ (algebraMap K L) x ≤ᵥ y) : Continuous ⇑(algebraMap K L)

The algebra map of a compatible extension is continuous if the nonzero base-field values are coinitial among the nonzero target values.

theorem TauCeti.continuous_algebraMap_of_valuativeExtension (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsValuativeTopology L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsAlgebraic K L] : Continuous ⇑(algebraMap K L)

The algebra map of an algebraic compatible extension is continuous for the valuative topologies.

theorem TauCeti.continuous_algebraMap_integerRing (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsValuativeTopology L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsAlgebraic K L] : Continuous ⇑(algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer)

The structure map of the rings of integers of an algebraic compatible extension is continuous for the subspace topologies.

theorem RingHom.isEquiv_comap_valuation_of_continuous {K : Type u_1} {L : Type u_2} [DivisionRing K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [ValuativeRel.IsNontrivial K] [MulArchimedean (ValuativeRel.ValueGroupWithZero K)] [DivisionRing L] [ValuativeRel L] [TopologicalSpace L] [IsValuativeTopology L] [MulArchimedean (ValuativeRel.ValueGroupWithZero L)] (f : K →+* L) (hf : Continuous ⇑f) : (Valuation.comap f (ValuativeRel.valuation L)).IsEquiv (ValuativeRel.valuation K)

A continuous ring homomorphism preserves the valuation up to equivalence: the pullback of the valuation of L along a continuous f : K →+* L is equivalent to the valuation of K.

@[simp]

theorem RingHom.map_vle_map_iff_of_continuous {K : Type u_1} {L : Type u_2} [DivisionRing K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [ValuativeRel.IsNontrivial K] [MulArchimedean (ValuativeRel.ValueGroupWithZero K)] [DivisionRing L] [ValuativeRel L] [TopologicalSpace L] [IsValuativeTopology L] [MulArchimedean (ValuativeRel.ValueGroupWithZero L)] (f : K →+* L) (hf : Continuous ⇑f) (x y : K) : f x ≤ᵥ f y ↔ x ≤ᵥ y

A continuous ring homomorphism preserves and reflects the valuative relation.

theorem ValuativeExtension.of_continuous_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsValuativeTopology K] [ValuativeRel.IsNontrivial K] [MulArchimedean (ValuativeRel.ValueGroupWithZero K)] [DivisionRing L] [ValuativeRel L] [TopologicalSpace L] [IsValuativeTopology L] [MulArchimedean (ValuativeRel.ValueGroupWithZero L)] [Algebra K L] (hf : Continuous ⇑(algebraMap K L)) : ValuativeExtension K L

An algebra whose structure map is continuous is a valuative extension: the valuative relation of L restricts to that of K.