English
For an isomorphism f of schemes, the inverse morphism inv f induces a corresponding morphism on each open U that is the inverse of the forward component on the corresponding preimage.
Русский
Пусть f: X → Y — изоморфизм схем. Инверсию inv f на каждом открытом U можно рассматривать как обратный компонент к отображению f на U, то есть он является его обратным отображением на соответствующем предобразе.
LaTeX
$$$\forall X,Y$ schemes, $f:X\to Y$ isIso, $U$ open in X,$$(f^{-1})_U = f|_{f^{-1}(U)}^{-1}.$$$$
Lean4
@[simp]
theorem inv_app {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U : X.Opens) :
(inv f).app U =
X.presheaf.map (eqToHom (show (f ≫ inv f) ⁻¹ᵁ U = U by rw [IsIso.hom_inv_id]; rfl)).op ≫
inv (f.app ((inv f) ⁻¹ᵁ U)) :=
by rw [IsIso.eq_comp_inv, ← Scheme.comp_app, Scheme.congr_app (IsIso.hom_inv_id f), Scheme.id_app, Category.id_comp]
