ofHom — Mathlib

English

Typecheck a BialgHom as a morphism in HopfAlgCat R: given f : X →ₐc[R] Y, there is a corresponding morphism in HopfAlgCat from of R X to of R Y.

Русский

Типизация BialgHom как морфизма в HopfAlgCat R: если f : X →ₐc[R] Y, существует соответствующий морфизм в HopfAlgCat от of R X к of R Y.

LaTeX

$$$\mathrm{ofHom} : BialgHom R X Y \to \mathrm{HopfAlgCat R} (\mathrm{of} R X) (\mathrm{of} R Y)$$$

Lean4

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

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