English
The canonical map from K to the finite adeles is implemented as a ring hom, factoring through evaluation at every place with finiteness of support.
Русский
Каноническое отображение из K в конечные адели реализуется как кольцо-гомоморфизм, учитывающее каждое место и конечную опору.
LaTeX
$$protected def algebraMap : K →+* FiniteAdeleRing R K$$
Lean4
/-- The canonical map from `K` to the finite adeles of `K`.
The content of the existence of this map is the fact that an element `k` of `K` is integral at
all but finitely many places, which is `IsDedekindDomain.HeightOneSpectrum.Support.finite R k`.
-/
protected def algebraMap : K →+* FiniteAdeleRing R K
where
toFun
k :=
⟨fun i ↦ k,
by
simp only [Filter.eventually_cofinite, SetLike.mem_coe, mem_adicCompletionIntegers R K, adicCompletion,
Valued.valuedCompletion_apply, not_le]
exact HeightOneSpectrum.Support.finite R k⟩
map_one' := rfl
map_mul' x
y := Subtype.eq <| funext (fun v ↦ UniformSpace.Completion.coe_mul ((WithVal.equiv (valuation K v)).symm x) y)
map_zero' := rfl
map_add' x
y := Subtype.eq <| funext (fun v ↦ UniformSpace.Completion.coe_add ((WithVal.equiv (valuation K v)).symm x) y)
