ofHom — Mathlib

English

Given a Bialgebra hom between rings X and Y, this morphism can be regarded as a morphism in the category BialgCat R between the corresponding free/built objects.

Русский

Дано биалгебровый гомоморфизм между кольцами X и Y, и этот гомоморфизм можно рассмотреть как морфизм в категории BialgCat R между соответствующими объектами.

LaTeX

$$$\text{ofHom}(f) : \operatorname{of}~R~X \to \operatorname{of}~R~Y$$$

Lean4

/-- Typecheck a `BialgHom` as a morphism in `BialgCat R`. -/
abbrev ofHom {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (f : X →ₐc[R] Y) : of R X ⟶ of R Y :=
  ConcreteCategory.ofHom f

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