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.

class AlgebraicGeometry.IsClosedImmersion {X 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 : Topology.IsClosedEmbedding ⇑f.base
• surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

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

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

@[deprecated AlgebraicGeometry.Scheme.Hom.isClosedEmbedding]

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

Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding.

@[deprecated AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding]

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

Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding.

---

Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding.

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

theorem AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} : AlgebraicGeometry.IsClosedImmersion f ↔ AlgebraicGeometry.IsPreimmersion f ∧ IsClosed (Set.range ⇑f.base)

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

@[instance 900]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme {X 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 Y 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 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 Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (h : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)) : AlgebraicGeometry.IsClosedImmersion f

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

theorem AlgebraicGeometry.IsClosedImmersion.of_comp_isClosedImmersion {X Y 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 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.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.surjective_of_isClosed_range_of_injective {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [CompactSpace ↑↑X.toPresheafedSpace] (hfcl : IsClosed (Set.range ⇑f.base)) (hfinj : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)) : 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.

theorem AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [CompactSpace ↑↑X.toPresheafedSpace] (hfopen : IsOpenMap ⇑f.base) (hfinj₁ : Function.Injective ⇑f.base) (hfinj₂ : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)) (x : ↑↑X.toPresheafedSpace) : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)

If f : X ⟶ Y is open, injective, X is quasi-compact and Y is affine, then f is stalkwise injective if it is injective on global sections.

theorem AlgebraicGeometry.IsClosedImmersion.isIso_of_injective_of_isAffine {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [AlgebraicGeometry.IsClosedImmersion f] (hf : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)) : CategoryTheory.IsIso f

If f is a closed immersion with affine target such that the induced map on global sections is injective, f is an isomorphism.

theorem AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] : AlgebraicGeometry.IsAffine X ∧ Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)

If f is a closed immersion with affine target, the source is affine and the induced map on global sections is surjective.

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

Being a closed immersion is local at the target.

Equations

• AlgebraicGeometry.IsClosedImmersion.isLocalAtTarget = ⋯

instance AlgebraicGeometry.IsClosedImmersion.hasAffineProperty : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsClosedImmersion fun (X x : AlgebraicGeometry.Scheme) (f : X ⟶ x) [AlgebraicGeometry.IsAffine x] => AlgebraicGeometry.IsAffine X ∧ Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)

On morphisms with affine target, being a closed immersion is precisely having affine source and being surjective on global sections.

Equations

• AlgebraicGeometry.IsClosedImmersion.hasAffineProperty = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsClosedImmersion

Being a closed immersion is stable under base change.

Equations

• AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange = ⋯

@[instance 900]

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

Closed immersions are locally of finite type.

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.IsReduced Y] : CategoryTheory.IsIso f

A surjective closed immersion is an isomorphism when the target is reduced.