English
Equality relating ΓIsoTop to the canonical opens functor on opens.
Русский
Равенство между ΓIsoTop и каноническим отображением функций открытых множеств.
LaTeX
$$$ \Gamma\text{IsoTop } f U = (\text{opens functor}) $$$
Lean4
@[simp]
theorem ΓIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) :
(ΓIso f U).inv =
f.appLE (f.opensRange ⊓ U) (f ⁻¹ᵁ U) (by rw [← f.image_preimage_eq_opensRange_inter, f.preimage_image_eq]) :=
by
simp only [ΓIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, eqToHom_op, Iso.symm_inv,
Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE]