mathlib documentation

algebraic_geometry.morphisms.open_immersion

Open immersions #

A morphism is an open immersions if the underlying map of spaces is an open embedding f : X ⟶ U ⊆ Y, and the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Most of the theories are developed in algebraic_geometry/open_immersion, and we provide the remaining theorems analogous to other lemmas in algebraic_geometry/morphisms/*.