English
There is a localization map from the monoid of powers of X in PowerSeries to LaurentSeries, exhibiting LaurentSeries as a localization of PowerSeries by powers of X.
Русский
Существует отображение локализации от моноида степеней X в PowerSeries к LaurentSeries, демонстрирующее LaurentSeries как локализацию PowerSeries по степеням X.
LaTeX
$$$\text{IsLocalization} (Submonoid.powers (PowerSeries.X))\; R⟨X⟩$$$
Lean4
/-- The localization map from power series to Laurent series. -/
@[simps (rhsMd := .all) +simpRhs]
instance of_powerSeries_localization [CommRing R] : IsLocalization (Submonoid.powers (PowerSeries.X : R⟦X⟧)) R⸨X⸩
where
map_units := by
rintro ⟨_, n, rfl⟩
refine ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩
· simp
· simp
· dsimp; rw [ofPowerSeries_X_pow]
surj
z := by
by_cases h : 0 ≤ z.order
· refine ⟨⟨PowerSeries.X ^ Int.natAbs z.order * powerSeriesPart z, 1⟩, ?_⟩
simp only [RingHom.map_one, mul_one, RingHom.map_mul, coe_algebraMap, ofPowerSeries_X_pow, Submonoid.coe_one]
rw [Int.natAbs_of_nonneg h, single_order_mul_powerSeriesPart]
· refine ⟨⟨powerSeriesPart z, PowerSeries.X ^ Int.natAbs z.order, ⟨_, rfl⟩⟩, ?_⟩
simp only [coe_algebraMap, ofPowerSeries_powerSeriesPart]
rw [mul_comm _ z]
refine congr rfl ?_
rw [ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos]
exact le_of_not_ge h
exists_of_eq
{x y} := by
rw [coe_algebraMap, ofPowerSeries_injective.eq_iff]
rintro rfl
exact ⟨1, rfl⟩
