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

The image of an ideal 𝔪 ⊆ R inside the Rees algebra R[𝔪 t].

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

The associated graded ring gr_𝔪 R = ⨁ 𝔪^n / 𝔪^{n+1}, defined as the Rees algebra quotiented by the image of 𝔪.

@[implicit_reducible]

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

The commutative ring structure on the associated graded ring.

@[reducible, inline]

abbrev Prop34Blowup.exceptionalFiberRing {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : Type u_1

The fibre of the blowup over the centre, realised as the tensor product reesAlgebra 𝔪 ⊗_R R/𝔪.

@[implicit_reducible]

noncomputable instance Prop34Blowup.assocGradedRing.algebraRees {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : Algebra (↥(reesAlgebra 𝔪)) (assocGradedRing 𝔪)

Algebra structure on the associated graded ring over the Rees algebra.

noncomputable def Prop34Blowup.assocGraded_equivExceptionalFiber {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : assocGradedRing 𝔪 ≃ₐ[↥(reesAlgebra 𝔪)] exceptionalFiberRing 𝔪

Algebra isomorphism between the associated graded ring and the exceptional fibre ring, viewed over the Rees algebra.

noncomputable def Prop34Blowup.assocGraded_ringEquivExceptionalFiber {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : assocGradedRing 𝔪 ≃+* exceptionalFiberRing 𝔪

Ring isomorphism gr_𝔪 R ≅ reesAlgebra 𝔪 ⊗_R R/𝔪.

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

The tangent cone scheme: Spec (gr_𝔪 R).

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

The exceptional fibre of the blowup as a scheme.

noncomputable def Prop34Blowup.tangentCone_isoExceptionalFiber {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : tangentConeScheme 𝔪 ≅ exceptionalFiberScheme 𝔪

Proposition 34 (key isomorphism): the tangent cone scheme is canonically isomorphic to the exceptional fibre of the blowup.

noncomputable def Prop34Blowup.scaleAlgHom {R : Type u_1} [CommRing R] (c : R) : Polynomial R →ₐ[R] Polynomial R

The R-algebra endomorphism of R[X] sending X ↦ c · X, used to define the scaling action on the Rees algebra.

theorem Prop34Blowup.scaleAlgHom_one {R : Type u_1} [CommRing R] : scaleAlgHom 1 = AlgHom.id R (Polynomial R)

Scaling by 1 is the identity on R[X].

theorem Prop34Blowup.scaleAlgHom_comp {R : Type u_1} [CommRing R] (c₁ c₂ : R) : (scaleAlgHom c₁).comp (scaleAlgHom c₂) = scaleAlgHom (c₁ * c₂)

Scaling by c₁ then c₂ is the same as scaling by c₁ · c₂.

theorem Prop34Blowup.scaleAlgHom_mem_reesAlgebra {R : Type u_1} [CommRing R] (I : Ideal R) (c : R) (f : Polynomial R) (hf : f ∈ reesAlgebra I) : (scaleAlgHom c) f ∈ reesAlgebra I

Scaling preserves membership in the Rees algebra.

noncomputable def Prop34Blowup.scaleOnRees {R : Type u_1} [CommRing R] (I : Ideal R) (c : R) : ↥(reesAlgebra I) →+* ↥(reesAlgebra I)

The induced scaling ring homomorphism on the Rees algebra.

theorem Prop34Blowup.scaleOnRees_algebraMap {R : Type u_1} [CommRing R] (I : Ideal R) (c r : R) : (scaleOnRees I c) ((algebraMap R ↥(reesAlgebra I)) r) = (algebraMap R ↥(reesAlgebra I)) r

The scaling action on the Rees algebra fixes elements of R.

theorem Prop34Blowup.reesIdealFromBase_le_comap_scaleOnRees {R : Type u_1} [CommRing R] (I : Ideal R) (c : R) : reesIdealFromBase I ≤ Ideal.comap (scaleOnRees I c) (reesIdealFromBase I)

The base ideal I · R[Rt] is invariant under the scaling map.

noncomputable def Prop34Blowup.scaleOnGraded {R : Type u_1} [CommRing R] (I : Ideal R) (c : R) : assocGradedRing I →+* assocGradedRing I

The descended scaling action on the associated graded ring.

theorem Prop34Blowup.scaleOnGraded_one {R : Type u_1} [CommRing R] (I : Ideal R) : scaleOnGraded I 1 = RingHom.id (assocGradedRing I)

The unit 1 ∈ R acts as the identity on the associated graded ring.

theorem Prop34Blowup.scaleOnGraded_comp {R : Type u_1} [CommRing R] (I : Ideal R) (c₁ c₂ : R) : scaleOnGraded I (c₁ * c₂) = (scaleOnGraded I c₁).comp (scaleOnGraded I c₂)

The scaling action is multiplicative on the associated graded ring.

theorem Prop34Blowup.proposition_34_blowup_properties {R : Type u_1} [CommRing R] (𝔪 : Ideal R) : Nonempty (tangentConeScheme 𝔪 ≅ exceptionalFiberScheme 𝔪) ∧ scaleOnGraded 𝔪 1 = RingHom.id (assocGradedRing 𝔪) ∧ ∀ (c₁ c₂ : R), scaleOnGraded 𝔪 (c₁ * c₂) = (scaleOnGraded 𝔪 c₁).comp (scaleOnGraded 𝔪 c₂)

Proposition 34: the tangent cone is canonically isomorphic to the exceptional fibre, and the scaling action is a group action.

theorem Prop34Blowup.proposition_34_iso_away_from_center {R : Type u_1} [CommRing R] (I : Ideal R) : ∃ (U : (AlgebraicGeometry.Proj (BlowupAtPoint.reesGrading I)).Opens) (f : ↑U ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)), AlgebraicGeometry.IsOpenImmersion f

Proposition 34 (corollary): the blowup is an isomorphism away from the centre V(I).

theorem Prop38TangentCone.associated_graded_eq_symmetric_of_regular (R : Type u_1) [CommRing R] [IsRegularLocalRing R] : Nonempty (Prop34Blowup.assocGradedRing (IsLocalRing.maximalIdeal R) ≃+* SymmetricAlgebra (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R))

Proposition 38: for a regular local ring, the associated graded ring is isomorphic to the symmetric algebra of the cotangent space over the residue field.

theorem Prop38TangentCone.assocGraded_isReduced_of_regular (R : Type u_1) [CommRing R] [IsRegularLocalRing R] : IsReduced (Prop34Blowup.assocGradedRing (IsLocalRing.maximalIdeal R))

Corollary of Proposition 38: the associated graded ring of a regular local ring is reduced.