English
If g: M0 → M1 is linear, then the induced map between localized modules sends LocalizedModule.mk m s to LocalizedModule.mk (g m) s.
Русский
Учитывая линейное отображение g: M0 → M1, полученная карта между локализованными модулями отправляет LocalizedModule.mk m s в LocalizedModule.mk (g m) s.
LaTeX
$$$$ \\text{map } S\; (mkLinearMap S M_0) (mkLinearMap S M_1)\\; g\\; (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s $$$$
Lean4
/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[R] Nₛ`. -/
noncomputable def map : (M →ₗ[R] N) →ₗ[R] (M' →ₗ[R] N')
where
toFun h := lift S f (g ∘ₗ h) (IsLocalizedModule.map_units g)
map_add' h₁
h₂ := by
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
simp only [lift_comp, LinearMap.add_comp, LinearMap.comp_add]
map_smul' r
h := by
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
simp only [lift_comp, LinearMap.smul_comp, LinearMap.comp_smul, RingHom.id_apply]
