ofHom_id — Mathlib

English

Let R be a commutative ring and X an R-algebra. The morphism in AlgCat corresponding to the identity algebra hom on X is the identity morphism on the object of X in AlgCat.

Русский

Пусть R — коммутативное кольцо, X — R-алгебра. Отображение через ofHom идентитного алгебраического гомома на X даёт тождественный морфизм на объекте X в AlgCat.

LaTeX

$$$\\ operatorsname{ofHom}(\\mathrm{AlgHom.id}_R X) = \\mathbf{1}_{\\operatorname{of} R X}$$$

Lean4

@[simp]
theorem ofHom_id {X : Type v} [Ring X] [Algebra R X] : ofHom (AlgHom.id R X) = 𝟙 (of R X) :=
  rfl

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