appIso — Mathlib

English

Let f: X → Y be an open immersion of schemes. For every open subset U of X, there is a natural isomorphism between the ring of global sections on the image f''U in Y and the ring of global sections on U in X; i.e. Γ(Y, f''ᵁU) ≅ Γ(X, U).

Русский

Пусть f: X → Y — открытое вложение схем. Для любого открытого подмножества U ⊆ X существует естественный изоморфизм колец глобальных секций над образами, а именно Γ(Y, f''ᵁU) ≅ Γ(X, U).

LaTeX

$$$$\Gamma(Y, f''^\!\!U) \cong \Gamma(X, U).$$$$

Lean4

/-- The isomorphism `Γ(Y, f(U)) ≅ Γ(X, U)` induced by an open immersion `f : X ⟶ Y`. -/
def appIso (U) : Γ(Y, f ''ᵁ U) ≅ Γ(X, U) :=
  (asIso <| LocallyRingedSpace.IsOpenImmersion.invApp f.toLRSHom U).symm

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