English
If f is localized, then composing f with a linear equivalence e yields a localized map; this induced is a new IsLocalizedModule instance for the composition.
Русский
Если f локализовано, то композиция с линейным эквалентом e даёт локализованное отображение; получается новый экземпляр IsLocalizedModule для композиции.
LaTeX
$$$[IsLocalizedModule\\; S\\; f] \\Rightarrow [IsLocalizedModule\\; S\\; (f \\circ e)].$$$
Lean4
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible and
`l` is another linear map `LocalizedModule S M ⟶ M''` such that `l ∘ mkLinearMap = g` then
`l = lift g`
-/
theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
(l : LocalizedModule S M →ₗ[R] M'') (hl : l.comp (LocalizedModule.mkLinearMap S M) = g) :
LocalizedModule.lift S g h = l := by
ext x;
induction x with
| _ m s
rw [LocalizedModule.lift_mk]
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp, Function.comp_apply,
LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_mk]
congr 1; rw [LocalizedModule.mk_eq]
refine ⟨1, ?_⟩; simp only [one_smul, Submonoid.smul_def]
