ofHom — Mathlib

English

Let R and S be semirings. For any ring hom f: R →+* S, there is a corresponding morphism in the category of semirings from the object of R to the object of S, given by the construction of ofHom f.

Русский

Пусть R и S — полукольца. Для любого кольмхома f: R →+* S существует соответствующий морфизм в категории полукольц от объекта R к объекту S, задаваемый конструктором ofHom f.

LaTeX

$$$ (\mathrm{ofHom}(f)) : \mathrm{of}(R) \to \mathrm{of}(S). $$$

Lean4

/-- Typecheck a `RingHom` as a morphism in `SemiRingCat`. -/
abbrev ofHom {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) : of R ⟶ of S :=
  ConcreteCategory.ofHom (C := SemiRingCat) f

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