Skip to content

feat(NumberTheory/NumberField/Completion/FinitePlace): compatibility of finite places across an algebra map #41604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tb65536 wants to merge 2 commits into
base: master
Choose a base branch
from
+23 −4
Open

feat(NumberTheory/NumberField/Completion/FinitePlace): compatibility of finite places across an algebra map #41604

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
39bdfca
add
tb65536 Jul 10, 2026
7a14eab
add todo
tb65536 Jul 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 23 additions & 4 deletions Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module
public import Mathlib.Algebra.Order.Archimedean.Submonoid
public import Mathlib.LinearAlgebra.FreeModule.IdealQuotient
public import Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
public import Mathlib.NumberTheory.RamificationInertia.Valuation
public import Mathlib.RingTheory.DedekindDomain.AdicValuation
public import Mathlib.RingTheory.DedekindDomain.Factorization
public import Mathlib.RingTheory.Valuation.Archimedean
Expand Down Expand Up @@ -88,8 +89,8 @@ end DVR

namespace NumberField

variable {K : Type*} [Field K] {R : Type*} [CommRing R] [Algebra R K] [IsDedekindDomain R]
[IsFractionRing R K] (v : HeightOneSpectrum R)
variable {K L : Type*} [Field K] [Field L] [Algebra K L] {R : Type*} [CommRing R] [Algebra R K]
[IsDedekindDomain R] [IsFractionRing R K] (v : HeightOneSpectrum R)

/-- The embedding of a field inside its `adicCompletion` with respect to `v`. -/
noncomputable def FinitePlace.embedding : K →+* adicCompletion K v :=
Expand Down Expand Up @@ -342,7 +343,7 @@ lemma isFinitePlace_iff [NumberField K] (v : AbsoluteValue K ℝ) :

namespace FinitePlace

variable [NumberField K]
variable [NumberField K] [NumberField L]

instance : FunLike (FinitePlace K) K ℝ where
coe w x := w.1 x
Expand Down Expand Up @@ -468,6 +469,24 @@ alias IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply :=
@[deprecated (since := "2026-03-11")]
alias IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm := embedding_mul_absNorm

-- todo: restate in terms of finite places once we get ramification theory for finite places
lemma equivHeightOneSpectrum_symm_apply_algebraMap
(v : HeightOneSpectrum (𝓞 K)) (w : HeightOneSpectrum (𝓞 L)) [w.1.LiesOver v.1] (x : K) :
FinitePlace.equivHeightOneSpectrum.symm w (algebraMap K L x) =
FinitePlace.equivHeightOneSpectrum.symm v x ^
(w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
by_cases hx : x = 0
· rw [hx, map_zero, map_zero, map_zero, zero_pow]
exact (mul_pos (w.asIdeal.ramificationIdx_pos (𝓞 K)) (w.asIdeal.inertiaDeg_pos (𝓞 K))).ne'
simp_rw [NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply,
FinitePlace.norm_embedding, HeightOneSpectrum.adicAbv_def]
rw [← IsDedekindDomain.HeightOneSpectrum.valuation_liesOver L v, map_pow,
Ideal.ramificationIdx'_eq_ramificationIdx v.1 w.1 v.ne_bot,
WithZeroMulInt.toNNReal_neg_apply _ (by simpa), WithZeroMulInt.toNNReal_neg_apply _ (by simpa),
← Ideal.absNorm_pow_inertiaDeg v.1 w.1]
simp only [Nat.cast_pow, NNReal.coe_zpow, ← zpow_natCast, ← zpow_mul]
grind

lemma finprod_finitePlace_pow_multiplicity {I : Ideal (𝓞 K)} (hI : I ≠ ⊥) :
∏ᶠ v : FinitePlace K, v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I := by
conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]
Expand All @@ -485,7 +504,7 @@ section LiesOver

namespace HeightOneSpectrum

variable {L : Type*} [NumberField K] [Field L] [NumberField L] [Algebra K L]
variable [NumberField K] [NumberField L]
variable (v : HeightOneSpectrum (𝓞 K)) (w : HeightOneSpectrum (𝓞 L))
variable [Algebra (v.adicCompletion K) (w.adicCompletion L)]
[ContinuousSMul (v.adicCompletion K) (w.adicCompletion L)]
Expand Down
Loading