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.

TODO

• Show preimmersions are local at the target.
• Show preimmersions are stable under pullback.
• Show that Spec f is a preimmersion for f : R ⟶ S if every s : S is of the form f a / f b.

class AlgebraicGeometry.IsPreimmersion {X Y : AlgebraicGeometry.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.toPresheafedSpace) : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x).hom
• base_embedding : Topology.IsEmbedding ⇑f.base

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

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

@[deprecated AlgebraicGeometry.Scheme.Hom.isEmbedding]

theorem AlgebraicGeometry.Scheme.Hom.embedding {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsPreimmersion f] : Topology.IsEmbedding ⇑f.base

Alias of AlgebraicGeometry.Scheme.Hom.isEmbedding.

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

instance AlgebraicGeometry.isSurjectiveOnStalks_isLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => Function.Surjective ⇑x)

Being surjective on stalks is local at the target.

instance AlgebraicGeometry.IsPreimmersion.instIsLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsPreimmersion

@[instance 900]

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

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

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

@[instance 900]

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

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

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

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

theorem AlgebraicGeometry.IsPreimmersion.mk_Spec_map {R S : CommRingCat} {f : R ⟶ S} (h₁ : Topology.IsEmbedding ⇑(PrimeSpectrum.comap f.hom)) (h₂ : f.hom.SurjectiveOnStalks) : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.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] : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))

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