inv_invApp — Mathlib

English

The inverse of the restriction inverse app equals the c-component composed with a presheaf map.

Русский

Обратное ограниченного invApp соответствует композиции с c-компонентом и отображением на предшехе.

LaTeX

$$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]))$$

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])) :=
  by
  rw [← cancel_epi (H.invApp _ U), IsIso.hom_inv_id]
  delta invApp
  simp [← Functor.map_comp]

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