def Blowup.reesGrading {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : AddSubgroup ↥(reesAlgebra I)

The n-th graded piece of the Rees algebra R[It] = ⨁ Iⁿ tⁿ: monomials a · tⁿ with a ∈ Iⁿ, packaged as an additive subgroup of the Rees algebra.

@[implicit_reducible]

noncomputable instance Blowup.reesGrading_addCommMonoid {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : AddCommMonoid ↥(reesGrading I n)

Each graded piece reesGrading I n carries the inherited AddCommMonoid structure.

noncomputable def Blowup.reesDecomposeComponent {R : Type u_1} [CommRing R] (I : Ideal R) (f : ↥(reesAlgebra I)) (n : ℕ) : ↥(reesGrading I n)

Project an element f of the Rees algebra onto its n-th graded component.

theorem Blowup.reesDecomposeComponent_coe_coe {R : Type u_1} [CommRing R] (I : Ideal R) (f : ↥(reesAlgebra I)) (n : ℕ) : ↑↑(reesDecomposeComponent I f n) = (Polynomial.monomial n) ((↑f).coeff n)

The underlying polynomial of reesDecomposeComponent I f n is the monomial of degree n with coefficient f.coeff n.

theorem Blowup.coeff_coeAddMonoidHom {R : Type u_1} [CommRing R] (I : Ideal R) (x : DirectSum ℕ fun (n : ℕ) => ↥(reesGrading I n)) (n : ℕ) : (↑((DirectSum.coeAddMonoidHom (reesGrading I)) x)).coeff n = (↑↑(x n)).coeff n

The n-th coefficient of the polynomial assembled from a direct-sum element coincides with the n-th coefficient of the component in degree n.

theorem Blowup.reesGrading_isInternal {R : Type u_1} [CommRing R] (I : Ideal R) : DirectSum.IsInternal (reesGrading I)

The graded pieces reesGrading I n form an internal direct sum decomposition of the Rees algebra.

theorem Blowup.reesGrading_one_mem {R : Type u_1} [CommRing R] (I : Ideal R) : 1 ∈ reesGrading I 0

The multiplicative identity lies in the degree-zero piece of the Rees algebra.

theorem Blowup.reesGrading_mul_mem {R : Type u_1} [CommRing R] (I : Ideal R) {i j : ℕ} {fi fj : ↥(reesAlgebra I)} (hi : fi ∈ reesGrading I i) (hj : fj ∈ reesGrading I j) : fi * fj ∈ reesGrading I (i + j)

Multiplication of homogeneous elements of degrees i and j lands in degree i + j.

@[implicit_reducible]

noncomputable instance Blowup.reesGradedRing {R : Type u_1} [CommRing R] (I : Ideal R) : GradedRing (reesGrading I)

The Rees algebra equipped with reesGrading is a graded ring.

noncomputable def Blowup.blowupAlong {R : Type u_1} [CommRing R] (I : Ideal R) : AlgebraicGeometry.Scheme

The blow-up of Spec R along the ideal I (Def 20, Lec 9): Proj of the Rees algebra.

noncomputable def Blowup.blowupProjection {R : Type u_1} [CommRing R] (I : Ideal R) : blowupAlong I ⟶ AlgebraicGeometry.Spec (CommRingCat.of ↥(reesGrading I 0))

Natural projection from the blow-up Bl_I(Spec R) down to Spec of the degree-zero piece, canonically identified with Spec R.

def Blowup.properTransformSet {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (Z C : TopologicalSpace.Closeds ↑Y.toTopCat) : TopologicalSpace.Closeds ↑X.toTopCat

Proper transform of a closed subset Z along π : X ⟶ Y, away from the center C: the closure in X of the preimage of Z \ C.

def Blowup.exceptionalLocusSet {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (C : TopologicalSpace.Closeds ↑Y.toTopCat) : TopologicalSpace.Closeds ↑X.toTopCat

Exceptional locus of π : X ⟶ Y over a closed subscheme C ⊂ Y, defined as π⁻¹(C).

noncomputable def Blowup.blowupAtCenter {R : Type u_1} [CommRing R] (I : Ideal R) (Z C : TopologicalSpace.Closeds ↑(AlgebraicGeometry.Spec (CommRingCat.of ↥(reesGrading I 0))).toTopCat) : TopologicalSpace.Closeds ↑(blowupAlong I).toTopCat

The proper transform of a closed subscheme Z along the blow-up projection, viewed as a closed subset of the blow-up.

def Blowup.blowupExceptionalLocus {R : Type u_1} [CommRing R] (I : Ideal R) (Z C : TopologicalSpace.Closeds ↑(AlgebraicGeometry.Spec (CommRingCat.of ↥(reesGrading I 0))).toTopCat) : TopologicalSpace.Closeds ↑(blowupAlong I).toTopCat

The exceptional locus of the blow-up of Z: the intersection of the proper transform with the preimage of the center C.

theorem Blowup.properTransform_contains_preimage_away {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (Z C : TopologicalSpace.Closeds ↑Y.toTopCat) : ⇑π ⁻¹' (↑Z \ ↑C) ⊆ ↑(properTransformSet π Z C)

The proper transform contains the preimage of the open complement Z \ C.

theorem Blowup.properTransform_top {X Y : AlgebraicGeometry.Scheme} (π : X ⟶ Y) (C : TopologicalSpace.Closeds ↑Y.toTopCat) : ↑(properTransformSet π ⊤ C) = closure (⇑π ⁻¹' (↑⊤ \ ↑C))

Proper transform of the whole space Z = ⊤ equals the closure of π⁻¹(Yᶜᶜ \ C).

theorem Blowup.reesGrading_zero_iso_base {R : Type u_1} [CommRing R] (I : Ideal R) : ∃ (e : ↥(reesGrading I 0) ≃+* R), True

The degree-zero piece of the Rees algebra is canonically ring-isomorphic to the base ring R via a · t⁰ ↦ a.

theorem Blowup.blowup_algebra_eq_rees {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (a : R) (ha : a ∈ I ^ n) : ⟨(Polynomial.monomial n) a, ⋯⟩ ∈ reesGrading I n

For a ∈ Iⁿ, the monomial a · tⁿ is a homogeneous element of degree n in the Rees algebra.

theorem Blowup.reesAlgebra_finiteType_over_gradeZero {R : Type u_1} [CommRing R] (I : Ideal R) (hI : I.FG) : Algebra.FiniteType ↥(reesGrading I 0) ↥(reesAlgebra I)

When the ideal I is finitely generated, the Rees algebra is of finite type as an algebra over its degree-zero piece.

theorem Blowup.blowup_projection_isProper {R : Type u_1} [CommRing R] (I : Ideal R) (hI : I.FG) : ∃ (f : blowupAlong I ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)), AlgebraicGeometry.IsProper f

The blow-up morphism Bl_I(Spec R) ⟶ Spec R is proper when I is finitely generated.

theorem Blowup.blowup_iso_away_from_center {R : Type u_1} [CommRing R] (I : Ideal R) : ∃ (U : (blowupAlong I).Opens) (f : ↑U ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)), AlgebraicGeometry.IsOpenImmersion f

There exists an open subscheme of the blow-up that is isomorphic (via an open immersion into Spec R) to the complement of the center; expresses that the blow-up is an isomorphism outside the center.

theorem Blowup.blowup_birational {R : Type u_1} [CommRing R] (I : Ideal R) (hI : I ≠ ⊥) : ∃ (U : (blowupAlong I).Opens) (f : ↑U ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)), AlgebraicGeometry.IsOpenImmersion f

The blow-up of Spec R along a non-zero ideal is birational to Spec R.