theorem QuasiprojectiveSeparated.separated_of_openImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [Y.IsSeparated] : X.IsSeparated

An open subscheme of a separated scheme is separated.

theorem QuasiprojectiveSeparated.separated_of_closedImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] [Y.IsSeparated] : X.IsSeparated

A closed subscheme of a separated scheme is separated.

theorem QuasiprojectiveSeparated.separated_of_locally_closed_immersion_to_separated {X Z Y : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Z ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] [AlgebraicGeometry.IsOpenImmersion g] [Y.IsSeparated] : X.IsSeparated

A scheme admitting a locally closed immersion (closed-in-open) into a separated scheme is itself separated.

class QuasiprojectiveSeparated.IsQuasiProjective (X : AlgebraicGeometry.Scheme) : Prop

Def 6 (Lec 3): X is quasi-projective if it admits a locally closed immersion into some projective scheme Proj 𝒜.

• exists_locally_closed_immersion : ∃ (σ : Type u) (A : Type u) (x : CommRing A) (x_1 : SetLike σ A) (x_2 : AddSubgroupClass σ A) (𝒜 : ℕ → σ) (x_3 : GradedRing 𝒜) (Z : AlgebraicGeometry.Scheme) (f : X ⟶ Z) (g : Z ⟶ AlgebraicGeometry.Proj 𝒜), AlgebraicGeometry.IsClosedImmersion f ∧ AlgebraicGeometry.IsOpenImmersion g

theorem QuasiprojectiveSeparated.quasiprojective_isSeparated (X : AlgebraicGeometry.Scheme) [IsQuasiProjective X] : X.IsSeparated

Cor 12 (Lec 3): every quasi-projective variety is separated, obtained by combining Proj 𝒜 separated with the locally closed immersion of Def 6.