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.

theorem AlgebraicGeometry.isClosedImmersion_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsClosedImmersion f ↔ ClosedEmbedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

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)

theorem AlgebraicGeometry.IsClosedImmersion.eq_inf : @AlgebraicGeometry.IsClosedImmersion = (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => ClosedEmbedding) ⊓ AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Surjective ⇑f

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

• ⋯ = ⋯

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

Composition with an isomorphism preserves closed immersions.

Equations

• AlgebraicGeometry.IsClosedImmersion.respectsIso = ⋯

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_surjective_of_isAffine {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (h : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Γ.map f.op)) : AlgebraicGeometry.IsClosedImmersion f

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

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

• ⋯ = ⋯

instance AlgebraicGeometry.isSurjectiveOnStalks_isLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Surjective ⇑f)

Being surjective on stalks is local at the target.

Equations

• AlgebraicGeometry.isSurjectiveOnStalks_isLocalAtTarget = ⋯

instance AlgebraicGeometry.IsClosedImmersion.isLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsClosedImmersion

Being a closed immersion is local at the target.

Equations

• AlgebraicGeometry.IsClosedImmersion.isLocalAtTarget = ⋯