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_eq_inf :
@AlgebraicGeometry.IsOpenImmersion = (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding) ⊓ AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f
instance
AlgebraicGeometry.instIsLocalAtTargetStalkwiseBijectiveCoeRingHom :
AlgebraicGeometry.IsLocalAtTarget
(AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f)