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), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)
theorem
AlgebraicGeometry.IsOpenImmersion.of_openCover_source
{X Y : Scheme}
(f : X ⟶ Y)
(𝒰 : X.OpenCover)
(hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base))
(h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (CategoryTheory.CategoryStruct.comp (𝒰.f i) f))
:
theorem
AlgebraicGeometry.IsOpenImmersion.of_forall_source_exists
{X Y : Scheme}
(f : X ⟶ Y)
(hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base))
(hX :
∀ (x : ↥X),
∃ (U : Scheme) (i : U ⟶ X) (x_1 : IsOpenImmersion i),
x ∈ Scheme.Hom.opensRange i ∧ IsOpenImmersion (CategoryTheory.CategoryStruct.comp i 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] (f : R →+* S) => Function.Bijective ⇑f
instance
AlgebraicGeometry.instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom :
IsZariskiLocalAtTarget (stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f)