English
If there is a linear map f : A →ₗ[R] B preserving 1 and for a fixed r the element algebraMap R A r is invertible, then algebraMap R B r is invertible with inverse given by f applied to the inverse in A, i.e., invOf = f( (algebraMap R A r)^{-1} ).
Русский
Если существует линейное отображение f:A→ₗ[R] B, сохраняющее 1, и для некоторого r элемент algebraMap R A r обратим, то algebraMap R B r также обратим, причём обратное равно f( (algebraMap R A r)^{-1} ).
LaTeX
$$$\\text{If } f:A\\to B,\\ f(1)=1,\\ h: \\operatorname{Invertible}(\\alpha_r) \\text{ with } \\alpha_r=\\operatorname{algebraMap}_{A}(r),\\ text{ then } \\operatorname{algebraMap}_{B}(r) \\text{ is invertible with } invOf = f(\\alpha_r^{-1}).$$$
Lean4
/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
invertible when `algebraMap R A r` is. -/
abbrev algebraMapOfInvertibleAlgebraMap (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : Invertible (algebraMap R A r)) :
Invertible (algebraMap R B r) where
invOf := f ⅟(algebraMap R A r)
invOf_mul_self := by rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]
mul_invOf_self := by rw [← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]
