mathlib3 documentation


Open immersions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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/*.