Immersions of schemes

A morphism of schemes f : X ⟶ Y is an immersion if the underlying map of topological spaces is a locally closed embedding, and the induced morphisms of stalks are all surjective. This is true if and only if it can be factored into a closed immersion followed by an open immersion.

Main result

• isImmersion_iff_exists: A morphism is a (locally-closed) immersion if and only if it can be factored into a closed immersion followed by a (dominant) open immersion.
• isImmersion_iff_exists_of_quasiCompact: A quasicompact morphism is a (locally-closed) immersion if and only if it can be factored into an open immersion followed by a closed immersion.

class AlgebraicGeometry.IsImmersion {X Y : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.IsPreimmersion f : Prop

A morphism of schemes f : X ⟶ Y is an immersion if

1. the underlying map of topological spaces is an embedding
2. the range of the map is locally closed
3. the induced morphisms of stalks are all surjective.

• surj_on_stalks (x : ↥X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
• base_embedding : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)
• isLocallyClosed_range : IsLocallyClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))

theorem AlgebraicGeometry.isImmersion_iff {X Y : Scheme} (f : X ⟶ Y) : IsImmersion f ↔ IsPreimmersion f ∧ IsLocallyClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))

theorem AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : IsLocallyClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))

def AlgebraicGeometry.Scheme.Hom.coborderRange {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : Y.Opens

Given an immersion f : X ⟶ Y, this is the biggest open set U ⊆ Y containing the image of X such that X is closed in U.

Equations

• AlgebraicGeometry.Scheme.Hom.coborderRange f = { carrier := coborder (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)), is_open' := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Hom.liftCoborder {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : X ⟶ ↑(coborderRange f)

The first part of the factorization of an immersion f : X ⟶ Y to a closed immersion f.liftCoborder : X ⟶ f.coborderRange and a dominant open immersion f.coborderRange.ι.

Equations

• AlgebraicGeometry.Scheme.Hom.liftCoborder f = AlgebraicGeometry.IsOpenImmersion.lift (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι f ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.liftCoborder_ι {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : CategoryTheory.CategoryStruct.comp (liftCoborder f) (coborderRange f).ι = f

Any (locally-closed) immersion can be factored into a closed immersion followed by a (dominant) open immersion.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.liftCoborder_ι_assoc {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftCoborder f) (CategoryTheory.CategoryStruct.comp (coborderRange f).ι h) = CategoryTheory.CategoryStruct.comp f h

theorem AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] (U : (↑(coborderRange f)).Opens) : (TopologicalSpace.Opens.map (liftCoborder f).base).obj U = (TopologicalSpace.Opens.map f.base).obj ((opensFunctor (coborderRange f).ι).obj U)

theorem AlgebraicGeometry.liftCoborder_app {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] (U : (↑(Scheme.Hom.coborderRange f)).Opens) : Scheme.Hom.app (Scheme.Hom.liftCoborder f) U = CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f ((Scheme.Hom.opensFunctor (Scheme.Hom.coborderRange f).ι).obj U)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

instance AlgebraicGeometry.instIsClosedImmersionLiftCoborder {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : IsClosedImmersion (Scheme.Hom.liftCoborder f)

instance AlgebraicGeometry.instIsDominantιCoborderRange {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : IsDominant (Scheme.Hom.coborderRange f).ι

theorem AlgebraicGeometry.isImmersion_eq_inf : @IsImmersion = @IsPreimmersion ⊓ topologically fun {x x_1 : Type u_1} (x_2 : TopologicalSpace x) (x_3 : TopologicalSpace x_1) (f : x → x_1) => IsLocallyClosed (Set.range f)

instance AlgebraicGeometry.IsImmersion.instIsZariskiLocalAtTarget : IsZariskiLocalAtTarget @IsImmersion

@[instance 900]

instance AlgebraicGeometry.IsImmersion.instOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsImmersion f

@[instance 900]

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

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

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

theorem AlgebraicGeometry.IsImmersion.isImmersion_iff_exists {X Y : Scheme} {f : X ⟶ Y} : IsImmersion f ↔ ∃ (Z : Scheme) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), IsClosedImmersion g₁ ∧ IsOpenImmersion g₂ ∧ CategoryTheory.CategoryStruct.comp g₁ g₂ = f

A morphism is a (locally-closed) immersion if and only if it can be factored into a closed immersion followed by an open immersion.

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

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

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

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

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

instance AlgebraicGeometry.IsImmersion.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [IsImmersion f] : IsImmersion (f ∣_ V)

instance AlgebraicGeometry.IsImmersion.instResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [IsImmersion f] : IsImmersion (Scheme.Hom.resLE f V U e)

instance AlgebraicGeometry.IsImmersion.instDiagonalScheme {X Y : Scheme} (f : X ⟶ Y) : IsImmersion (CategoryTheory.Limits.pullback.diagonal f)

The diagonal morphism is always an immersion.

instance AlgebraicGeometry.IsImmersion.instLiftSchemeId {X : Scheme} : IsImmersion (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))

instance AlgebraicGeometry.IsImmersion.instιScheme {X Y : Scheme} (f g : X ⟶ Y) : IsImmersion (CategoryTheory.Limits.equalizer.ι f g)

instance AlgebraicGeometry.IsImmersion.instToImage {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : IsImmersion (Scheme.Hom.toImage f)

theorem AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] [QuasiCompact f] : CategoryTheory.IsPullback (Scheme.Hom.toImage f) (Scheme.Hom.liftCoborder f) (Scheme.Hom.imageι f) (Scheme.Hom.coborderRange f).ι

If f : X ⟶ Y is a quasi-compact immersion, then X is the pullback of the closed immersion im f ⟶ Y and an open immersion U ⟶ Y.

instance AlgebraicGeometry.IsImmersion.instIsOpenImmersionToImageOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] [QuasiCompact f] : IsOpenImmersion (Scheme.Hom.toImage f)

theorem AlgebraicGeometry.IsImmersion.isImmersion_iff_exists_of_quasiCompact {X Y : Scheme} {f : X ⟶ Y} [QuasiCompact f] : IsImmersion f ↔ ∃ (Z : Scheme) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), IsOpenImmersion g₁ ∧ IsClosedImmersion g₂ ∧ CategoryTheory.CategoryStruct.comp g₁ g₂ = f

A quasi-compact morphism is a (locally-closed) immersion if and only if it can be factored into an open immersion followed by a closed immersion.