English
The universal linear equivalence between two localized modules is given by the composition of their isomorphisms.
Русский
Универсальное линейное эквивалентность между двумя локализованными модулями задана композицией их изоморфизмов.
LaTeX
$$$$ \mathrm{IsLocalizedModule.linearEquiv}(S,f,g) = (\mathrm{iso}~S~f)^{-1} \circ \mathrm{iso}~S~g. $$$$
Lean4
theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) (l : M' →ₗ[R] M'')
(hl : l.comp f = g) : lift S f g h = l :=
by
dsimp only [IsLocalizedModule.lift]
rw [LocalizedModule.lift_unique S g h (l.comp (iso S f).toLinearMap), LinearMap.comp_assoc, LinearEquiv.comp_coe,
LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, LinearMap.comp_id]
rw [LinearMap.comp_assoc, ← hl]
ext x
simp
