theorem coeff_finset_sum_monomial {R : Type u_1} [CommRing R] {s : Finset ℕ} {g : ℕ → R} (i : ℕ) : (∑ j ∈ s, (Polynomial.monomial j) (g j)).coeff i = if i ∈ s then g i else 0

The coefficient of a finite sum of monomials indexed by a finset s: it equals g i when i ∈ s and 0 otherwise.

theorem ChowBlowup.mem_reesAlgebra_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (I : Ideal R) (p : Polynomial R) (hp : p ∈ reesAlgebra I) : Polynomial.map f p ∈ reesAlgebra (Ideal.map f I)

A polynomial in the Rees algebra of I maps under a ring homomorphism f into the Rees algebra of the pushed-forward ideal I.map f.

theorem ChowBlowup.symm_mem_ideal_pow_of_mem_map_pow {R : Type u} {S : Type v} [CommRing R] [CommRing S] (e : R ≃+* S) (I : Ideal R) (i : ℕ) (s : S) (h : s ∈ Ideal.map (↑e) I ^ i) : e.symm s ∈ I ^ i

If s lies in (I.map e)^i for a ring isomorphism e, then e.symm s lies in I^i.

theorem ChowBlowup.mem_reesAlgebra_map_symm {R : Type u} {S : Type v} [CommRing R] [CommRing S] (e : R ≃+* S) (I : Ideal R) (q : Polynomial S) (hq : q ∈ reesAlgebra (Ideal.map (↑e) I)) : Polynomial.map (↑e.symm) q ∈ reesAlgebra I

Pulling back along the inverse of a ring isomorphism preserves membership in the Rees algebra.

noncomputable def ChowBlowup.reesAlgebra_ringEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] (e : R ≃+* S) (I : Ideal R) : ↥(reesAlgebra I) ≃+* ↥(reesAlgebra (Ideal.map (↑e) I))

A ring isomorphism e : R ≃+* S induces a ring isomorphism between the Rees algebra of I and the Rees algebra of I.map e.

noncomputable def ChowBlowup.reesAlgebra_comap_to_rees {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] (f : R →+* A) (I : Ideal A) : ↥(reesAlgebra (Ideal.comap f I)) →+* ↥(reesAlgebra I)

The ring homomorphism from the Rees algebra of I.comap f to the Rees algebra of I, induced coefficient-wise by f.

theorem ChowBlowup.reesAlgebra_comap_to_rees_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] (f : R →+* A) (hf : Function.Surjective ⇑f) (I : Ideal A) : Function.Surjective ⇑(reesAlgebra_comap_to_rees f I)

If f : R →+* A is surjective, the induced map of Rees algebras is also surjective.

noncomputable def ChowBlowup.reesAlgebra_quotient_equiv {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] (f : R →+* A) (hf : Function.Surjective ⇑f) (I : Ideal A) : ↥(reesAlgebra (Ideal.comap f I)) ⧸ RingHom.ker (reesAlgebra_comap_to_rees f I) ≃+* ↥(reesAlgebra I)

For a surjective ring map f : R →+* A, the Rees algebra of I.comap f modulo the kernel of the induced map is isomorphic to the Rees algebra of I.

noncomputable def ChowBlowup.blowup_intrinsic {R₁ : Type u_1} {R₂ : Type u_2} {A : Type u_3} [CommRing R₁] [CommRing R₂] [CommRing A] (f₁ : R₁ →+* A) (hf₁ : Function.Surjective ⇑f₁) (f₂ : R₂ →+* A) (hf₂ : Function.Surjective ⇑f₂) (I : Ideal A) : ↥(reesAlgebra (Ideal.comap f₁ I)) ⧸ RingHom.ker (reesAlgebra_comap_to_rees f₁ I) ≃+* ↥(reesAlgebra (Ideal.comap f₂ I)) ⧸ RingHom.ker (reesAlgebra_comap_to_rees f₂ I)

The blowup of A along I is intrinsic: any two surjective presentations of A yield isomorphic Rees algebra quotients.

noncomputable def ChowBlowup.blowup_intrinsic_equiv (k : Type u_1) [Field k] {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra k A] [Algebra k R] (f : R →+* A) (hf : Function.Surjective ⇑f) (𝔪 : Ideal A) (_h𝔪 : 𝔪.IsMaximal) : ↥(reesAlgebra (Ideal.comap f 𝔪)) ⧸ RingHom.ker (reesAlgebra_comap_to_rees f 𝔪) ≃+* ↥(reesAlgebra 𝔪)

Specialization of blowup_intrinsic: the Rees algebra blowup at a maximal ideal is intrinsic relative to any surjective k-algebra presentation.

theorem algebraMap_reesAlgebra_injective {R : Type u} [CommRing R] (I : Ideal R) : Function.Injective ⇑(algebraMap R ↥(reesAlgebra I))

The structure map R → reesAlgebra I (inclusion as constant polynomials) is injective.

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

Two schemes X and Y are birational if there exists a scheme Z with open immersions into both that have dense image.

def IsProjectiveScheme (X : AlgebraicGeometry.Scheme) : Prop

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

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

Every affine scheme U admits a projective completion: an open immersion into a projective scheme with dense image.

theorem closed_subscheme_projective' {X Y : AlgebraicGeometry.Scheme} (i : X ⟶ Y) (hi : AlgebraicGeometry.IsClosedImmersion i) (hY : IsProjectiveScheme Y) : IsProjectiveScheme X

A closed subscheme of a projective scheme is projective.

theorem product_projective_schemes' (Y₁ Y₂ : AlgebraicGeometry.Scheme) (h₁ : IsProjectiveScheme Y₁) (h₂ : IsProjectiveScheme Y₂) : ∃ (P : AlgebraicGeometry.Scheme), IsProjectiveScheme P

The product of two projective schemes is projective (existence form).

theorem graph_closed_of_separated' {U Y S : AlgebraicGeometry.Scheme} (Δ : U ⟶ Y) (fU : U ⟶ S) (fY : Y ⟶ S) [AlgebraicGeometry.IsSeparated fY] (hcomp : CategoryTheory.CategoryStruct.comp Δ fY = fU) : ∃ (Γ : AlgebraicGeometry.Scheme) (incl : Γ ⟶ U), AlgebraicGeometry.IsClosedImmersion incl ∧ AlgebraicGeometry.IsOpenImmersion incl ∧ Dense (Set.range ⇑incl)

The graph of a morphism into a separated scheme is closed, and packaged as an open and closed immersion with dense image.

theorem closure_birational' {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.IsIntegral X] : ∃ (X_tilde : AlgebraicGeometry.Scheme), IsBirational X X_tilde

The scheme-theoretic closure construction produces a birational model of an integral proper scheme.

theorem second_proj_closed_immersion' {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.IsIntegral X] : ∃ (X_tilde : AlgebraicGeometry.Scheme) (Y : AlgebraicGeometry.Scheme) (_ : IsProjectiveScheme Y) (g : X_tilde ⟶ Y), AlgebraicGeometry.IsClosedImmersion g ∧ IsBirational X X_tilde

Auxiliary step in Chow's lemma: there exists a birational model X_tilde of X admitting a closed immersion into a projective scheme.

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

Chow's lemma (Lec 9, Lem 20): every proper integral scheme X over S is birational to a projective scheme X'.