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.

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

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] (f : R →+* S) => Function.Bijective ⇑f

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

instance AlgebraicGeometry.isOpenImmersion_isLocalAtTarget : IsLocalAtTarget @IsOpenImmersion