Documentation

TauCeti.AlgebraicGeometry.Compactification.Closure

Scheme-theoretic closures of quasi-compact immersions as compactifications #

Let i : X ⟶ Y be a quasi-compact immersion and q : Y ⟶ S a proper morphism. Then X is a quasi-compact open subscheme of the scheme-theoretic image of i, and that image is proper over S as a closed subscheme of Y. So the scheme-theoretic closure of X in Y is a dense compactification of i ≫ q (TauCeti.DenseCompactification.ofImmersion). It keeps the full scheme structure of X, including nilpotents. Every dense compactification whose ambient scheme maps to Y compatibly with i and q maps to it (TauCeti.DenseCompactification.ofImmersionLift), and such a map is unique because dense compactifications form a thin category.

This construction is shared by the dense replacement of a compactification C (the case i = C.j, q = C.p), the common refinement of two compactifications (the immersion of X into the fibre product of their ambient schemes) and the compactifications induced along quasi-compact immersions.

Main declarations #

References #

source
@[implicit_reducible]
noncomputable def TauCeti.DenseCompactification.ofImmersion {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (i : X ⟶ Y) [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] (q : Y ⟶ S) [AlgebraicGeometry.IsProper q] (w : CategoryTheory.CategoryStruct.comp i q = f) :
DenseCompactification f

The scheme-theoretic image of a quasi-compact immersion i : X ⟶ Y into a proper S-scheme q : Y ⟶ S, as a dense compactification of f = i ≫ q.

Instances For
    source
    @[simp]
    theorem TauCeti.DenseCompactification.ofImmersion_obj_Xbar {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (i : X ⟶ Y) [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] (q : Y ⟶ S) [AlgebraicGeometry.IsProper q] (w : CategoryTheory.CategoryStruct.comp i q = f) :
    (ofImmersion i q w).obj.Xbar = AlgebraicGeometry.Scheme.Hom.image i
    source
    @[simp]
    theorem TauCeti.DenseCompactification.ofImmersion_obj_j {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (i : X ⟶ Y) [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] (q : Y ⟶ S) [AlgebraicGeometry.IsProper q] (w : CategoryTheory.CategoryStruct.comp i q = f) :
    (ofImmersion i q w).obj.j = AlgebraicGeometry.Scheme.Hom.toImage i
    source
    @[simp]
    theorem TauCeti.DenseCompactification.ofImmersion_obj_p {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (i : X ⟶ Y) [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] (q : Y ⟶ S) [AlgebraicGeometry.IsProper q] (w : CategoryTheory.CategoryStruct.comp i q = f) :
    (ofImmersion i q w).obj.p = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι i) q
    source
    noncomputable def TauCeti.DenseCompactification.ofImmersionLift {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {i : X ⟶ Y} [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] {q : Y ⟶ S} [AlgebraicGeometry.IsProper q] {w : CategoryTheory.CategoryStruct.comp i q = f} (E : DenseCompactification f) (h : E.obj.Xbar ⟶ Y) (hj : CategoryTheory.CategoryStruct.comp E.obj.j h = i) (hp : CategoryTheory.CategoryStruct.comp h q = E.obj.p) :
    E ⟶ ofImmersion i q w

    A dense compactification E of f maps to the scheme-theoretic closure of i, given a map h from its ambient scheme to Y which restricts to i on X and lies over S. Its interior is scheme-theoretically dense, so h factors through the closed subscheme.

    Instances For
      source
      @[simp]
      theorem TauCeti.DenseCompactification.ofImmersionLift_hom_hom_h_imageι {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {i : X ⟶ Y} [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] {q : Y ⟶ S} [AlgebraicGeometry.IsProper q] {w : CategoryTheory.CategoryStruct.comp i q = f} (E : DenseCompactification f) (h : E.obj.Xbar ⟶ Y) (hj : CategoryTheory.CategoryStruct.comp E.obj.j h = i) (hp : CategoryTheory.CategoryStruct.comp h q = E.obj.p) :
      CategoryTheory.CategoryStruct.comp (E.ofImmersionLift h hj hp).hom.hom.h (AlgebraicGeometry.Scheme.Hom.imageι i) = h

      On ambient schemes, the map to the closure of i followed by the closed immersion into Y is the given map.

      source
      @[simp]
      theorem TauCeti.DenseCompactification.ofImmersionLift_hom_hom_h_imageι_assoc {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {i : X ⟶ Y} [AlgebraicGeometry.IsImmersion i] [AlgebraicGeometry.QuasiCompact i] {q : Y ⟶ S} [AlgebraicGeometry.IsProper q] {w : CategoryTheory.CategoryStruct.comp i q = f} (E : DenseCompactification f) (h : E.obj.Xbar ⟶ Y) (hj : CategoryTheory.CategoryStruct.comp E.obj.j h = i) (hp : CategoryTheory.CategoryStruct.comp h q = E.obj.p) {Z : AlgebraicGeometry.Scheme} (h✝ : Y ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (E.ofImmersionLift h hj hp).hom.hom.h (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι i) h✝) = CategoryTheory.CategoryStruct.comp h h✝

      On ambient schemes, the map to the closure of i followed by the closed immersion into Y is the given map.