English
Let S be a submonoid of a commutative semiring R, and f: M → M' and g: M → M'' be R-linear maps with M, M', M'' additive commutative monoids. If M, M', M'' are localized along S via f and g, then the induced linear equivalence between the localizations satisfies (linearEquiv S f g)(f x) = g x for all x in M.
Русский
Пусть S—подмоноид относительно кольца R, и f: M → M', g: M → M'' — R-линейные отображения. Если M, M', M'' локализованы вдоль S через f и g, то полученное линейное эквивалентное отображение локализаций удовлетворяет (linearEquiv S f g)(f x) = g x для всех x ∈ M.
LaTeX
$$$\\forall x \\in M:\\ (\\mathrm{linearEquiv}\\ S\\ f\\ g)(f\\,x) = g\\,x$$$
Lean4
@[simp]
theorem linearEquiv_apply [IsLocalizedModule S g] (x : M) : (linearEquiv S f g) (f x) = g x := by simp [linearEquiv]
