English
If M is finitely presented over R, then the induced localization map IsLocalizedModule.map S f g is itself a localized module morphism.
Русский
Если M имеет конечную презентацию над R, то индукцированное отображение локализации IsLocalizedModule.map S f g является локализованным модуль-морфизмом.
LaTeX
$$$$ \\text{If } [\\text{Module.FinitePresentation } R M],\\; \\text{IsLocalizedModule S } (\\text{IsLocalizedModule.map } S f g). $$$$
Lean4
instance isLocalizedModule_map [Module.FinitePresentation R M] : IsLocalizedModule S (IsLocalizedModule.map S f g) :=
by
constructor
· intro s
rw [Module.End.isUnit_iff]
have := (Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := S) (f := g) s)
constructor
· exact fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)
· intro h
use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h
ext x
exact Module.End.isUnit_apply_inv_apply_of_isUnit (IsLocalizedModule.map_units (S := S) (f := g) s) (h x)
· intro h
obtain ⟨h', s, e⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (h ∘ₗ f)
refine ⟨⟨h', s⟩, ?_⟩
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
refine e.symm.trans (by ext; simp)
· intro h₁ h₂ e
apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g
ext x
simpa using LinearMap.congr_fun e (f x)
