Documentation

Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Open immersions #

A morphism is an open immersion 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 AlgebraicGeometry/OpenImmersion, and we provide the remaining theorems analogous to other lemmas in AlgebraicGeometry/Morphisms/*.

theorem AlgebraicGeometry.IsOpenImmersion.openCover_TFAE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) :
List.TFAE [AlgebraicGeometry.IsOpenImmersion f, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y), ∀ (i : 𝒰.J), AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (i : 𝒰.J), AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd, ∀ (U : TopologicalSpace.Opens Y.toPresheafedSpace), AlgebraicGeometry.IsOpenImmersion (f ∣_ U), ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd, ∃ (ι : Type u) (U : ιTopologicalSpace.Opens Y.toPresheafedSpace) (_ : iSup U = ), ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion (f ∣_ U i)]