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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : 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.

• base_embedding : IsEmbedding ⇑f.base
• surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

theorem AlgebraicGeometry.isPreimmersion_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsPreimmersion f ↔ IsEmbedding ⇑f.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

theorem AlgebraicGeometry.IsPreimmersion.base_embedding {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsPreimmersion f] : IsEmbedding ⇑f.base

theorem AlgebraicGeometry.IsPreimmersion.surj_on_stalks {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsPreimmersion f] (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

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

@[deprecated AlgebraicGeometry.Scheme.Hom.isEmbedding]

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

Alias of AlgebraicGeometry.Scheme.Hom.isEmbedding.

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsPreimmersion f] (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(f.stalkMap x)

theorem AlgebraicGeometry.isPreimmersion_eq_inf : @AlgebraicGeometry.IsPreimmersion = (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding) ⊓ AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => Function.Surjective ⇑x

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.

Equations

• AlgebraicGeometry.isSurjectiveOnStalks_isLocalAtTarget = ⋯

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

Equations

• AlgebraicGeometry.IsPreimmersion.instIsLocalAtTarget = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

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

Equations

• AlgebraicGeometry.IsPreimmersion.instIsMultiplicativeScheme = ⋯

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

Equations

• ⋯ = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsPreimmersion.of_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map f) ↔ IsEmbedding ⇑(PrimeSpectrum.comap f) ∧ RingHom.SurjectiveOnStalks f

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

theorem AlgebraicGeometry.IsPreimmersion.of_isLocalization {R : Type u} {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)))