def TangentCone.AssocGradedPiece (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) : Type u_1

The n-th graded piece I^n / I^{n+1} of the associated graded ring of R with respect to the ideal I.

@[implicit_reducible]

instance TangentCone.AssocGradedPiece.instAddCommGroup (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) : AddCommGroup (AssocGradedPiece R I n)

Additive group structure on the associated graded piece I^n / I^{n+1}.

@[implicit_reducible]

instance TangentCone.AssocGradedPiece.instModule (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) : Module R (AssocGradedPiece R I n)

R-module structure on the associated graded piece I^n / I^{n+1}.

def TangentCone.assocGradedProj (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) : ↥(I ^ n) →ₗ[R] AssocGradedPiece R I n

The canonical projection I^n → I^n / I^{n+1} onto the n-th associated graded piece.

@[implicit_reducible]

instance TangentCone.assocGradedGCommRing (R : Type u_1) [CommRing R] (I : Ideal R) : DirectSum.GCommRing (AssocGradedPiece R I)

Graded commutative ring structure on the family of associated graded pieces I^n / I^{n+1}.

def TangentCone.AssocGraded (R : Type u_1) [CommRing R] (I : Ideal R) : Type u_1

The associated graded ring gr_I(R) = ⊕_n I^n / I^{n+1}.

@[implicit_reducible]

instance TangentCone.AssocGraded.instCommRing (R : Type u_1) [CommRing R] (I : Ideal R) : CommRing (AssocGraded R I)

Commutative ring structure on the associated graded ring.

def TangentCone.reesAugmentationIdeal (R : Type u_1) [CommRing R] (I : Ideal R) : Ideal ↥(reesAlgebra I)

The augmentation ideal inside the Rees algebra of I, consisting of those polynomials f whose coefficient in degree n lies in I^{n+1}.

def TangentCone.reesToAssocGradedComponent (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) (f : ↥(reesAlgebra I)) : AssocGradedPiece R I n

The map sending an element of the Rees algebra to its n-th graded component in the associated graded ring, by taking the coefficient at n.

theorem TangentCone.monomial_mem_reesAlgebra (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) (a : R) (ha : a ∈ I ^ n) : (Polynomial.monomial n) a ∈ reesAlgebra I

A monomial a · X^n with a ∈ I^n belongs to the Rees algebra of I.

theorem TangentCone.reesToAssocGraded_surjective (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) : Function.Surjective (reesToAssocGradedComponent R I n)

The map from the Rees algebra to the n-th associated graded piece is surjective, witnessed by the monomial a · X^n.

theorem TangentCone.reesToAssocGraded_eq_zero_iff (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) (f : ↥(reesAlgebra I)) : reesToAssocGradedComponent R I n f = 0 ↔ (↑f).coeff n ∈ I ^ (n + 1)

The n-th graded component of an element f of the Rees algebra vanishes in I^n / I^{n+1} iff its coefficient at n lies in I^{n+1}.

theorem TangentCone.mem_reesAugmentationIdeal_iff (R : Type u_1) [CommRing R] (I : Ideal R) (f : ↥(reesAlgebra I)) : f ∈ reesAugmentationIdeal R I ↔ ∀ (n : ℕ), reesToAssocGradedComponent R I n f = 0

An element f of the Rees algebra lies in the augmentation ideal iff all of its graded components in the associated graded ring vanish.

def TangentCone.tangentConeIsoReesQuotient (R : Type u_1) [CommRing R] (I : Ideal R) : ↥(reesAlgebra I) ⧸ reesAugmentationIdeal R I ≃+* AssocGraded R I

The tangent cone Spec(gr_I(R)) is isomorphic to Spec of the quotient of the Rees algebra by its augmentation ideal, exhibiting the cone over the exceptional locus of the blowup (Def 38, Lec 19; Prop 38, Lec 20).