class ChowLemma.IsProper (X : AlgebraicGeometry.Scheme) : Prop

A scheme is proper (as an abstract property) when it is equipped with a proper morphism to some base scheme S.

• exists_proper_morphism : ∃ (S : AlgebraicGeometry.Scheme) (f : X ⟶ S), AlgebraicGeometry.IsProper f

def ChowLemma.IsProjective (X : AlgebraicGeometry.Scheme) : Prop

A scheme is projective when it embeds as a closed subscheme of some Proj 𝒜.

def ChowLemma.Birational (X Y : AlgebraicGeometry.Scheme) : Prop

Two schemes are birational when they share a common dense open subscheme.

theorem ChowLemma.chow_lemma (X : AlgebraicGeometry.Scheme) [IsProper X] [AlgebraicGeometry.IsIntegral X] : ∃ (X' : AlgebraicGeometry.Scheme), IsProjective X' ∧ Birational X' X

Chow's lemma (Lem 20, Lec 9): a complete irreducible variety is birational to a projective variety.