Common refinements of scheme compactifications

Two compactifications C₁, C₂ of f : X ⟶ S have a common dense refinement: the scheme-theoretic closure of X in C₁.Xbar ×_S C₂.Xbar. The map of X into the fibre product is an immersion, because its composite with the first projection is the open immersion C₁.j. It is quasi-compact, because that projection is separated. Hence X is a quasi-compact open subscheme of its scheme-theoretic closure, which is proper over S as a closed subscheme of a fibre product of proper schemes.

A dense compactification with maps to C₁ and C₂ factors uniquely through the refinement, so the refinement is the binary product in the category of dense compactifications. Iterating gives a dense compactification refining any nonempty finite family of compactifications. No hypotheses on S or f are needed for these constructions.

Main declarations

• TauCeti.Compactification.toPullback: the immersion of X into C₁.Xbar ×_S C₂.Xbar.
• TauCeti.Compactification.commonRefinement: the dense compactification given by the scheme-theoretic closure of X in C₁.Xbar ×_S C₂.Xbar.
• TauCeti.Compactification.commonRefinementFst, TauCeti.Compactification.commonRefinementSnd: its maps to C₁ and C₂.
• TauCeti.Compactification.commonRefinementLift: the factorization of a dense compactification mapping to C₁ and C₂.
• TauCeti.DenseCompactification.isLimitCommonRefinementFan: the common refinement is the binary product of dense compactifications.
• TauCeti.Compactification.exists_forall_nonempty_hom: a nonempty finite family of compactifications has a dense common refinement.

References

• The Stacks Project, Lemma 38.32.1 (tag 0ATU), Compactifications.
• The Stacks Project, Section 29.6, Scheme theoretic image (tag 01R5).
• The Stacks Project, Section 29.7, Scheme theoretic closure and density (tag 01RB).

noncomputable def TauCeti.Compactification.toPullback {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : X ⟶ CategoryTheory.Limits.pullback C₁.p C₂.p

The map of the source into the fibre product of two compactifications over the base.

@[simp]

theorem TauCeti.Compactification.toPullback_fst {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : CategoryTheory.CategoryStruct.comp (C₁.toPullback C₂) (CategoryTheory.Limits.pullback.fst C₁.p C₂.p) = C₁.j

@[simp]

theorem TauCeti.Compactification.toPullback_fst_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) {Z : AlgebraicGeometry.Scheme} (h : C₁.Xbar ⟶ Z) : CategoryTheory.CategoryStruct.comp (C₁.toPullback C₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst C₁.p C₂.p) h) = CategoryTheory.CategoryStruct.comp C₁.j h

@[simp]

theorem TauCeti.Compactification.toPullback_snd {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : CategoryTheory.CategoryStruct.comp (C₁.toPullback C₂) (CategoryTheory.Limits.pullback.snd C₁.p C₂.p) = C₂.j

@[simp]

theorem TauCeti.Compactification.toPullback_snd_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) {Z : AlgebraicGeometry.Scheme} (h : C₂.Xbar ⟶ Z) : CategoryTheory.CategoryStruct.comp (C₁.toPullback C₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd C₁.p C₂.p) h) = CategoryTheory.CategoryStruct.comp C₂.j h

instance TauCeti.Compactification.isImmersion_toPullback {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : AlgebraicGeometry.IsImmersion (C₁.toPullback C₂)

The source is an immersion into the fibre product of two compactifications.

instance TauCeti.Compactification.quasiCompact_toPullback {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : AlgebraicGeometry.QuasiCompact (C₁.toPullback C₂)

The immersion of the source into the fibre product is quasi-compact, since the first projection is separated.

@[implicit_reducible]

noncomputable def TauCeti.Compactification.commonRefinement {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : DenseCompactification f

The common refinement of two compactifications: the scheme-theoretic closure of the source in the fibre product of their ambient schemes over the base.

@[simp]

theorem TauCeti.Compactification.commonRefinement_Xbar {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinement C₂).obj.Xbar = AlgebraicGeometry.Scheme.Hom.image (C₁.toPullback C₂)

@[simp]

theorem TauCeti.Compactification.commonRefinement_j {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinement C₂).obj.j = AlgebraicGeometry.Scheme.Hom.toImage (C₁.toPullback C₂)

@[simp]

theorem TauCeti.Compactification.commonRefinement_p {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinement C₂).obj.p = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι (C₁.toPullback C₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst C₁.p C₂.p) C₁.p)

noncomputable def TauCeti.Compactification.commonRefinementFst {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinement C₂).obj ⟶ C₁

The map from the common refinement to the first compactification.

noncomputable def TauCeti.Compactification.commonRefinementSnd {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinement C₂).obj ⟶ C₂

The map from the common refinement to the second compactification.

@[simp]

theorem TauCeti.Compactification.commonRefinementFst_hom_h {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinementFst C₂).hom.h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι (C₁.toPullback C₂)) (CategoryTheory.Limits.pullback.fst C₁.p C₂.p)

@[simp]

theorem TauCeti.Compactification.commonRefinementSnd_hom_h {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (C₁ C₂ : Compactification f) : (C₁.commonRefinementSnd C₂).hom.h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι (C₁.toPullback C₂)) (CategoryTheory.Limits.pullback.snd C₁.p C₂.p)

theorem TauCeti.Compactification.commonRefinement_hom_ext {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ D : Compactification f} {g g' : D ⟶ (C₁.commonRefinement C₂).obj} (h₁ : CategoryTheory.CategoryStruct.comp g (C₁.commonRefinementFst C₂) = CategoryTheory.CategoryStruct.comp g' (C₁.commonRefinementFst C₂)) (h₂ : CategoryTheory.CategoryStruct.comp g (C₁.commonRefinementSnd C₂) = CategoryTheory.CategoryStruct.comp g' (C₁.commonRefinementSnd C₂)) : g = g'

Maps into the common refinement are determined by their composites with both projections. No density of the source is needed.

noncomputable def TauCeti.Compactification.commonRefinementLift {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) : E.obj ⟶ (C₁.commonRefinement C₂).obj

A dense compactification mapping to C₁ and C₂ factors through their common refinement: its interior is scheme-theoretically dense, so its map to the fibre product lands in the scheme-theoretic closure of the source.

@[simp]

theorem TauCeti.Compactification.commonRefinementLift_hom_h_imageι {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) : CategoryTheory.CategoryStruct.comp (commonRefinementLift E h₁ h₂).hom.h (AlgebraicGeometry.Scheme.Hom.imageι (C₁.toPullback C₂)) = CategoryTheory.Limits.pullback.lift h₁.hom.h h₂.hom.h ⋯

On ambient schemes, the factorization through the common refinement followed by the closed immersion into the fibre product is the pair of the given maps.

@[simp]

theorem TauCeti.Compactification.commonRefinementLift_hom_h_imageι_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback C₁.p C₂.p ⟶ Z) : CategoryTheory.CategoryStruct.comp (commonRefinementLift E h₁ h₂).hom.h (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι (C₁.toPullback C₂)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h₁.hom.h h₂.hom.h ⋯) h

On ambient schemes, the factorization through the common refinement followed by the closed immersion into the fibre product is the pair of the given maps.

@[simp]

theorem TauCeti.Compactification.commonRefinementLift_fst {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) : CategoryTheory.CategoryStruct.comp (commonRefinementLift E h₁ h₂) (C₁.commonRefinementFst C₂) = h₁

@[simp]

theorem TauCeti.Compactification.commonRefinementLift_fst_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) {Z : Compactification f} (h : C₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (commonRefinementLift E h₁ h₂) (CategoryTheory.CategoryStruct.comp (C₁.commonRefinementFst C₂) h) = CategoryTheory.CategoryStruct.comp h₁ h

@[simp]

theorem TauCeti.Compactification.commonRefinementLift_snd {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) : CategoryTheory.CategoryStruct.comp (commonRefinementLift E h₁ h₂) (C₁.commonRefinementSnd C₂) = h₂

@[simp]

theorem TauCeti.Compactification.commonRefinementLift_snd_assoc {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C₁ C₂ : Compactification f} (E : DenseCompactification f) (h₁ : E.obj ⟶ C₁) (h₂ : E.obj ⟶ C₂) {Z : Compactification f} (h : C₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (commonRefinementLift E h₁ h₂) (CategoryTheory.CategoryStruct.comp (C₁.commonRefinementSnd C₂) h) = CategoryTheory.CategoryStruct.comp h₂ h

theorem TauCeti.Compactification.exists_forall_nonempty_hom {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {ι : Type u_1} [Finite ι] [Nonempty ι] (C : ι → Compactification f) : ∃ (E : DenseCompactification f), ∀ (i : ι), Nonempty (E.obj ⟶ C i)

Every nonempty finite family of compactifications has a dense common refinement.

@[reducible, inline]

noncomputable abbrev TauCeti.DenseCompactification.commonRefinementFan {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (D₁ D₂ : DenseCompactification f) : CategoryTheory.Limits.BinaryFan D₁ D₂

The binary fan of dense compactifications given by the common refinement.

noncomputable def TauCeti.DenseCompactification.isLimitCommonRefinementFan {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} (D₁ D₂ : DenseCompactification f) : CategoryTheory.Limits.IsLimit (D₁.commonRefinementFan D₂)

The common refinement is the binary product in the category of dense compactifications.

instance TauCeti.DenseCompactification.instHasBinaryProducts {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} : CategoryTheory.Limits.HasBinaryProducts (DenseCompactification f)