app_appIso_inv — Mathlib

English

Reiterating the explicit expression for the forward map of the isomorphism appIso: (f.appIso U).hom = f.app (f''ᵁ U) ∘ X.presheaf.map (eqToHom (preimage_image_eq f U).symm).op.

Русский

Повторяем явное выражение для горизонтального гомоморфизма: (f.appIso U).hom = f.app (f''ᵁ U) ∘ X.presheaf.map (eqToHom (preimage_image_eq f U).symm).op.

LaTeX

$$$$ (f.appIso U).hom = f.app (f''^\!U) \circ X.presheaf.map (eqToHom (preimage_image_eq f U).symm).op $$$$

Lean4

@[reassoc (attr := simp)]
theorem app_appIso_inv (U) :
    f.app U ≫ (f.appIso (f ⁻¹ᵁ U)).inv = Y.presheaf.map (homOfLE (Set.image_preimage_subset f.base U.1)).op :=
  PresheafedSpace.IsOpenImmersion.app_invApp _ _

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