inv_invApp — Mathlib

English

The inverse of the invApp map composes with f.c.app to give a canonical expression in terms of Y and X presheaves.

Русский

Обратное к карте invApp при композиции с f.c.app даёт каноническое выражение через пред sheaf.

LaTeX

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

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.1 U

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