instConcreteCategoryRingHomCarrier

English

There is a canonical concrete category structure on RingCat, where objects are rings and morphisms are RingHom, taken with their carrier functions as the underlying maps.

Русский

Существует каноническая структура конкретной категории на RingCat: объекты — кольца, морфизмы — RingHom, а отображения на носителях — её фундаментальные функции.

LaTeX

$$$ \text{RingCat is a ConcreteCategory }(\text{fun } R S \Rightarrow R \to+* S),\ \text{hom} := \mathrm{Hom.hom}',\ \text{ofHom } f := ⟨f⟩. $$$

Lean4

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

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