ofHom — Mathlib

English

There is a canonical morphism in RingCat corresponding to a RingHom f: R →+* S, namely ofHom f.

Русский

Существует канонический морфизм в RingCat, соответствующий RingHom f: R →+* S, именно ofHom f.

LaTeX

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

Lean4

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

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