inv_invApp — Mathlib

English

The inverse of invApp corresponds to the c-morphism and presheaf map as shown by a specific equality.

Русский

Обратное к invApp соответствует картам c и отображениям пресшеаф по конкретному равенству.

LaTeX

$$$\mathrm{inv}(\mathrm{invApp}\ f\ U) = f.c.app( op( opensFunctor f ).obj U ) \circ X.presheaf.map( eqToHom ( ... ) ).$$$

Lean4

theorem inv_invApp (U : Opens X) :
    inv (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.inv_invApp f U

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