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.

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

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

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

Alias of AlgebraicGeometry.IsPreimmersion.isEmbedding.

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

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)

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

instance AlgebraicGeometry.IsPreimmersion.instFstScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsPreimmersion g] : IsPreimmersion (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.IsPreimmersion.instSndScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsPreimmersion f] : IsPreimmersion (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.IsPreimmersion.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [IsPreimmersion f] : IsPreimmersion (f ∣_ V)