instConcreteCategoryAlgHomCarrier

English

There is a concrete category structure on the category of R-algebras, with Hom-sets given by AlgHom between carrier algebras.

Русский

Существует конкретная структура категории AlgCat над R-алгебрами, где множество морфизмов между X и Y соответствует множеству AlgHom между носителями X и Y.

LaTeX

$$$\mathrm{Hom}_{\mathrm{AlgCat}(R)}(X,Y) = \mathrm{AlgHom}(R, X_{carrier}, Y_{carrier})$$$

Lean4

instance : ConcreteCategory (AlgCat.{v} R) (· →ₐ[R] ·)
    where
  hom := Hom.hom'
  ofHom := Hom.mk

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