instIsIsoCommRingCatApp — Mathlib

English

If f is an isomorphism of schemes, then for every open subset U of the target Y, the induced map on the rings of sections f#: OY(U) → OX(f^{-1}(U)) is an isomorphism.

Русский

Пусть f: X → Y — изоморфизм схем; тогда для каждого открытого множества U ⊆ Y отображение O_Y(U) → O_X(f^{-1}(U)) является изоморфизмом.

LaTeX

$$$\forall X,Y$ schemes, $f:X\to Y$ isIso, and $U\subseteq Y$ open, the induced map $f^{\#}_U: \mathcal{O}_Y(U) \to \mathcal{O}_X(f^{-1}(U))$ is an isomorphism.$$

Lean4

instance {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U) : IsIso (f.app U) :=
  haveI := PresheafedSpace.c_isIso_of_iso f.toPshHom
  NatIso.isIso_app_of_isIso f.c _

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