eval — Mathlib

English

Define eval for a presheaf P on Type: map an element s: P.obj(op α) and x: α to P.obj(op PUnit) via P.map.

Русский

Определяем отображение eval для пресейфа P на Type: переводим элемент s: P.obj(op α) и x: α в P.obj(op PUnit) через P.map.

LaTeX

$$$ \\text{eval}(P,α,s,x) = P.map(\\uparrow(\\lambda _ . x)).op(s) $$$

Lean4

/-- Given a presheaf `P` on the category of types, construct
a map `P(α) → (α → P(*))` for all type `α`. -/
def eval (P : Type uᵒᵖ ⥤ Type u) (α : Type u) (s : P.obj (op α)) (x : α) : P.obj (op PUnit) :=
  P.map (↾fun _ => x).op s

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