English
For an immersion f and an open U in f.coborderRange, the preimage of U under liftCoborder equals the preimage under f of the image of U under the inclusion ι.
Русский
Для вложения f и открытого множества U в coborderRange f предобраз liftCoborder совпадает с предобразом через f образа U под включением ι.
LaTeX
$$$f.liftCoborder^{-1}U = f^{-1}(\\,f.coborderRange.ι ''ᵁ U\\,)$$$
Lean4
theorem liftCoborder_app [IsImmersion f] (U : f.coborderRange.toScheme.Opens) :
f.liftCoborder.app U = f.app (f.coborderRange.ι ''ᵁ U) ≫ X.presheaf.map (eqToHom <| f.liftCoborder_preimage U).op :=
by
rw [Scheme.congr_app (f.liftCoborder_ι).symm (f.coborderRange.ι ''ᵁ U)]
simp [Scheme.app_eq f.liftCoborder (f.coborderRange.ι.preimage_image_eq U), ← Functor.map_comp_assoc,
-Functor.map_comp, Subsingleton.elim _ (𝟙 _)]
