appIso_hom — Mathlib

English

The forward component of the AppIso is the canonical map on sections along the open immersion; more precisely, (f.appIso U).hom = f.app (f''ᵁ U) ∘ X.presheaf.map (eqToHom (preimage_image_eq f U).symm).op.

Русский

Первая компонента изоморфизма AppIso есть канонический морфизм секций вдоль открытого вложения; точнее, (f.appIso U).hom = f.app (f''ᵁ U) ∘ X.presheaf.map (eqToHom (preimage_image_eq f U).symm).op.

LaTeX

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

Lean4

theorem appIso_hom (U) :
    (f.appIso U).hom = f.app (f ''ᵁ U) ≫ X.presheaf.map (eqToHom (preimage_image_eq f U).symm).op :=
  (PresheafedSpace.IsOpenImmersion.inv_invApp f.toPshHom U).trans (by rw [eqToHom_op])

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