English
The finite adele ring carries a canonical Algebra structure over the base Dedekind domain, obtained by composing with the base algebra map.
Русский
У конечного адела на базе Дедекдина существует каноническая структура Algebra над базовым Дедекдиновым доменом, получаемая композицией с алгебраической отображением.
LaTeX
$$instance : Algebra R (IsDedekindDomain.FiniteAdeleRing R K) := (IsDedekindDomain.FiniteAdeleRing.algebraMap R K).toAlgebra$$
Lean4
/-- If `p` is a maximal ideal, then the lift of `p` in an extension is the product of the primes
over `p` to the power the ramification index.
-/
theorem map_algebraMap_eq_finset_prod_pow {p : Ideal S} [p.IsMaximal] (hp : p ≠ 0) :
map (algebraMap S R) p = ∏ P ∈ p.primesOver R, P ^ p.ramificationIdx (algebraMap S R) P := by
classical
have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} := (finite_factors h).fintype
rw [finprod_eq_finset_prod_of_mulSupport_subset (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ←
Finset.prod_set_coe, ← Finset.prod_set_coe]
· let _ : Fintype { v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p } := hF
refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
simp [maxPowDividing_eq_pow_multiset_count _ h, ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]
· intro v hv
simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv
