def ChowHelperBlowupProjective.IsBirational (X Y : AlgebraicGeometry.Scheme) : Prop

Two schemes are birational when they share a common dense open Z, i.e. there exist open immersions f : Z ↪ X and g : Z ↪ Y with dense images.

def ChowHelperBlowupProjective.IsProjectiveScheme (X : AlgebraicGeometry.Scheme) : Prop

A scheme is projective if it admits a closed immersion into some Proj 𝒜 for a finitely-generated graded (𝒜 0)-algebra.

theorem ChowHelperBlowupProjective.exists_projective_completion (U : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine U] : ∃ (Y : AlgebraicGeometry.Scheme), IsProjectiveScheme Y ∧ ∃ (ι : U ⟶ Y), AlgebraicGeometry.IsOpenImmersion ι ∧ Dense (Set.range ⇑ι)

Every affine scheme admits a projective completion: there is a projective scheme Y and an open immersion U ↪ Y with dense image.

theorem ChowHelperBlowupProjective.graph_closure_projective_birational {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.IsIntegral X] : ∃ (X' : AlgebraicGeometry.Scheme), IsProjectiveScheme X' ∧ IsBirational X X'

The graph-closure construction: given a proper morphism f : X → S with integral domain, the closure of the graph yields a projective scheme X' birational to X. This is the geometric heart of Chow's lemma.

theorem ChowHelperBlowupProjective.chow_helper_blowup_projective {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.IsIntegral X] : ∃ (X' : AlgebraicGeometry.Scheme) (_ : IsProjectiveScheme X'), IsBirational X X'

Chow's lemma helper: for any proper morphism X → S with integral X, there is a projective scheme X' birational to X.

theorem ChowHelperBlowupProjective.isBirational_refl (X : AlgebraicGeometry.Scheme) : IsBirational X X

Birationality is reflexive: every scheme is birational to itself via the identity.

theorem ChowHelperBlowupProjective.isBirational_symm {X Y : AlgebraicGeometry.Scheme} (h : IsBirational X Y) : IsBirational Y X

Birationality is symmetric: swap the roles of X and Y in the witnessing common open.