Commit 2026-05-28 09:20 0784f68c

View on Github →

feat: algebraMap K L is uniform continuous with respect to adic topologies, when the ideal w of L lies above v (#34045)

A is a Dedekind domain with field of fractions K.
B is a Dedekind domain with field of fractions L.
L is a field extension of K.
v is a height one prime ideal of A.
w is a height one prime ideal of B lying over v. Then respective valuations are related via the ramification index, and algebraMap (WithVal (v.valuation K)) (WithVal (w.valuation L)) is uniform continuous.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Hom/Units.lean

modified def OrderMonoidIso.unitsCongr

added theorem OrderMonoidIso.unitsCongr_symm_apply

Created Mathlib/NumberTheory/RamificationInertia/Valuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_liesOver

added theorem IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_liesOver

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/Valuation/Discrete/RankOne.lean

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean

added theorem WithVal.valuation_apply_eq_ofVal

deleted theorem WithVal.valuation_equiv_symm

added theorem WithVal.valuation_toVal

modified def WithVal.valueGroupEquiv

modified def WithVal.valueGroupOrderIso₀

modified theorem WithVal.valueGroup_eq