ofHom — Mathlib

English

There is a canonical morphism in CommAlgCat corresponding to any R-algebra hom f: X →ₐ[R] Y; this morphism is the embedding of f into the morphism-set of CommAlgCat.

Русский

Существует каноническое отображение в CommAlgCat, соответствующее любому гомоморфизму R-алгебры f: X →ₐ[R] Y; это отображение в множестве мореморизмов CommAlgCat.

LaTeX

$$$\mathrm{ofHom} (f) : \mathrm{of\, R\, X} \to \mathrm{of\, R\, Y}$$$

Lean4

/-- Typecheck an `AlgHom` as a morphism in `CommAlgCat`. -/
abbrev ofHom (f : X →ₐ[R] Y) : of R X ⟶ of R Y :=
  ConcreteCategory.ofHom (C := CommAlgCat R) f

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