ofHom — Mathlib

English

Type-checking a RingHom as a morphism in CommRingCat is formalized by the construction of ofHom; hence any RingHom f: R → S induces a morphism of CommRingCat from of R to of S.

Русский

Пусть f: R → S — RingHom. Тогда он порождает морфизм CommRingCat от of R к of S через конструктор ofHom.

LaTeX

$$$f:\; R \to S \; (\text{RingHom}) \Rightarrow\; \mathrm{of}(f): \mathrm{of}R \to \mathrm{of}S \text{ в CommRingCat}$$$

Lean4

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

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