Documentation

Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

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.

theorem AlgebraicGeometry.isPreimmersion_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :

AlgebraicGeometry.IsPreimmersion f ↔ Embedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

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

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 : Embedding ⇑f.val.base
surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

Instances

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

Embedding ⇑f.val.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.embedding {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsPreimmersion f] :

Embedding ⇑f.val.base

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 β] => Embedding) ⊓ 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