English
The linear map underlying the AlgHom obtained from a linear map f is f itself: toLinearMap (ofLinearMap f map_one map_mul) = f.
Русский
Линейное отображение, содержащееся в AlgHom, полученном из линейного отображения f, равно самому f.
LaTeX
$$$$\mathrm{toLinearMap}(\mathrm{ofLinearMap}\ f\ map\_one\ map\_mul) = f.$$$$
Lean4
/-- Promote a `LinearMap` to an `AlgHom` by supplying proofs about the behavior on `1` and `*`. -/
@[simps]
def ofLinearMap (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ x y, f (x * y) = f x * f y) : A →ₐ[R] B :=
{ f.toAddMonoidHom with
toFun := f
map_one' := map_one
map_mul' := map_mul
commutes' c := by simp only [Algebra.algebraMap_eq_smul_one, f.map_smul, map_one] }
