Spreading out morphisms

Under certain conditions, a morphism on stalks Spec 𝒪_{X, x} ⟶ Spec 𝒪_{Y, y} can be spread out into a neighborhood of x.

Main result

Given S-schemes X Y and points x : X y : Y over s : S. Suppose we have the following diagram of S-schemes

Spec 𝒪_{X, x} ⟶ X
    |
  Spec(φ)
    ↓
Spec 𝒪_{Y, y} ⟶ Y

We would like to spread Spec(φ) out to an S-morphism on an open subscheme U ⊆ X

Spec 𝒪_{X, x} ⟶ U ⊆ X
    |             |
  Spec(φ)         |
    ↓             ↓
Spec 𝒪_{Y, y} ⟶ Y

• AlgebraicGeometry.spread_out_unique_of_isGermInjective: The lift is "unique" if the germ map is injective at x.
• AlgebraicGeometry.spread_out_of_isGermInjective: The lift exists if Y is locally of finite type and the germ map is injective at x.

TODO

Show that certain morphism properties can also be spread out.

class AlgebraicGeometry.Scheme.IsGermInjectiveAt (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : Prop

The germ map at x is injective if there exists some affine U ∋ x such that the map Γ(X, U) ⟶ X_x is injective

• cond : ∃ (U : X.Opens) (hx : x ∈ U), AlgebraicGeometry.IsAffineOpen U ∧ Function.Injective ⇑(X.presheaf.germ U x hx)

theorem AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} [self : X.IsGermInjectiveAt x] : ∃ (U : X.Opens) (hx : x ∈ U), AlgebraicGeometry.IsAffineOpen U ∧ Function.Injective ⇑(X.presheaf.germ U x hx)

theorem AlgebraicGeometry.injective_germ_basicOpen {X : AlgebraicGeometry.Scheme} (U : X.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) (hf : x ∈ X.basicOpen f) (H : Function.Injective ⇑(X.presheaf.germ U x hx)) : Function.Injective ⇑(X.presheaf.germ (X.basicOpen f) x hf)

theorem AlgebraicGeometry.Scheme.exists_germ_injective (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) [X.IsGermInjectiveAt x] : ∃ (U : X.Opens) (hx : x ∈ U), AlgebraicGeometry.IsAffineOpen U ∧ Function.Injective ⇑(X.presheaf.germ U x hx)

theorem AlgebraicGeometry.Scheme.exists_le_and_germ_injective (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) [X.IsGermInjectiveAt x] (V : X.Opens) (hxV : x ∈ V) : ∃ (U : X.Opens) (hx : x ∈ U), AlgebraicGeometry.IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(X.presheaf.germ U x hx)

instance AlgebraicGeometry.instIsGermInjectiveAtCoeHomTopCatCarrierCommRingCatαTopologicalSpaceBaseOfIsOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) [X.IsGermInjectiveAt x] [AlgebraicGeometry.IsOpenImmersion f] : Y.IsGermInjectiveAt (f.base x)

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↑↑X.toPresheafedSpace} [AlgebraicGeometry.IsOpenImmersion f] : Y.IsGermInjectiveAt (f.base x) ↔ X.IsGermInjectiveAt x

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.IsGermInjective (X : AlgebraicGeometry.Scheme) : Prop

The class of schemes such that for each x : X, Γ(X, U) ⟶ X_x is injective for some affine U containing x.

This is typically satisfied when X is integral or locally noetherian.

Equations

• X.IsGermInjective = ∀ (x : ↑↑X.toPresheafedSpace), X.IsGermInjectiveAt x

theorem AlgebraicGeometry.Scheme.IsGermInjective.of_openCover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), (𝒰.obj i).IsGermInjective] : X.IsGermInjective

theorem AlgebraicGeometry.Scheme.IsGermInjective.Spec {R : CommRingCat} (H : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0) : (AlgebraicGeometry.Spec R).IsGermInjective

@[instance 100]

instance AlgebraicGeometry.instIsGermInjectiveOfIsIntegral {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : X.IsGermInjective

Equations

• ⋯ = ⋯

@[instance 100]

instance AlgebraicGeometry.instIsGermInjectiveOfIsLocallyNoetherian {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] : X.IsGermInjective

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.spread_out_unique_of_isGermInjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (f : X ⟶ Y) (g : X ⟶ Y) (e : f.base x = g.base x) (H : AlgebraicGeometry.Scheme.Hom.stalkMap f x = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap g x)) : ∃ (U : X.Opens), x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g

Let x : X and f g : X ⟶ Y be two morphisms such that f x = g x. If f and g agree on the stalk of x, then they agree on an open neighborhood of x, provided X is "germ-injective" at x (e.g. when it's integral or locally noetherian).

TODO: The condition on X is unnecessary when Y is locally of finite type.

theorem AlgebraicGeometry.spread_out_unique_of_isGermInjective' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (f : X ⟶ Y) (g : X ⟶ Y) (e : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) g) : ∃ (U : X.Opens), x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g

A variant of spread_out_unique_of_isGermInjective whose condition is an equality of scheme morphisms instead of ring homomorphisms.

theorem AlgebraicGeometry.exists_lift_of_germInjective_aux {X : AlgebraicGeometry.Scheme} {R : CommRingCat} {A : CommRingCat} {U : X.Opens} {x : ↑↑X.toPresheafedSpace} (hxU : x ∈ U) (φ : A ⟶ X.presheaf.stalk x) (φRA : R ⟶ A) (φRX : R ⟶ X.presheaf.obj (Opposite.op U)) (hφRA : RingHom.FiniteType φRA) (e : CategoryTheory.CategoryStruct.comp φRA φ = CategoryTheory.CategoryStruct.comp φRX (X.presheaf.germ U x hxU)) : ∃ (V : X.Opens) (hxV : x ∈ V), V ≤ U ∧ RingHom.range φ ≤ RingHom.range (X.presheaf.germ V x hxV)

theorem AlgebraicGeometry.exists_lift_of_germInjective {X : AlgebraicGeometry.Scheme} {R : CommRingCat} {A : CommRingCat} {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] {U : X.Opens} (hxU : x ∈ U) (φ : A ⟶ X.presheaf.stalk x) (φRA : R ⟶ A) (φRX : R ⟶ X.presheaf.obj (Opposite.op U)) (hφRA : RingHom.FiniteType φRA) (e : CategoryTheory.CategoryStruct.comp φRA φ = CategoryTheory.CategoryStruct.comp φRX (X.presheaf.germ U x hxU)) : ∃ (V : X.Opens) (hxV : x ∈ V) (φ' : A ⟶ X.presheaf.obj (Opposite.op V)) (i : V ≤ U), AlgebraicGeometry.IsAffineOpen V ∧ φ = CategoryTheory.CategoryStruct.comp φ' (X.presheaf.germ V x hxV) ∧ CategoryTheory.CategoryStruct.comp φRX (X.presheaf.map i.hom.op) = CategoryTheory.CategoryStruct.comp φRA φ'

Suppose X is a scheme, x : X such that the germ map at x is (locally) injective, and U is a neighborhood of x. Given a commutative diagram of CommRingCat

R ⟶ Γ(X, U)
↓    ↓
A ⟶ 𝒪_{X, x}

such that R is of finite type over A, we may lift A ⟶ 𝒪_{X, x} to some A ⟶ Γ(X, V).

theorem AlgebraicGeometry.spread_out_of_isGermInjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] {y : ↑↑Y.toPresheafedSpace} (e : sX.base x = sY.base y) (φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x) (h : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap sY y) φ = CategoryTheory.CategoryStruct.comp (S.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap sX x)) : ∃ (U : X.Opens) (hxU : x ∈ U) (f : ↑U ⟶ Y), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) (Y.fromSpecStalk y) = CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧ CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ι sX

Given S-schemes X Y and points x : X y : Y over s : S. Suppose we have the following diagram of S-schemes

Spec 𝒪_{X, x} ⟶ X
    |
  Spec(φ)
    ↓
Spec 𝒪_{Y, y} ⟶ Y

Then the map Spec(φ) spreads out to an S-morphism on an open subscheme U ⊆ X,

Spec 𝒪_{X, x} ⟶ U ⊆ X
    |             |
  Spec(φ)         |
    ↓             ↓
Spec 𝒪_{Y, y} ⟶ Y

provided that Y is locally of finite type over S and X is "germ-injective" at x (e.g. when it's integral or locally noetherian).

TODO: The condition on X is unnecessary when Y is locally of finite presentation.

theorem AlgebraicGeometry.spread_out_of_isGermInjective' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX) : ∃ (U : X.Opens) (hxU : x ∈ U) (f : ↑U ⟶ Y), φ = CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧ CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ι sX

Given S-schemes X Y, a point x : X, and a S-morphism φ : Spec 𝒪_{X, x} ⟶ Y, we may spread it out to an S-morphism f : U ⟶ Y provided that Y is locally of finite type over S and X is "germ-injective" at x (e.g. when it's integral or locally noetherian).

TODO: The condition on X is unnecessary when Y is locally of finite presentation.