class AlgebraicGeometry.IsAlgebraicVariety {S : Scheme} (X : Scheme) [X.Over S] [IsLocallyNoetherian S] : Prop

A scheme X is an algebraic variety over a locally Noetherian base S if it is reduced, separated, of locally finite type and quasi-compact over S.

• isReduced : IsReduced X
• isSeparated : X.IsSeparated
• locallyOfFiniteType : LocallyOfFiniteType (X ↘ S)
• quasiCompact : QuasiCompact (X ↘ S)

@[implicit_reducible]

instance AlgebraicGeometry.openSubschemeOver {S : Scheme} (X : Scheme) [X.Over S] (U : X.Opens) : (↑U).Over S

An open subscheme inherits the structure morphism to S via composition with the inclusion U ↪ X.

instance AlgebraicGeometry.isReduced_openSubscheme (X : Scheme) [IsReduced X] (U : X.Opens) : IsReduced ↑U

Open subschemes of reduced schemes are reduced.

theorem AlgebraicGeometry.isSeparated_openSubscheme (X : Scheme) [X.IsSeparated] (U : X.Opens) : (↑U).IsSeparated

Separatedness descends to open subschemes.

theorem AlgebraicGeometry.locallyOfFiniteType_openSubscheme {S : Scheme} (X : Scheme) [X.Over S] (U : X.Opens) [LocallyOfFiniteType (X ↘ S)] : LocallyOfFiniteType (↑U ↘ S)

Local finite type descends to open subschemes.

theorem AlgebraicGeometry.quasiCompact_openSubscheme {S : Scheme} (X : Scheme) [X.Over S] (U : X.Opens) [IsLocallyNoetherian S] [LocallyOfFiniteType (X ↘ S)] [QuasiCompact (X ↘ S)] : QuasiCompact (↑U ↘ S)

Quasi-compactness over S descends to open subschemes when X is locally Noetherian of finite type over S.

theorem AlgebraicGeometry.isAlgebraicVariety_openSubscheme {S : Scheme} (X : Scheme) [X.Over S] [IsLocallyNoetherian S] [hX : IsAlgebraicVariety X] (U : X.Opens) : IsAlgebraicVariety ↑U

An open subscheme of an algebraic variety is again an algebraic variety (Corollary 4, Lecture 2).