of_linearEquiv_right — Mathlib

English

If e: M' ≃ M'' is a linear equivalence and f is localized, then e∘f is localized.

Русский

Если e: M' ≃ M'' линейное эквалентное отображение и f локализовано, то e∘f локализовано.

LaTeX

$$$[IsLocalizedModule\\, S\\, f] \\Rightarrow [IsLocalizedModule\\, S\\ (e\\circ f)].$$$

Lean4

instance of_linearEquiv_right (e : M'' ≃ₗ[R] M) [hf : IsLocalizedModule S f] :
    IsLocalizedModule S (f ∘ₗ e : M'' →ₗ[R] M')
    where
  map_units s := hf.map_units s
  surj
    x := by
    obtain ⟨⟨p, s⟩, h⟩ := hf.surj x
    exact ⟨⟨e.symm p, s⟩, by simpa using h⟩
  exists_of_eq
    h := by
    simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] at h
    obtain ⟨c, hc⟩ := hf.exists_of_eq h
    exact ⟨c, by simpa only [Submonoid.smul_def, map_smul, e.symm_apply_apply] using congr(e.symm $hc)⟩

Похожие утверждения