English
If there exists a linear map f preserving 1, then IsUnit(algebraMap_R_B(r)) whenever IsUnit(algebraMap_R_A(r)). In particular, units are preserved from A to B under such a map.
Русский
Если существует линейное отображение, сохраняющее единицу, то элемент algebraMap_R_B(r) является единицей, если algebraMap_R_A(r) — единица; т.е. единицы в A переходят в единицы в B под таким отображением.
LaTeX
$$$\\text{If } f(1)=1,\\quad \\text{then } IsUnit(\\operatorname{algebraMap}_R^B(r))\\text{ whenever } IsUnit(\\operatorname{algebraMap}_R^A(r)).$$$
Lean4
/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
a unit when `algebraMap R A r` is. -/
theorem algebraMap_of_algebraMap (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : IsUnit (algebraMap R A r)) :
IsUnit (algebraMap R B r) :=
let ⟨i⟩ := nonempty_invertible h
letI := Invertible.algebraMapOfInvertibleAlgebraMap f hf i
isUnit_of_invertible _
