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.

TODO

• Show that diagonal morphisms are immersions

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

• base_embedding : IsEmbedding ⇑f.base
• surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
• isLocallyClosed_range : IsLocallyClosed (Set.range ⇑f.base)

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

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

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

def AlgebraicGeometry.Scheme.Hom.coborderRange {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.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

• f.coborderRange = { carrier := coborder (Set.range ⇑f.base), is_open' := ⋯ }

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

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

• f.liftCoborder = AlgebraicGeometry.IsOpenImmersion.lift f.coborderRange.ι f ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.liftCoborder_ι {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsImmersion f] : CategoryTheory.CategoryStruct.comp f.liftCoborder f.coborderRange.ι = 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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsImmersion f] {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f.liftCoborder (CategoryTheory.CategoryStruct.comp f.coborderRange.ι h) = CategoryTheory.CategoryStruct.comp f h

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isImmersion_eq_inf : @AlgebraicGeometry.IsImmersion = @AlgebraicGeometry.IsPreimmersion ⊓ AlgebraicGeometry.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.instIsLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsImmersion

Equations

• AlgebraicGeometry.IsImmersion.instIsLocalAtTarget = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

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

Equations

• AlgebraicGeometry.IsImmersion.instIsMultiplicativeScheme = ⋯

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsImmersion.isImmersion_iff_exists {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} : AlgebraicGeometry.IsImmersion f ↔ ∃ (Z : AlgebraicGeometry.Scheme) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), AlgebraicGeometry.IsClosedImmersion g₁ ∧ AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsImmersion g] [AlgebraicGeometry.IsImmersion (CategoryTheory.CategoryStruct.comp f g)] : AlgebraicGeometry.IsImmersion f

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

theorem AlgebraicGeometry.IsImmersion.stableUnderBaseChange : CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.IsImmersion