ofHom — Mathlib

English

Typecheck an AlgHom as a morphism in AlgCat; the morphism corresponds to the original AlgHom on carriers.

Русский

Проверка типа AlgHom как морфизма в AlgCat; получившийся морфизм соответствует исходному AlgHom на носителях.

LaTeX

$$ofHom f : A ⟶ B$$

Lean4

/-- Typecheck an `AlgHom` as a morphism in `AlgCat`. -/
abbrev ofHom {A B : Type v} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : of R A ⟶ of R B :=
  ConcreteCategory.ofHom (C := AlgCat R) f

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