def AlgebraicGeometry.IsComplete (X S : Scheme) [X.Over S] : Prop

Definition 19 (Lec 8): a scheme X over S is complete if its structural morphism is proper (i.e. separated, universally closed, and locally of finite type).

theorem AlgebraicGeometry.isComplete_iff (X S : Scheme) [X.Over S] : IsComplete X S ↔ IsSeparated (X ↘ S) ∧ UniversallyClosed (X ↘ S) ∧ LocallyOfFiniteType (X ↘ S)

Unfolds IsComplete to the conjunction separated ∧ universally closed ∧ locally of finite type.

theorem AlgebraicGeometry.IsComplete.mk' {X S : Scheme} [X.Over S] [IsSeparated (X ↘ S)] [UniversallyClosed (X ↘ S)] [LocallyOfFiniteType (X ↘ S)] : IsComplete X S

Constructor for IsComplete from instance arguments.

theorem AlgebraicGeometry.IsComplete.isSeparated {X S : Scheme} [X.Over S] (h : IsComplete X S) : IsSeparated (X ↘ S)

A complete scheme is separated.

theorem AlgebraicGeometry.IsComplete.universallyClosed {X S : Scheme} [X.Over S] (h : IsComplete X S) : UniversallyClosed (X ↘ S)

A complete scheme is universally closed.

theorem AlgebraicGeometry.IsComplete.locallyOfFiniteType {X S : Scheme} [X.Over S] (h : IsComplete X S) : LocallyOfFiniteType (X ↘ S)

A complete scheme is locally of finite type.