noncomputable def Definition38.reesIdealFromBase {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : Ideal ↥(reesAlgebra 𝔪)

The ideal of the Rees algebra of 𝔪 generated by the image of 𝔪 ⊆ R.

def Definition38.assocGradedRing {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : Type u_1

Associated graded ring gr_𝔪(R) = ⊕_n 𝔪^n / 𝔪^{n+1}, realized as the Rees algebra modulo the ideal generated by 𝔪 (Def 38, Lec 19).

@[implicit_reducible]

noncomputable instance Definition38.assocGradedRing.instCommRing {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : CommRing (assocGradedRing 𝔪)

The associated graded ring is a commutative ring.

noncomputable def Definition38.ringHomToAssocGraded {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : R →+* assocGradedRing 𝔪

Canonical ring map R → gr_𝔪(R) factoring through the Rees algebra and quotient.

theorem Definition38.tangentCone_over_closedPoint {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : 𝔪 ≤ RingHom.ker (ringHomToAssocGraded 𝔪)

The maximal ideal 𝔪 lies in the kernel of R → gr_𝔪(R), i.e. the associated graded ring lives over the closed point.

noncomputable def Definition38.tangentCone {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : AlgebraicGeometry.Scheme

The tangent cone (Def 38, Lec 19): T_x X = Spec(gr_𝔪(O_{X,x})) for the maximal ideal 𝔪.

noncomputable def Definition38.tangentConeMap {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : tangentCone 𝔪 ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)

The canonical morphism tangentCone 𝔪 → Spec R induced by R → gr_𝔪(R).