toAlgHomHom — Mathlib

English

There is a canonical monoid hom from the group of algebra automorphisms to the algebra endomorphisms, sending each automorphism to its underlying algebra homomorphism.

Русский

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

LaTeX

$$$ \\mathrm{toAlgHom}: (A \\cong_R A) \\to_* (A \\to_R A). $$$

Lean4

/-- `AlgEquiv.toAlgHom` as a `MonoidHom`. -/
@[simps]
def toAlgHomHom (R A) [CommSemiring R] [Semiring A] [Algebra R A] : (A ≃ₐ[R] A) →* A →ₐ[R] A
    where
  toFun := AlgEquiv.toAlgHom
  map_one' := rfl
  map_mul' _ _ := rfl

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