English
A variant of app_invApp gives an eqToHom version of the identity: f.app U ≫ (f.appIso (f ⁻¹ᵁ U)).inv = Y.presheaf.map (eqToHom (Opens.ext ...)).op, i.e. the inverse-app composition equals a structural map.
Русский
Вариант app_invApp' даёт экв-умножение в виде eqToHom, показывая, что композиция обратной части и применения совпадает со структурной картой.
LaTeX
$$$$ f.app U \;\; ≫ (f.appIso (f^{-1}^U)).inv = Y.presheaf.map (eqToHom (Opens.ext (\text{...}))).op $$$$
Lean4
@[reassoc (attr := simp), elementwise nosimp]
theorem appLE_appIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens}
(e : V ≤ f ⁻¹ᵁ U) :
f.appLE U V e ≫ (f.appIso V).inv =
Y.presheaf.map
(homOfLE <| (f.image_le_image_of_le e).trans (f.image_preimage_eq_opensRange_inter U ▸ inf_le_right)).op :=
by
simp only [appLE, Category.assoc, appIso_inv_naturality, Functor.op_obj, Functor.op_map, Quiver.Hom.unop_op,
opensFunctor_map_homOfLE, app_appIso_inv_assoc, Opens.carrier_eq_coe]
rw [← Functor.map_comp]
rfl
