invApp_app — Mathlib

English

For an open immersion f and U open in X, app_invApp gives the equality between the composed app and the map on presheaves.

Русский

Для открытого вложения f и открытого U в X выполняется равенство между составленными app_invApp и отображением на пресхиве.

LaTeX

$$$ f.c.app(op U) ≫ H.invApp _ (opensFunctor f obj U) = Y.presheaf.map( eqToHom(⋯) ) $$$

Lean4

@[reassoc (attr := simp)]
theorem invApp_app (U : Opens X) :
    H.invApp _ U ≫ f.c.app (op (opensFunctor f |>.obj U)) =
      X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective])) :=
  PresheafedSpace.IsOpenImmersion.invApp_app f.1 U

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