pullback — Mathlib

English

A morphism f: X → Y with pullbacks defines a functor pullback f: Subobject Y ⥤ Subobject X, pulling back subobjects along f.

Русский

Гомоморфизм f: X → Y, имеющий пары вытягиваний, задаёт канонический функтор pullback f: Subobject Y ⥤ Subobject X, тянущий подобъекты вдоль f.

LaTeX

$$$\text{pullback}(f): \mathrm{Subobject}(Y) \to \mathrm{Subobject}(X)$ is a functor.$$

Lean4

/-- When `C` has pullbacks, a morphism `f : X ⟶ Y` induces a functor `Subobject Y ⥤ Subobject X`,
by pulling back a monomorphism along `f`. -/
def pullback (f : X ⟶ Y) : Subobject Y ⥤ Subobject X :=
  lower (MonoOver.pullback f)

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