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 of affines are induced by surjective ring maps
• Show closed immersions are stable under pullback
• 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.

class AlgebraicGeometry.IsClosedImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : 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.

• base_closed : ClosedEmbedding ⇑f.val.base
• surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

theorem AlgebraicGeometry.IsClosedImmersion.base_closed {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsClosedImmersion f] : ClosedEmbedding ⇑f.val.base

theorem AlgebraicGeometry.IsClosedImmersion.surj_on_stalks {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsClosedImmersion f] (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

theorem AlgebraicGeometry.IsClosedImmersion.closedEmbedding {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] : ClosedEmbedding ⇑f.val.base

theorem AlgebraicGeometry.IsClosedImmersion.surjective_stalkMap {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

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

Isomorphisms are closed immersions.

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsClosedImmersion

Equations

• AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme = ⋯

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

Composition of closed immersions is a closed immersion.

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsClosedImmersion.respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsClosedImmersion

Composition with an isomorphism preserves closed immersions.

theorem AlgebraicGeometry.IsClosedImmersion.spec_of_surjective {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (h : Function.Surjective ⇑f) : AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.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.

instance AlgebraicGeometry.IsClosedImmersion.spec_of_quotient_mk {R : CommRingCat} (I : Ideal ↑R) : AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.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.

Equations

• ⋯ = ⋯

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

If f ≫ g is a closed immersion, then f is a closed immersion.

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

Equations

• ⋯ = ⋯