instConcreteCategoryRingHomCarrier

English

There is a concrete category structure on a carrier that turns ring homs into morphisms.

Русский

Существует конкретная структура категории на носителе, превращающая кольцевые гомоморфизмы в морфизмы.

LaTeX

$$$ \text{ConcreteCategory.Carrier: RingHom } \Rightarrow \text{Hom} \text{ objects }$$$

Lean4

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

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