fromLocalizedModule_mk — Mathlib

English

On basic representatives, the canonical map sends the class of m localized at s to the inverse unit applied to f(m).

Русский

На базовых представителях каноническое отображение отправляет класс m локализованный по s в инвертированную единицу, применённую к f(m).

LaTeX

$$$$ \mathrm{fromLocalizedModule}(\mathrm{LocalizedModule.mk}(m,s)) = (\mathrm{map\_units} f s)^{-1}(f(m)). $$$$

Lean4

theorem fromLocalizedModule_mk (m : M) (s : S) :
    fromLocalizedModule S f (LocalizedModule.mk m s) = (IsLocalizedModule.map_units f s).unit⁻¹.val (f m) :=
  rfl

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