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