Scheme compactifications

A compactification of a scheme morphism is a factorization through a quasi-compact open immersion followed by a proper morphism. Morphisms fix the source and lie over the base. We realize this category as a full subcategory of Mathlib's CategoryTheory.Factorisation, so its morphisms and category laws are inherited rather than reconstructed. As in the Stacks Project's category of compactifications, density is not required. These definitions impose no quasi-compactness or quasi-separatedness condition on the base. Being a compactification is invariant under isomorphism of factorizations, and an isomorphism of ambient schemes compatible with both maps is an isomorphism of compactifications (Compactification.isoMk).

The dense compactifications form the further full subcategory where the open immersion is scheme-theoretically dominant. This condition retains the scheme structure, including nilpotents. No existence theorem or reducedness assumption is part of these definitions. Every map from a dense compactification lifts along a closed immersion of compactifications (Compactification.liftOfIsClosedImmersion).

References

• The Stacks Project, Section 38.32, Compactifications (tag 0ATT).

def TauCeti.compactificationProperty {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : CategoryTheory.ObjectProperty (CategoryTheory.Factorisation f)

Factorizations with a quasi-compact open first map and proper second map.

@[simp]

theorem TauCeti.compactificationProperty_iff {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (C : CategoryTheory.Factorisation f) : compactificationProperty f C ↔ AlgebraicGeometry.IsOpenImmersion C.ι ∧ AlgebraicGeometry.QuasiCompact C.ι ∧ AlgebraicGeometry.IsProper C.π

@[reducible, inline]

abbrev TauCeti.Compactification {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : Type (u + 1)

Compactifications of f, with maps fixing X and lying over S.

@[reducible, inline]

abbrev TauCeti.Compactification.Xbar {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.Scheme

The ambient proper scheme of a compactification.

@[reducible, inline]

abbrev TauCeti.Compactification.j {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : X ⟶ C.Xbar

The open immersion of the source into its compactification.

@[reducible, inline]

abbrev TauCeti.Compactification.p {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : C.Xbar ⟶ S

The proper structure map of a compactification.

instance TauCeti.Compactification.instIsOpenImmersionJ {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.IsOpenImmersion C.j

instance TauCeti.Compactification.instQuasiCompactJ {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.QuasiCompact C.j

instance TauCeti.Compactification.instIsProperP {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.IsProper C.p

@[reducible, inline]

abbrev TauCeti.Compactification.ofHom {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {Y : AlgebraicGeometry.Scheme} (j : X ⟶ Y) (p : Y ⟶ S) [AlgebraicGeometry.IsOpenImmersion j] [AlgebraicGeometry.QuasiCompact j] [AlgebraicGeometry.IsProper p] (fac : CategoryTheory.CategoryStruct.comp j p = f) : Compactification f

Bundle a quasi-compact open immersion and a proper map as a compactification.

@[simp]

theorem TauCeti.Compactification.ofHom_obj_ι {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {Y : AlgebraicGeometry.Scheme} (j : X ⟶ Y) (p : Y ⟶ S) [AlgebraicGeometry.IsOpenImmersion j] [AlgebraicGeometry.QuasiCompact j] [AlgebraicGeometry.IsProper p] (fac : CategoryTheory.CategoryStruct.comp j p = f) : (ofHom j p fac).obj.ι = j

@[simp]

theorem TauCeti.Compactification.ofHom_obj_mid {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {Y : AlgebraicGeometry.Scheme} (j : X ⟶ Y) (p : Y ⟶ S) [AlgebraicGeometry.IsOpenImmersion j] [AlgebraicGeometry.QuasiCompact j] [AlgebraicGeometry.IsProper p] (fac : CategoryTheory.CategoryStruct.comp j p = f) : (ofHom j p fac).obj.mid = Y

@[simp]

theorem TauCeti.Compactification.ofHom_obj_π {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {Y : AlgebraicGeometry.Scheme} (j : X ⟶ Y) (p : Y ⟶ S) [AlgebraicGeometry.IsOpenImmersion j] [AlgebraicGeometry.QuasiCompact j] [AlgebraicGeometry.IsProper p] (fac : CategoryTheory.CategoryStruct.comp j p = f) : (ofHom j p fac).obj.π = p

@[reducible, inline]

noncomputable abbrev TauCeti.Compactification.localizationAway {R : CommRingCat} (r : ↑R) : Compactification (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))))

The tautological compactification of a principal affine open, over its ambient spectrum.

theorem TauCeti.Compactification.isSchemeTheoreticallyDominant_localizationAway {R : CommRingCat} (r : ↑R) (hr : IsRegular r) : AlgebraicGeometry.IsSchemeTheoreticallyDominant (localizationAway r).j

Localizing at a non-zero-divisor gives a schematically dense interior; the ring need not be reduced.

@[reducible, inline]

abbrev TauCeti.Compactification.Hom {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C D : Compactification f) : Type (u + 1)

A morphism of compactifications fixes the source and lies over the base.

instance TauCeti.Compactification.Hom.proper {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (h : C.Hom D) : AlgebraicGeometry.IsProper h.hom.h

Every morphism of compactifications is proper.

theorem TauCeti.Compactification.Hom.mono_of_mono_h {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (h : C.Hom D) [CategoryTheory.Mono h.hom.h] : CategoryTheory.Mono h

A morphism of compactifications is a monomorphism when its map of ambient schemes is.

instance TauCeti.Compactification.Hom.instMonoOfIsClosedImmersionHSchemeHomFullSubcategoryFactorisationCompactificationProperty {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (h : C.Hom D) [AlgebraicGeometry.IsClosedImmersion h.hom.h] : CategoryTheory.Mono h

instance TauCeti.Compactification.Hom.isIso_hom_h {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (h : C.Hom D) [CategoryTheory.IsIso h] : CategoryTheory.IsIso h.hom.h

The map of ambient schemes underlying an isomorphism of compactifications is an isomorphism.

def TauCeti.Compactification.isoMk {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (e : C.Xbar ≅ D.Xbar) (hj : CategoryTheory.CategoryStruct.comp C.j e.hom = D.j) (hp : CategoryTheory.CategoryStruct.comp e.hom D.p = C.p) : C ≅ D

An isomorphism of ambient schemes fixing the source and lying over the base is an isomorphism of compactifications.

@[simp]

theorem TauCeti.Compactification.isoMk_hom_hom_h {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (e : C.Xbar ≅ D.Xbar) (hj : CategoryTheory.CategoryStruct.comp C.j e.hom = D.j) (hp : CategoryTheory.CategoryStruct.comp e.hom D.p = C.p) : (isoMk e hj hp).hom.hom.h = e.hom

@[simp]

theorem TauCeti.Compactification.isoMk_inv_hom_h {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (e : C.Xbar ≅ D.Xbar) (hj : CategoryTheory.CategoryStruct.comp C.j e.hom = D.j) (hp : CategoryTheory.CategoryStruct.comp e.hom D.p = C.p) : (isoMk e hj hp).inv.hom.h = e.inv

theorem TauCeti.Compactification.isSeparated {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.IsSeparated f

A compactifiable morphism is separated.

theorem TauCeti.Compactification.locallyOfFiniteType {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.LocallyOfFiniteType f

A compactifiable morphism is locally of finite type.

theorem TauCeti.Compactification.quasiCompact {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) : AlgebraicGeometry.QuasiCompact f

A compactifiable morphism is quasi-compact.

@[reducible, inline]

abbrev TauCeti.Compactification.identity {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] : Compactification f

The identity compactification of a proper morphism.

noncomputable def TauCeti.Compactification.isInitialIdentity {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] : CategoryTheory.Limits.IsInitial (identity f)

The identity compactification is initial: its map to any compactification is the specified open immersion.

@[simp]

theorem TauCeti.Compactification.isInitialIdentity_to_hom_h {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] (C : Compactification f) : ((isInitialIdentity f).to C).hom.h = C.j

instance TauCeti.instIsClosedUnderIsomorphismsFactorisationSchemeCompactificationProperty {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : (compactificationProperty f).IsClosedUnderIsomorphisms

Being a compactification is invariant under isomorphism of factorizations.

def TauCeti.denseCompactificationProperty {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : CategoryTheory.ObjectProperty (Compactification f)

Scheme-theoretic density of the interior of a compactification.

@[simp]

theorem TauCeti.denseCompactificationProperty_iff {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (C : Compactification f) : denseCompactificationProperty f C ↔ AlgebraicGeometry.IsSchemeTheoreticallyDominant C.j

instance TauCeti.instIsClosedUnderIsomorphismsCompactificationDenseCompactificationProperty {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : (denseCompactificationProperty f).IsClosedUnderIsomorphisms

Schematic density of the interior is invariant under isomorphism of compactifications.

@[reducible, inline]

abbrev TauCeti.DenseCompactification {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : Type (u + 1)

The full subcategory of compactifications with scheme-theoretically dense interior.

instance TauCeti.DenseCompactification.instIsSchemeTheoreticallyDominantJObjCompactificationDenseCompactificationProperty {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : DenseCompactification f) : AlgebraicGeometry.IsSchemeTheoreticallyDominant C.obj.j

@[reducible, inline]

abbrev TauCeti.DenseCompactification.identity {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsProper f] : DenseCompactification f

A proper morphism has a dense identity compactification.

@[simp]

theorem TauCeti.DenseCompactification.identity_obj {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} [AlgebraicGeometry.IsProper f] : identity.obj = Compactification.identity f

noncomputable def TauCeti.Compactification.liftOfIsClosedImmersion {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (φ : D ⟶ C) [AlgebraicGeometry.IsClosedImmersion φ.hom.h] (E : DenseCompactification f) (h : E.obj ⟶ C) : E.obj ⟶ D

A map out of a dense compactification into C lifts along a closed immersion φ : D ⟶ C of compactifications: the interior of E is scheme-theoretically dense and lands in the closed subscheme D.Xbar of C.Xbar.

@[simp]

theorem TauCeti.Compactification.liftOfIsClosedImmersion_comp {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (φ : D ⟶ C) [AlgebraicGeometry.IsClosedImmersion φ.hom.h] (E : DenseCompactification f) (h : E.obj ⟶ C) : CategoryTheory.CategoryStruct.comp (liftOfIsClosedImmersion φ E h) φ = h

@[simp]

theorem TauCeti.Compactification.liftOfIsClosedImmersion_comp_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (φ : D ⟶ C) [AlgebraicGeometry.IsClosedImmersion φ.hom.h] (E : DenseCompactification f) (h : E.obj ⟶ C) {Z : Compactification f} (h✝ : C ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftOfIsClosedImmersion φ E h) (CategoryTheory.CategoryStruct.comp φ h✝) = CategoryTheory.CategoryStruct.comp h h✝

@[simp]

theorem TauCeti.Compactification.liftOfIsClosedImmersion_hom_h_comp {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (φ : D ⟶ C) [AlgebraicGeometry.IsClosedImmersion φ.hom.h] (E : DenseCompactification f) (h : E.obj ⟶ C) : CategoryTheory.CategoryStruct.comp (liftOfIsClosedImmersion φ E h).hom.h φ.hom.h = h.hom.h

@[simp]

theorem TauCeti.Compactification.liftOfIsClosedImmersion_hom_h_comp_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} (φ : D ⟶ C) [AlgebraicGeometry.IsClosedImmersion φ.hom.h] (E : DenseCompactification f) (h : E.obj ⟶ C) {Z : AlgebraicGeometry.Scheme} (h✝ : C.obj.mid ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftOfIsClosedImmersion φ E h).hom.h (CategoryTheory.CategoryStruct.comp φ.hom.h h✝) = CategoryTheory.CategoryStruct.comp h.hom.h h✝

theorem TauCeti.Compactification.app_p_eq_zero_iff {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C : Compactification f) [AlgebraicGeometry.IsSchemeTheoreticallyDominant C.j] {U : S.Opens} (s : ↑(S.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app C.p U)) s = 0 ↔ (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) s = 0

Over a schematically dense interior, a section of the base vanishes on the ambient scheme exactly when it vanishes on the source. In particular nilpotent sections pulled back from the base are not lost.