invApp — Mathlib

English

For an open immersion f and X, Y, invApp assigns a morphism X.presheaf.obj(op U) → Y.presheaf.obj(op (opensFunctor f).obj U).

Русский

Для открытого вложения f и X, Y invApp задаёт морфизм X.presheaf.obj(op U) → Y.presheaf.obj(op (opensFunctor f).obj U).

LaTeX

$$$\text{invApp} : (U:\mathrm{Opens}(X)) \to X.presheaf(U) \to Y.presheaf(op( opensFunctor f(U))).$$$

Lean4

/-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`. -/
noncomputable def invApp (U : Opens X) : X.presheaf.obj (op U) ⟶ Y.presheaf.obj (op (opensFunctor f |>.obj U)) :=
  PresheafedSpace.IsOpenImmersion.invApp f U

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