noncomputable def BlowupReesConnection.originIdeal (k : Type u_1) [CommRing k] : Ideal (Polynomial (Polynomial k))

The ideal (X, Y) ⊂ k[X][Y] cutting out the origin in the affine plane.

theorem BlowupReesConnection.x_mem_originIdeal (k : Type u_1) [CommRing k] : Polynomial.C Polynomial.X ∈ originIdeal k

The generator X (as C X ∈ k[X][Y]) lies in the origin ideal.

theorem BlowupReesConnection.y_mem_originIdeal (k : Type u_1) [CommRing k] : Polynomial.X ∈ originIdeal k

The generator Y (as X ∈ k[X][Y]) lies in the origin ideal.

theorem BlowupReesConnection.xt_mem_reesAlgebra (k : Type u_1) [CommRing k] : (Polynomial.monomial 1) (Polynomial.C Polynomial.X) ∈ reesAlgebra (originIdeal k)

The monomial X · t belongs to the Rees algebra of the origin ideal.

theorem BlowupReesConnection.yt_mem_reesAlgebra (k : Type u_1) [CommRing k] : (Polynomial.monomial 1) Polynomial.X ∈ reesAlgebra (originIdeal k)

The monomial Y · t belongs to the Rees algebra of the origin ideal.

theorem BlowupReesConnection.CX_mul_X_eq_monomial (k : Type u_1) [CommRing k] : Polynomial.C Polynomial.X * Polynomial.X = (Polynomial.monomial 1) Polynomial.X

The product C(Y) · t rewrites as the monomial Y · t.

theorem BlowupReesConnection.yt_product_mem_reesAlgebra (k : Type u_1) [CommRing k] : Polynomial.C Polynomial.X * Polynomial.X ∈ reesAlgebra (originIdeal k)

The product C(Y) · t (rewritten form of Y · t) belongs to the Rees algebra.

noncomputable def BlowupReesConnection.coeffEmbed (k : Type u_1) [CommRing k] : Polynomial k →+* Polynomial (Polynomial (Polynomial k))

Embedding k[X] → k[X][Y][t] sending a polynomial to its image as a doubly-constant coefficient; used as the scalar part of the Rees lift.

noncomputable def BlowupReesConnection.reesLift (k : Type u_1) [CommRing k] : Polynomial (Polynomial k) →+* Polynomial (Polynomial (Polynomial k))

Lift of a polynomial in k[X][Y] to the Rees algebra by sending Y ↦ C(Y) · t, exhibiting the Rees algebra structure relevant to the blow-up at the origin.

theorem BlowupReesConnection.coeffEmbed_mem_reesAlgebra (k : Type u_1) [CommRing k] (a : Polynomial k) : (coeffEmbed k) a ∈ reesAlgebra (originIdeal k)

The image of coeffEmbed lies inside the Rees algebra of the origin ideal.

theorem BlowupReesConnection.reesLift_mem_reesAlgebra (k : Type u_1) [CommRing k] (f : Polynomial (Polynomial k)) : (reesLift k) f ∈ reesAlgebra (originIdeal k)

The Rees lift of any element of k[X][Y] lies in the Rees algebra of the origin ideal.

noncomputable def BlowupReesConnection.evalAtX (k : Type u_1) [CommRing k] : Polynomial (Polynomial (Polynomial k)) →+* Polynomial (Polynomial k)

Evaluation map specialising the Rees variable t to X; recovers the blow-up chart map after composing with the Rees lift.

theorem BlowupReesConnection.blowup_chart_factors_through_rees (k : Type u_1) [CommRing k] : (evalAtX k).comp (reesLift k) = blowupChartMap k

Key factorisation: the blow-up chart map is the composition of the Rees lift with evaluation at t = X.

theorem BlowupReesConnection.blowup_chart_eq_eval_reesLift (k : Type u_1) [CommRing k] (f : Polynomial (Polynomial k)) : (blowupChartMap k) f = (evalAtX k) ((reesLift k) f)

Pointwise version of blowup_chart_factors_through_rees.

theorem BlowupReesConnection.reesLift_x (k : Type u_1) [CommRing k] : (reesLift k) (Polynomial.C Polynomial.X) = (coeffEmbed k) Polynomial.X

The Rees lift fixes the base variable X.

theorem BlowupReesConnection.reesLift_y (k : Type u_1) [CommRing k] : (reesLift k) Polynomial.X = Polynomial.C Polynomial.X * Polynomial.X

The Rees lift sends the fibre variable Y to C(Y) · t.

theorem BlowupReesConnection.reesLift_y_eq_monomial (k : Type u_1) [CommRing k] : (reesLift k) Polynomial.X = (Polynomial.monomial 1) Polynomial.X

Equivalent monomial form: reesLift Y = Y · t = monomial 1 Y.