Preimmersions of schemes

A morphism of schemes f : X ⟶ Y is a preimmersion if the underlying map of topological spaces is an embedding and the induced morphisms of stalks are all surjective. This is not a concept seen in the literature but it is useful for generalizing results on immersions to other maps including Spec 𝒪_{X, x} ⟶ X and inclusions of fibers κ(x) ×ₓ Y ⟶ Y.

class AlgebraicGeometry.IsPreimmersion {X Y : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.SurjectiveOnStalks f : Prop

A morphism of schemes f : X ⟶ Y is a preimmersion if the underlying map of topological spaces is an embedding and the induced morphisms of stalks are all surjective.

• surj_on_stalks (x : ↥X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
• base_embedding : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.isPreimmersion_iff {X Y : Scheme} (f : X ⟶ Y) : IsPreimmersion f ↔ SurjectiveOnStalks f ∧ Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.Scheme.Hom.isEmbedding {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f] : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.isPreimmersion_eq_inf : @IsPreimmersion = @SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding

instance AlgebraicGeometry.IsPreimmersion.instIsZariskiLocalAtTarget : IsZariskiLocalAtTarget @IsPreimmersion

@[instance 900]

instance AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsPreimmersion f

instance AlgebraicGeometry.IsPreimmersion.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @IsPreimmersion

instance AlgebraicGeometry.IsPreimmersion.comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion f] [IsPreimmersion g] : IsPreimmersion (CategoryTheory.CategoryStruct.comp f g)

@[instance 900]

instance AlgebraicGeometry.IsPreimmersion.instMonoScheme {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f] : CategoryTheory.Mono f

theorem AlgebraicGeometry.IsPreimmersion.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] [IsPreimmersion (CategoryTheory.CategoryStruct.comp f g)] : IsPreimmersion f

theorem AlgebraicGeometry.IsPreimmersion.comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] : IsPreimmersion (CategoryTheory.CategoryStruct.comp f g) ↔ IsPreimmersion f

theorem AlgebraicGeometry.IsPreimmersion.SpecMap_iff {R S : CommRingCat} (f : R ⟶ S) : IsPreimmersion (Spec.map f) ↔ Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

@[deprecated AlgebraicGeometry.IsPreimmersion.SpecMap_iff (since := "2025-10-07")]

theorem AlgebraicGeometry.IsPreimmersion.Spec_map_iff {R S : CommRingCat} (f : R ⟶ S) : IsPreimmersion (Spec.map f) ↔ Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

Alias of AlgebraicGeometry.IsPreimmersion.SpecMap_iff.

theorem AlgebraicGeometry.IsPreimmersion.mk_SpecMap {R S : CommRingCat} {f : R ⟶ S} (h₁ : Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f))) (h₂ : (CommRingCat.Hom.hom f).SurjectiveOnStalks) : IsPreimmersion (Spec.map f)

@[deprecated AlgebraicGeometry.IsPreimmersion.mk_SpecMap (since := "2025-10-07")]

theorem AlgebraicGeometry.IsPreimmersion.mk_Spec_map {R S : CommRingCat} {f : R ⟶ S} (h₁ : Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f))) (h₂ : (CommRingCat.Hom.hom f).SurjectiveOnStalks) : IsPreimmersion (Spec.map f)

Alias of AlgebraicGeometry.IsPreimmersion.mk_SpecMap.

theorem AlgebraicGeometry.IsPreimmersion.of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S] [Algebra R S] [IsLocalization M S] : IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))

instance AlgebraicGeometry.IsPreimmersion.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsPreimmersion