instFullFunctor — Mathlib

English

An order-embedding f: X →o Y induces a full functor X ⥤ Y, i.e., every morphism between f(a) and f(b) in Y comes from a morphism a → b in X.

Русский

Вложение порядка f: X →o Y порождает полный функтор X ⥤ Y: каждое отображение f(a) ⟶ f(b) в Y имеет прообраз в виде отображения a ⟶ b в X.

LaTeX

$$$\forall a,b\in X,\; \forall g:\mathrm{Hom}_{Y}(f(a),f(b)),\; \exists h:\mathrm{Hom}_{X}(a,b),\; f(h)=g.$$$

Lean4

instance (f : X ↪o Y) : f.monotone.functor.Full where map_surjective h := ⟨homOfLE (f.map_rel_iff.1 h.le), rfl⟩

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