English
Let f be a localization map and g a monoid-with-zero homomorphism satisfying hg for all y in S. Then for every x, the lifted map satisfies a specific explicit formula: f.lift₀ g hg x = g((f.sec x).1) · (IsUnit.liftRight (g.restrict S) hg (f.sec x).2)^{-1}.
Русский
Пусть f — локализационная карта, g — гомоморфизм моноида с единицей, удовлетворяющий hg для всех y ∈ S. Тогда для каждого x сущности лифтинга выполняется явная формула: f.lift₀ g hg x = g((f.sec x).1) · (IsUnit.liftRight (g.restrict S) hg (f.sec x).2)^{-1}.
LaTeX
$$$f.lift_0\,g\,hg\,x = g\bigl(f.sec\,x\bigr)\!\_\{1\} \cdot \bigl(\text{IsUnit.liftRight}(g.restrict S)\,hg\,(f.sec x).\text{2}\bigr)^{-1}$$$
Lean4
theorem lift₀_apply (f : LocalizationMap S N) (g : M →*₀ P) (hg : ∀ y : S, IsUnit (g y)) (x) :
f.lift₀ g hg x = g (f.sec x).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec x).2)⁻¹ :=
rfl
