isLocalizedModule_id — Mathlib

English

The identity linear map id: M → M is localized with respect to any S and any M.

Русский

Единичное отображение id: M → M локализуется относительно любого S и любого M.

LaTeX

$$$[IsLocalizedModule S (\\mathrm{id})]$$$

Lean4

theorem isLocalizedModule_id (R') [CommSemiring R'] [Algebra R R'] [IsLocalization S R'] [Module R' M]
    [IsScalarTower R R' M] : IsLocalizedModule S (.id : M →ₗ[R] M)
    where
  map_units s := by rw [← (Algebra.lsmul R (A := R') R M).commutes]; exact (IsLocalization.map_units R' s).map _
  surj m := ⟨(m, 1), one_smul _ _⟩
  exists_of_eq h := ⟨1, congr_arg _ h⟩

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