instConcreteCategoryRingHomCarrier

English

The category CommRingCat is equipped with a concrete realization: objects are commutative rings, and morphisms are ring homomorphisms between their carriers; in particular, there is a canonical underlying ring homomorphism associated to each morphism.

Русский

Категория CommRingCat имеет конкретное представление: объекты — коммутативные кольца, морфизмы — гомоморфизмы колец между носителями; при этом каждому морфизму соответствует канонический исходный гомоморфизм между носителями.

LaTeX

$$$\text{CommRingCat}$ is a concrete category with objects = commutative rings and morphisms = ring homomorphisms on carriers.$$

Lean4

instance : ConcreteCategory.{u} CommRingCat (fun R S => R →+* S)
    where
  hom := Hom.hom'
  ofHom f := ⟨f⟩

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