Separated gluing along a common open

Let i : U ⟶ X and j : U ⟶ Y be open immersions over S. The pushout glues X and Y along exactly U. If both pieces are separated over S, their gluing is separated over S if and only if U ⟶ X ×_S Y is a closed immersion. Local finite type and quasi-compactness pass from the two structure maps to the glued structure map, so separated schemes of finite type can be glued whenever their overlap is closed in their fibre product.

This criterion is used to glue modifications after arranging a closed overlap. No density, Noetherian, or quasi-compactness hypothesis on the base is needed here.

References

• The Stacks Project, Lemma 38.33.1, in Nagata compactification (Tag 0F3U).
• The Stacks Project, Section 26.14, Gluing schemes (Tag 01JA).

theorem AlgebraicGeometry.IsSeparated.pushout_desc_iff {U X Y S : Scheme} (i : U ⟶ X) (j : U ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] (f : X ⟶ S) (g : Y ⟶ S) (h : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp j g) [IsSeparated f] [IsSeparated g] : IsSeparated (CategoryTheory.Limits.pushout.desc f g h) ↔ IsClosedImmersion (CategoryTheory.Limits.pullback.lift i j h)

For open immersions i : U ⟶ X, j : U ⟶ Y over S with f, g separated, the glued morphism pushout.desc f g h is separated if and only if pullback.lift i j h : U ⟶ X ×_S Y is a closed immersion.

theorem AlgebraicGeometry.IsZariskiLocalAtSource.pushout_desc {U X Y S : Scheme} (i : U ⟶ X) (j : U ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] (f : X ⟶ S) (g : Y ⟶ S) (h : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp j g) {P : CategoryTheory.MorphismProperty Scheme} [IsZariskiLocalAtSource P] (hf : P f) (hg : P g) : P (CategoryTheory.Limits.pushout.desc f g h)

A property local at the source passes to a morphism glued from two open pieces.

theorem AlgebraicGeometry.LocallyOfFiniteType.pushout_desc {U X Y S : Scheme} (i : U ⟶ X) (j : U ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] (f : X ⟶ S) (g : Y ⟶ S) (h : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp j g) [LocallyOfFiniteType f] [LocallyOfFiniteType g] : LocallyOfFiniteType (CategoryTheory.Limits.pushout.desc f g h)

Local finite type passes to the morphism glued from two open pieces.

theorem AlgebraicGeometry.QuasiCompact.pushout_desc {U X Y S : Scheme} (i : U ⟶ X) (j : U ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] (f : X ⟶ S) (g : Y ⟶ S) (h : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp j g) [QuasiCompact f] [QuasiCompact g] : QuasiCompact (CategoryTheory.Limits.pushout.desc f g h)

Quasi-compactness passes to the morphism glued from two open pieces.