def BlowupAtPoint.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 BlowupAtPoint.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 BlowupAtPoint.reesDecomposeComponent {R : Type u_1} [CommRing R] (I : Ideal R) (f : ↥(reesAlgebra I)) (n : ℕ) : ↥(reesGrading I n)

The component of f ∈ R[It] in the n-th graded piece, namely the monomial f.coeff n · tⁿ.

theorem BlowupAtPoint.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 BlowupAtPoint.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 BlowupAtPoint.reesGrading_isInternal {R : Type u_1} [CommRing R] (I : Ideal R) : DirectSum.IsInternal (reesGrading I)

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

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

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

theorem BlowupAtPoint.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 BlowupAtPoint.reesGradedRing {R : Type u_1} [CommRing R] (I : Ideal R) : GradedRing (reesGrading I)

The Rees algebra together with reesGrading is a graded ring.

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

The blow-up scheme of Spec R along the ideal I, defined as Proj of the Rees algebra.

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

The natural projection from the blow-up to Spec of the degree-zero piece (canonically identified with Spec R).

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

Proper transform of a closed subscheme Z along a morphism π : X ⟶ Y, removing the center C: take the closure of the preimage of Z \ C in X.

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

Exceptional locus of a morphism π : X ⟶ Y over a closed subscheme C ⊂ Y: the preimage of C in X.

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

The blow-up of the closed subscheme Z ⊂ Spec R at the center C: the proper transform along the blow-up projection.

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

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

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

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

theorem BlowupAtPoint.reesAlgebra_monomial_mem {R : Type u_1} [CommRing R] (I : Ideal R) {n : ℕ} {a : R} : (Polynomial.monomial n) a ∈ reesAlgebra I ↔ a ∈ I ^ n

A monomial a · Xⁿ lies in the Rees algebra iff a ∈ Iⁿ.

theorem BlowupAtPoint.mem_reesAlgebra_char {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) : f ∈ reesAlgebra I ↔ ∀ (i : ℕ), f.coeff i ∈ I ^ i

Characterisation of membership in the Rees algebra: a polynomial f belongs to R[It] iff f.coeff i ∈ Iⁱ for every i.