ofHom — Mathlib

English

There is a canonical way to regard a linear coalgebra hom f: X →ₗc[R] Y as a morphism in CoalgCat R from the object of X to the object of Y.

Русский

Существуют канонические преобразования линейных коалгебрных гомоморфизмов f: X →ₗc[R] Y в морфизмы CoalgCat R от объекта X к объекту Y.

LaTeX

$$$\\text{ofHom} : (X \\to_{\\ell c[R]} Y) \\to (\\text{of } R X \\to \\text{of } R Y)$$$

Lean4

/-- Typecheck a `CoalgHom` as a morphism in `CoalgCat R`. -/
abbrev ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y]
    (f : X →ₗc[R] Y) : of R X ⟶ of R Y :=
  ConcreteCategory.ofHom f

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