lift_mk — Mathlib

English

If f: M →ₗ[A] N is localized over S, then f is localized over the algebra map submonoid AlgAlgebraSubmonoid(A,S).

Русский

Если отображение f: M →ₗ[A] N локализуется над S, тогда f локализуется и над подмонойдом алгебраического отображения A и S.

LaTeX

$$$\\text{IsLocalizedModule}(S, f) \\Rightarrow \\text{IsLocalizedModule}(\\mathrm{Algebra.algebraMapSubmonoid}(A,S), f).$$$

Lean4

/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
`lift g m s = s⁻¹ • g m`.
-/
theorem lift_mk (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit (algebraMap R (Module.End R M'') x)) (m : M) (s : S) :
    LocalizedModule.lift S g h (LocalizedModule.mk m s) = (h s).unit⁻¹.val (g m) :=
  rfl

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