English
If e: M'' ≃ M is a linear equivalence and f is localized, then f∘e is localized.
Русский
Если e: M'' ≃ M линейное эквалентное отображение и f локализовано, то f∘e локализовано.
LaTeX
$$$[IsLocalizedModule\\, S\\, f] \\Rightarrow [IsLocalizedModule\\, S\\ (f\\circ e)].$$$
Lean4
instance of_linearEquiv (e : M' ≃ₗ[R] M'') [hf : IsLocalizedModule S f] : IsLocalizedModule S (e ∘ₗ f : M →ₗ[R] M'')
where
map_units
s :=
by
rw [show algebraMap R (Module.End R M'') s = e ∘ₗ (algebraMap R (Module.End R M') s) ∘ₗ e.symm by ext; simp,
Module.End.isUnit_iff, LinearMap.coe_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, LinearEquiv.coe_coe,
EquivLike.comp_bijective, EquivLike.bijective_comp]
exact (Module.End.isUnit_iff _).mp <| hf.map_units s
surj
x := by
obtain ⟨p, h⟩ := hf.surj (e.symm x)
exact
⟨p, by
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h, Submonoid.smul_def,
Submonoid.smul_def, LinearEquiv.map_smul, LinearEquiv.apply_symm_apply]⟩
exists_of_eq
h :=
by
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] at h
exact hf.exists_of_eq h
