toLinearMapHom — Mathlib

English

There is a natural monoid hom from AlgEquiv toLinearMap by composing toAlgHomHom with the linear map construction, yielding a monoid hom into module endomorphisms.

Русский

Существует естественная моноидальная гомоморфия от AlgEquiv кToLinearMap, получаемая композицией toAlgHomHom и линейного отображения, показывающая переход к модуля-конечному отображению.

LaTeX

$$$ (\\mathrm{AlgEquiv R A A}) \\to_* (\\mathrm{Module.End} \\; R \\; A). $$$

Lean4

/-- `AlgEquiv.toLinearMap` as a `MonoidHom`. -/
@[simps!]
def toLinearMapHom (R A) [CommSemiring R] [Semiring A] [Algebra R A] : (A ≃ₐ[R] A) →* Module.End R A :=
  AlgHom.toEnd.comp (toAlgHomHom R A)

Похожие утверждения