functor — Mathlib

English

A functor between preorder categories is monotone on objects: if x ≤ x' in X, then F.obj x ≤ F.obj x' in Y.

Русский

Функтор между категориями, индукованными предреядными множествами, монотонно отображает элементы: если x ≤ x' в X, то F(x) ≤ F(x') в Y.

LaTeX

$$$\forall x,x'\in X\, (x \le x' )\Rightarrow F(x) \le F(x').$$$

Lean4

/-- A monotone function between preorders induces a functor between the associated categories. -/
def functor {f : X → Y} (h : Monotone f) : X ⥤ Y where
  obj := f
  map g := CategoryTheory.homOfLE (h g.le)

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