algebraMap_eq_inlRingHom_comp — Mathlib

English

Compatibility relations ensure functorial behavior of Unitization under algebra maps.

Русский

Совместимости обеспечивают функториальное поведение Unitization при алгебраических отображениях.

LaTeX

$$$\mathrm{inlRingHom}(R,A) \circ \mathrm{algebraMap}_S^R = \mathrm{algebraMap}_S^{Unitization(R,A)}$$$

Lean4

theorem algebraMap_eq_inlRingHom_comp : algebraMap S (Unitization R A) = (inlRingHom R A).comp (algebraMap S R) :=
  rfl

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