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 forf : R ⶠS
if everys : S
is of the formf 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)
:
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
@[instance 900]
instance
AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⶠY)
[AlgebraicGeometry.IsOpenImmersion f]
:
Equations
- ⯠= âŻ
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]
:
Equations
- ⯠= âŻ
@[instance 900]
instance
AlgebraicGeometry.IsPreimmersion.instMonoScheme
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⶠY)
[AlgebraicGeometry.IsPreimmersion 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)]
:
theorem
AlgebraicGeometry.IsPreimmersion.comp_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⶠY)
(g : Y ⶠZ)
[AlgebraicGeometry.IsPreimmersion g]
: