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_iff_stalk
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{f : X ⟶ Y}
:
AlgebraicGeometry.IsOpenImmersion f ↔ OpenEmbedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)
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)]
theorem
AlgebraicGeometry.IsOpenImmersion.openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(𝒰 : AlgebraicGeometry.Scheme.OpenCover Y)
(f : X ⟶ Y)
:
AlgebraicGeometry.IsOpenImmersion f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd