English
The map between LaurentSeries and powerSeries extends to an equality of subrings: the image of powerSeries_as_subring under LaurentSeries RingEquiv equals the adic completion integers subring.
Русский
Отображение powerSeries_as_subring через LaurentSeries RingEquiv равно подкольцу целых адикционного завершения.
LaTeX
$$$\\mathrm{Subring.map}\\bigl( \\mathrm{LaurentSeriesRingEquiv}\\,K\\mathrm{.toRingHom},\\; \\mathrm{powerSeries\\_as\\_subring}\\,K\\bigr) = (\\mathrm{idealX}\\,K)^{\\mathrm{adicCompletionIntegers}}(\\mathrm{RatFunc}\\,K)$$$
Lean4
theorem powerSeries_ext_subring :
Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) =
((idealX K).adicCompletionIntegers (RatFunc K)).toSubring :=
by
ext x
refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩
· simp only [ValuationSubring.mem_toSubring, ← hF, ← coe_F]
apply mem_integers_of_powerSeries
· obtain ⟨F, hF⟩ := exists_powerSeries_of_memIntegers K H
simp only [Subring.mem_map]
exact ⟨F, ⟨F, trivial, rfl⟩, hF⟩
