English
Let R, S, M be as above with the stated module and algebra structures. If x ∈ R determines a unit endomorphism in End_S(M) via the map algebraMap R (End_S M), i.e. algebraMap R (End_S M) x is a unit, then for all m, m' ∈ M, the inverse of that endomorphism applied to m equals m' if and only if m equals x acting on m'.
Русский
Пусть R, S, M удовлетворяют условиям и соответствуют заданной структуре модуля. Пусть элемент x ∈ R задаёт единичный преобразователь в End_S(M) через отображение algebraMap R (End_S M), то есть algebraMap R (End_S M) x является единицей. Тогда для всех m, m' ∈ M выполнено: inv(end)(m) = m' тогда и только тогда, когда m = x · m'.
LaTeX
$$$\forall x\in R,\;\text{If }\;\mathrm{algebraMap}_{R}(\mathrm{Module.End}_{S} M)(x)\ \text{is a unit in }\mathrm{End}_{S}(M),\;\big( (\mathrm{algebraMap}_{R}(\mathrm{Module.End}_{S} M)(x))^{-1} m = m' \big) \iff m = x \cdot m'. $$$
Lean4
theorem algebraMap_isUnit_inv_apply_eq_iff {x : R} (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
(↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m'
where
mp H := H ▸ (isUnit_apply_inv_apply_of_isUnit h m).symm
mpr
H :=
H.symm ▸ by
apply_fun ⇑h.unit.val using ((isUnit_iff _).mp h).injective
simpa using Module.End.isUnit_apply_inv_apply_of_isUnit h (x • m')
