val_awayMap — Mathlib

English

In homogeneous localization, the value of awayMap matches the Localization.awayLift expression, reflecting the canonical lifting of values through the localization.

Русский

В однородной локализации значение awayMap совпадает с выражением Localization.awayLift, отражающим каноническое поднятие значений через локализацию.

LaTeX

$$$(awayMap 𝒜 hg hx a).val = \\mathrm{Localization.awayLift}(\\text{algebraMap } A \\_, \\_, \\text{isUnit_of_dvd_unit} (map_dvd _ ⟨_, hx⟩) (\\mathrm{IsLocalization.Away.algebraMap_isUnit } x))\, a$.val$$

Lean4

theorem val_awayMap (a) :
    (awayMap 𝒜 hg hx a).val =
      Localization.awayLift (algebraMap A _) _
        (isUnit_of_dvd_unit (map_dvd _ ⟨_, hx⟩) (IsLocalization.Away.algebraMap_isUnit x)) a.val :=
  by
  rw [val_awayMap_eq_aux]
  rfl

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