Closed immersions of schemes #

A morphism of schemes f : X ⟶ Y is a closed immersion if the underlying map of topological spaces is a closed immersion and the induced morphisms of stalks are all surjective.

Main definitions #

IsClosedImmersion : The property of scheme morphisms stating f : X ⟶ Y is a closed immersion.

TODO #

Show closed immersions are precisely the proper monomorphisms
Define closed immersions of locally ringed spaces, where we also assume that the kernel of O_X → f_*O_Y is locally generated by sections as an O_X-module, and relate it to this file. See https://stacks.math.columbia.edu/tag/01HJ.

source

class AlgebraicGeometry.IsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.SurjectiveOnStalks f :

Prop

A morphism of schemes X ⟶ Y is a closed immersion if the underlying topological map is a closed embedding and the induced stalk maps are surjective.

surj_on_stalks (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(Scheme.Hom.stalkMap f x).hom
base_closed : Topology.IsClosedEmbedding ⇑f.base

Instances

source

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

IsClosedImmersion f ↔ SurjectiveOnStalks f ∧ Topology.IsClosedEmbedding ⇑f.base

source

theorem AlgebraicGeometry.Scheme.Hom.isClosedEmbedding {X Y : Scheme} (f : X.Hom Y) [IsClosedImmersion f] :

Topology.IsClosedEmbedding ⇑f.base

source

@[deprecated AlgebraicGeometry.Scheme.Hom.isClosedEmbedding (since := "2024-10-24")]

theorem AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding {X Y : Scheme} (f : X.Hom Y) [IsClosedImmersion f] :

Topology.IsClosedEmbedding ⇑f.base

Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding.

source

@[deprecated AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding (since := "2024-10-20")]

theorem AlgebraicGeometry.IsClosedImmersion.closedEmbedding {X Y : Scheme} (f : X.Hom Y) [IsClosedImmersion f] :

Topology.IsClosedEmbedding ⇑f.base

Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding.

source

theorem AlgebraicGeometry.IsClosedImmersion.eq_inf :

@IsClosedImmersion = (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding) ⊓ @SurjectiveOnStalks

source

theorem AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion {X Y : Scheme} {f : X ⟶ Y} :

IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range ⇑f.base)

source

theorem AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f] (hf : IsClosed (Set.range ⇑f.base)) :

IsClosedImmersion f

source

@[instance 900]

instance AlgebraicGeometry.IsClosedImmersion.instIsPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] :

IsPreimmersion f

source

instance AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

IsClosedImmersion f

Isomorphisms are closed immersions.

source

instance AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @IsClosedImmersion

source

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

IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)

Composition of closed immersions is a closed immersion.

source

instance AlgebraicGeometry.IsClosedImmersion.respectsIso :

CategoryTheory.MorphismProperty.RespectsIso @IsClosedImmersion

Composition with an isomorphism preserves closed immersions.

source

theorem AlgebraicGeometry.IsClosedImmersion.spec_of_surjective {R S : CommRingCat} (f : R ⟶ S) (h : Function.Surjective ⇑f.hom) :

IsClosedImmersion (Spec.map f)

Given two commutative rings R S : CommRingCat and a surjective morphism f : R ⟶ S, the induced scheme morphism specObj S ⟶ specObj R is a closed immersion.

source

instance AlgebraicGeometry.IsClosedImmersion.spec_of_quotient_mk {R : CommRingCat} (I : Ideal ↑R) :

IsClosedImmersion (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

For any ideal I in a commutative ring R, the quotient map specObj R ⟶ specObj (R ⧸ I) is a closed immersion.

source

theorem AlgebraicGeometry.IsClosedImmersion.of_surjective_of_isAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) (h : Function.Surjective ⇑(Scheme.Hom.appTop f).hom) :

IsClosedImmersion f

Any morphism between affine schemes that is surjective on global sections is a closed immersion.

source

theorem AlgebraicGeometry.IsClosedImmersion.of_comp_isClosedImmersion {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion g] [IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)] :

IsClosedImmersion f

If f ≫ g and g are closed immersions, then f is a closed immersion. Also see IsClosedImmersion.of_comp for the general version where g is only required to be separated.

source

instance AlgebraicGeometry.IsClosedImmersion.Spec_map_residue {X : Scheme} (x : ↑↑X.toPresheafedSpace) :

IsClosedImmersion (Spec.map (X.residue x))

source

instance AlgebraicGeometry.IsClosedImmersion.instQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] :

QuasiCompact f

source

theorem AlgebraicGeometry.surjective_of_isClosed_range_of_injective {X Y : Scheme} [IsAffine Y] {f : X ⟶ Y} [CompactSpace ↑↑X.toPresheafedSpace] (hfcl : IsClosed (Set.range ⇑f.base)) (hfinj : Function.Injective ⇑(Scheme.Hom.appTop f).hom) :

Function.Surjective ⇑f.base

If f : X ⟶ Y is a morphism of schemes with quasi-compact source and affine target, f has a closed image and f induces an injection on global sections, then f is surjective.

source