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
.
class
AlgebraicGeometry.IsPreimmersion
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
extends AlgebraicGeometry.SurjectiveOnStalks f :
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
Instances
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 900]
instance
AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsOpenImmersion f]
:
instance
AlgebraicGeometry.IsPreimmersion.comp
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.IsPreimmersion f]
[AlgebraicGeometry.IsPreimmersion g]
:
@[instance 900]
instance
AlgebraicGeometry.IsPreimmersion.instMonoScheme
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsPreimmersion 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)]
:
theorem
AlgebraicGeometry.IsPreimmersion.comp_iff
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.IsPreimmersion g]
:
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)
:
theorem
AlgebraicGeometry.IsPreimmersion.of_isLocalization
{R S : Type u}
[CommRing R]
(M : Submonoid R)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
: