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 ⇑f.hom)
:
IsOpenImmersion (Spec.map f) ↔ ∃ (e : ↑R), IsIdempotentElem e ∧ RingHom.ker f.hom = 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 ⇑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)