fromLocalizedModule'_mk — Mathlib

English

In the localization framework, the representative class [m,s] maps under the canonical map to the image of f(m) acted on by the inverse of the unit associated to s. Concretely, the class of (m localized at s) is sent to (map_units f s)^{-1}(f(m)).

Русский

В рамках локализации элемент [m,s] переходит через каноническое отображение в образ f(m), умноженный на обратное к единству, соответствующему s; то есть отображение отправляет [m,s] в (map_units f s)^{-1}(f(m)).

LaTeX

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

Lean4

@[simp]
theorem fromLocalizedModule'_mk (m : M) (s : S) :
    fromLocalizedModule' S f (LocalizedModule.mk m s) = (IsLocalizedModule.map_units f s).unit⁻¹.val (f m) :=
  rfl

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