English
For a submodule M′ of M, the localized version M′ toLocalized₀ p f carries a canonical localized module structure with respect to the localization p of R and the linear map f: M → N; i.e., M′ toLocalized₀ p f is a localized R-module.
Русский
Для подмодуля M′ под M локализация M′ toLocalized₀ p f обладает канонической структурой локализованного модуля по отношению к локализации p кольца R и линейному отображению f: M → N; т.е. M′ toLocalized₀ p f является локализованным модулем над R.
LaTeX
$$$\text{IsLocalizedModule } p\, (M'.\mathrm{toLocalized}_0(p,f) )$$$
Lean4
instance : IsLocalizedModule p (M'.toLocalized₀ p f)
where
map_units
x := by
simp_rw [Module.End.isUnit_iff]
constructor
· exact fun _ _ e ↦ Subtype.ext (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))
· rintro ⟨_, m, hm, s, rfl⟩
refine ⟨⟨IsLocalizedModule.mk' f m (s * x), ⟨_, hm, _, rfl⟩⟩, Subtype.ext ?_⟩
rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower, ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def,
IsLocalizedModule.mk'_cancel_right]
surj := by
rintro ⟨y, x, hx, s, rfl⟩
exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩
exists_of_eq
e := by simpa [Subtype.ext_iff] using IsLocalizedModule.exists_of_eq (S := p) (f := f) (congr_arg Subtype.val e)
