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.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)) :
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)) :
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.instIsOpenImmersionMapScheme {X Y X' Y' : Scheme} (f : X ⟶ X') (g : Y ⟶ Y') [IsOpenImmersion f] [IsOpenImmersion g] :