app_invApp' — Mathlib

English

A variant of the naturality statement for the inverse of appIso, expressed with a direct equality using op maps and preimage-image equalities: (f.appIso U).hom = ... (some expression).ge

Русский

Вариант натуральности для обратной части appIso, выраженный через равенство и свойства предобраз-в-image: (f.appIso U).hom = ... .ge

LaTeX

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

Lean4

/-- A variant of `app_invApp` that gives an `eqToHom` instead of `homOfLE`. -/
@[reassoc]
theorem app_invApp' (U) (hU : U ≤ f.opensRange) :
    f.app U ≫ (f.appIso (f ⁻¹ᵁ U)).inv =
      Y.presheaf.map (eqToHom (Opens.ext <| by simpa [Set.image_preimage_eq_inter_range])).op :=
  PresheafedSpace.IsOpenImmersion.app_invApp _ _

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