Corresponding finite-completion maps carry local integers to local integers.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable {K : Type u} {M : Type v}
[Field K] [NumberField K] [Algebra ℚ K]
[Field M] [NumberField M] [Algebra ℚ M]Lean source · statement
theorem finitePlaceAdicCompletionCongrHom_mapsToIntegers
(e : K ≃ₐ[ℚ] M) (W : HeightOneSpectrum (𝓞 M)) :
Set.MapsTo (finitePlaceAdicCompletionCongrHom e W)
(((finitePlaceCongr e).symm W).adicCompletionIntegers K :
Set (((finitePlaceCongr e).symm W).adicCompletion K))
(W.adicCompletionIntegers M : Set (W.adicCompletion M))