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
.
class
AlgebraicGeometry.IsPreimmersion
{X Y : 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.
- base_embedding : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)
Instances
@[deprecated AlgebraicGeometry.Scheme.Hom.isEmbedding (since := "2024-10-26")]
Alias of AlgebraicGeometry.Scheme.Hom.isEmbedding
.
theorem
AlgebraicGeometry.isPreimmersion_eq_inf :
@IsPreimmersion = @SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding
@[instance 900]
instance
AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion
{X Y : Scheme}
(f : X ⟶ Y)
[IsOpenImmersion f]
:
instance
AlgebraicGeometry.IsPreimmersion.comp
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[IsPreimmersion f]
[IsPreimmersion g]
:
@[instance 900]
instance
AlgebraicGeometry.IsPreimmersion.instMonoScheme
{X Y : Scheme}
(f : X ⟶ Y)
[IsPreimmersion f]
:
theorem
AlgebraicGeometry.IsPreimmersion.of_comp
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[IsPreimmersion g]
[IsPreimmersion (CategoryTheory.CategoryStruct.comp f g)]
:
theorem
AlgebraicGeometry.IsPreimmersion.comp_iff
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[IsPreimmersion g]
:
theorem
AlgebraicGeometry.IsPreimmersion.mk_Spec_map
{R S : CommRingCat}
{f : R ⟶ S}
(h₁ : Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)))
(h₂ : (CommRingCat.Hom.hom f).SurjectiveOnStalks)
:
theorem
AlgebraicGeometry.IsPreimmersion.of_isLocalization
{R S : Type u}
[CommRing R]
(M : Submonoid R)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
:
IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))