Uniqueness of maps from dense compactifications

Two maps from a compactification with schematically dense interior to any fixed compactification agree. The target need not be dense, and the source need not be reduced. Consequently, dense compactifications form a thin category: once refinement maps exist, all diagrams of such maps commute. This is the uniqueness input for comparing different compactifications coherently.

The geometric input is TauCeti.ext_of_isSchemeTheoreticallyDominant, applied to the proper, hence separated, structure map of the target compactification. Density is required only on the source: agreement on the interior does not control extra components of a nondense compactification.

References

• The Stacks Project, Section 38.32, Compactifications (tag 0ATT), and Section 29.7, Scheme theoretic closure and density (tag 01RA).

theorem TauCeti.Compactification.hom_unique {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} [AlgebraicGeometry.IsSchemeTheoreticallyDominant C.j] (h k : C ⟶ D) : h = k

Maps from a compactification with schematically dense interior to any fixed compactification are unique. No density assumption on the target is needed.

instance TauCeti.Compactification.instSubsingletonHomOfIsSchemeTheoreticallyDominantJ {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {C D : Compactification f} [AlgebraicGeometry.IsSchemeTheoreticallyDominant C.j] : Subsingleton (C ⟶ D)

instance TauCeti.DenseCompactification.instIsThin {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} : Quiver.IsThin (DenseCompactification f)

Dense compactifications have at most one refinement map between any two objects.