Separatedness from an open cover of the source

A morphism f : X ⟶ S is separated when its diagonal X ⟶ X ×_S X is a closed immersion. Given an open cover {Uᵢ} of X, the products Uᵢ ×_S Uⱼ cover X ×_S X, and the diagonal restricted over Uᵢ ×_S Uⱼ is the canonical map Uᵢ ×_X Uⱼ ⟶ Uᵢ ×_S Uⱼ from the intersection of the two pieces (pullback.mapDesc). Over Uᵢ ×_S Uᵢ this map is the diagonal of Uᵢ ⟶ S. So f is separated as soon as each piece is separated over S and the maps Uᵢ ×_X Uⱼ ⟶ Uᵢ ×_S Uⱼ for distinct pieces are closed immersions. When the pieces and S are affine and Uᵢ ×_X Uⱼ is affine, the latter is the classical condition that the functions on Uᵢ and Uⱼ generate the functions on the intersection.

This is the shape of Mathlib's proof that Proj is separated (AlgebraicGeometry.Proj.isSeparated), with the computation on its affine charts abstracted away. Mathlib's AffineTargetMorphismProperty.diagonal_of_openCover_source is the analogue for an affine target and affine pieces, phrased for affine-target properties and asking for every pair of pieces; here the target is arbitrary, and the pairs of equal pieces are replaced by the separatedness of each piece over the target. It is the criterion used to show that a scheme glued from two affine charts, such as the two-chart model of an algebraic function field, is separated.

Separated morphisms compose, so a scheme separated over a separated scheme is itself separated; in particular a scheme proper over a separated base, such as a field, is a separated scheme.

Main results

• AlgebraicGeometry.IsSeparated.of_openCover: f is separated if each piece of an open cover of its source is separated over the target and the pieces meet in closed subschemes of their products over the target.
• AlgebraicGeometry.Scheme.IsSeparated.of_isSeparated: the source of a separated morphism to a separated scheme is a separated scheme.
• AlgebraicGeometry.isAffineHom_hasOfPostcompProperty: since affine morphisms are separated, f is affine whenever f ≫ g and g are; this gives finite limits of affine schemes over a base, computed in schemes.

theorem AlgebraicGeometry.IsSeparated.of_openCover {X S : Scheme} (f : X ⟶ S) (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), IsSeparated (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)] (H : ∀ (i j : 𝒰.I₀), i ≠ j → IsClosedImmersion (CategoryTheory.Limits.pullback.mapDesc (𝒰.f i) (𝒰.f j) f)) : IsSeparated f

Separatedness from an open cover of the source. If every piece Uᵢ of an open cover of X is separated over S, and for distinct pieces the canonical map Uᵢ ×_X Uⱼ ⟶ Uᵢ ×_S Uⱼ is a closed immersion, then f : X ⟶ S is separated.

theorem AlgebraicGeometry.Scheme.IsSeparated.of_isSeparated {X S : Scheme} (f : X ⟶ S) [IsSeparated f] [S.IsSeparated] : X.IsSeparated

A scheme separated over a separated scheme is separated. If f : X ⟶ S is separated and S is a separated scheme, then so is X, since X ⟶ ⊤_ Scheme factors as f followed by the separated morphism S ⟶ ⊤_ Scheme. For instance, a scheme proper over a field is separated.

instance AlgebraicGeometry.isAffineHom_hasOfPostcompProperty : CategoryTheory.MorphismProperty.HasOfPostcompProperty @IsAffineHom @IsAffineHom

If f ≫ g and g are affine, then so is f, because affine morphisms are separated.