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_SpecMap_iff_of_surjective {R S : CommRingCat} (f : R ⟶ S) (hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)) : IsOpenImmersion (Spec.map f) ↔ ∃ (e : ↑R), IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Spec (R ⧸ I) ⟶ Spec R is an open immersion iff I is generated by an idempotent.

@[deprecated AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap (since := "2026-01-20")]

theorem AlgebraicGeometry.isOpenImmersion_iff_stalk {X Y : Scheme} {f : X ⟶ Y} : IsOpenImmersion f ↔ Topology.IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)

Alias of AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap.

theorem AlgebraicGeometry.IsOpenImmersion.of_openCover_source {X Y : Scheme} (f : X ⟶ Y) (𝒰 : X.OpenCover) (hf : Function.Injective ⇑f) (h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : IsOpenImmersion f

theorem AlgebraicGeometry.IsOpenImmersion.of_forall_source_exists {X Y : Scheme} (f : X ⟶ Y) (hf : Function.Injective ⇑f) (hX : ∀ (x : ↥X), ∃ (U : Scheme) (i : U ⟶ X) (x_1 : IsOpenImmersion i), x ∈ Scheme.Hom.opensRange i ∧ IsOpenImmersion (CategoryTheory.CategoryStruct.comp i f)) : IsOpenImmersion f

theorem AlgebraicGeometry.isOpenImmersion_eq_inf : IsOpenImmersion = (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓ stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => Function.Bijective ⇑x

instance AlgebraicGeometry.instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom : IsZariskiLocalAtTarget (stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => Function.Bijective ⇑x)

instance AlgebraicGeometry.isOpenImmersion_isZariskiLocalAtTarget : IsZariskiLocalAtTarget IsOpenImmersion

instance AlgebraicGeometry.instIsOpenImmersionMapScheme {X Y X' Y' : Scheme} (f : X ⟶ X') (g : Y ⟶ Y') [IsOpenImmersion f] [IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.Limits.coprod.map f g)