invApp — Mathlib

English

For an open immersion f and an open U ⊆ X, there is a canonical map invApp(U): X.presheaf(U) → Y.presheaf(op opens f(U)).

Русский

Для открытого вложения f и открытого множества U ⊆ X существует каноническое отображение invApp(U): X.presheaf(U) → Y.presheaf(op opens f(U)).

LaTeX

$$$ invApp(f, U) : X.presheaf.obj(\\mathrm{op} \uplus U) \\to Y.presheaf.obj(\\mathrm{op}(opensFunctor(f) . obj 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.1 U

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