app_invApp — Mathlib

English

Relates invApp with the action of the maps on opens and presheaves via app_invApp.

Русский

Связь invApp с действием отображений на открытых множествах и пресхиве через app_invApp.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem app_invApp (U : Opens Y) :
    f.c.app (op U) ≫ H.invApp _ ((Opens.map f.base).obj U) =
      Y.presheaf.map
        ((homOfLE (Set.image_preimage_subset f.base U.1)).op :
          op U ⟶ op (opensFunctor f |>.obj ((Opens.map f.base).obj U))) :=
  PresheafedSpace.IsOpenImmersion.app_invApp f.1 U

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