localPreimage — Mathlib

English

Given a morphism f and a sieve element s, localPreimage selects a preimage of G.map g restricted to s in F.obj(op V).

Русский

Заданному отображению f и элементу сито s локальныйpreimage выбирает предобраз для G.map g ограниченного на s в F.obj(op V).

LaTeX

$$localPreimage (f) (s) (g) (hg) : ToType (F.obj (op V))$$

Lean4

/-- If a morphism `g : V ⟶ U.unop` belongs to the sieve `imageSieve f s g`, then
this is choice of a preimage of `G.map g.op s` in `F.obj (op V)`, see
`app_localPreimage`. -/
noncomputable def localPreimage {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : Cᵒᵖ} (s : ToType (G.obj U)) {V : C} (g : V ⟶ U.unop)
    (hg : imageSieve f s g) : ToType (F.obj (op V)) :=
  hg.choose

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