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 : 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) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
• base_closed : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.isClosedImmersion_iff {X Y : Scheme} (f : X ⟶ Y) : IsClosedImmersion f ↔ SurjectiveOnStalks f ∧ Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

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

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

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

Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding.

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

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

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

@[instance 900]

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

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

Isomorphisms are closed immersions.

@[instance 100]

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

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

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.

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

Composition with an isomorphism preserves closed immersions.

instance AlgebraicGeometry.IsClosedImmersion.instSubschemeι {X : Scheme} (I : X.IdealSheafData) : IsClosedImmersion I.subschemeι

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

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.

theorem AlgebraicGeometry.IsClosedImmersion.of_surjective_of_isAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) (h : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f))) : 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 : 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.

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

@[instance 100]

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

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

noncomputable def AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData (X : Scheme) : (CategoryTheory.MorphismProperty.Over @IsClosedImmersion ⊤ X)ᵒᵖ ≌ X.IdealSheafData

The category of closed subschemes is contravariantly equivalent to the lattice of ideal sheaves.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot {X Y : Scheme} {f : X ⟶ Y} [IsClosedImmersion f] : CategoryTheory.IsIso f ↔ Scheme.Hom.ker f = ⊥

noncomputable def AlgebraicGeometry.IsClosedImmersion.lift {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] (H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g) : Y ⟶ X

The universal property of closed immersions: For a closed immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose kernel contains the kernel of X in Z, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.IsClosedImmersion.lift_fac {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] (H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g) : CategoryTheory.CategoryStruct.comp (lift f g H) f = g

@[simp]

theorem AlgebraicGeometry.IsClosedImmersion.lift_fac_assoc {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] (H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g) {Z✝ : Scheme} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift f g H) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h

theorem AlgebraicGeometry.isDominant_of_of_appTop_injective {X Y : Scheme} [IsAffine Y] {f : X ⟶ Y} [CompactSpace ↥X] (hfinj : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f))) : IsDominant f

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

@[deprecated AlgebraicGeometry.isDominant_of_of_appTop_injective (since := "2025-05-10")]

theorem AlgebraicGeometry.surjective_of_isClosed_range_of_injective {X Y : Scheme} [IsAffine Y] {f : X ⟶ Y} [CompactSpace ↥X] (hfinj : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f))) : IsDominant f

Alias of AlgebraicGeometry.isDominant_of_of_appTop_injective.

---

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

instance AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat {X : Scheme} [CompactSpace ↥X] : IsDominant X.toSpecΓ

theorem AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective {X Y : Scheme} [IsAffine Y] {f : X ⟶ Y} [CompactSpace ↥X] (hfopen : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (hfinj₁ : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (hfinj₂ : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f))) (x : ↥X) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (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 : Scheme} [IsAffine Y] {f : X ⟶ Y} [IsClosedImmersion f] (hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop 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 : Scheme} [IsAffine Y] (f : X ⟶ Y) [IsClosedImmersion f] : IsAffine X ∧ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f))

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

theorem AlgebraicGeometry.IsClosedImmersion.Spec_iff {X : Scheme} {R : CommRingCat} {f : X ⟶ Spec R} : IsClosedImmersion f ↔ ∃ (I : Ideal ↑R) (e : X ≅ Spec (CommRingCat.of (↑R ⧸ I))), f = CategoryTheory.CategoryStruct.comp e.hom (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

instance AlgebraicGeometry.IsClosedImmersion.isLocalAtTarget : IsLocalAtTarget @IsClosedImmersion

Being a closed immersion is local at the target.

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

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

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

Being a closed immersion is stable under base change.

instance AlgebraicGeometry.instIsClosedImmersionFstScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion g] : IsClosedImmersion (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instIsClosedImmersionSndScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] : IsClosedImmersion (CategoryTheory.Limits.pullback.snd f g)

@[instance 900]

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

Closed immersions are locally of finite type.

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

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

theorem AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion {X : Scheme} {x : ↥X} : IsClosed {x} ↔ IsClosedImmersion (X.fromSpecResidueField x)

theorem AlgebraicGeometry.isClosedImmersion_of_comp_eq_id {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y) : IsClosedImmersion g

instance AlgebraicGeometry.instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat {X Y : Scheme} [Subsingleton ↥X] (f : CategoryTheory.Retract X Y) : IsClosedImmersion f.i

@[instance 100]

instance AlgebraicGeometry.instIsClosedImmersionOfSubsingletonCarrierCarrierCommRingCatOfIsOver {X Y : Scheme} [Subsingleton ↥Y] [X.Over Y] (f : Y ⟶ X) [Scheme.Hom.IsOver f Y] : IsClosedImmersion f