noncomputable def blowupChartMap (k : Type u_1) [CommRing k] : Polynomial (Polynomial k) →+* Polynomial (Polynomial k)

Ring map on k[X][Y] substituting Y ↦ C(X) · Y, modelling one affine chart of the blow-up of the affine plane at the origin (where the exceptional y-coordinate is replaced by the product of the base coordinate X and a new fibre coordinate Y).

theorem blowupChartMap_eq_comp (k : Type u_1) [CommRing k] (p : Polynomial (Polynomial k)) : (blowupChartMap k) p = p.comp (Polynomial.C Polynomial.X * Polynomial.X)

The blow-up chart map computes as composition by C X * X in the Y variable.

theorem blowupChartMap_X (k : Type u_1) [CommRing k] : (blowupChartMap k) Polynomial.X = Polynomial.C Polynomial.X * Polynomial.X

Image of the outer variable Y (denoted X in k[X][Y]) under the blow-up chart map.

theorem blowupChartMap_C (k : Type u_1) [CommRing k] (a : Polynomial k) : (blowupChartMap k) (Polynomial.C a) = Polynomial.C a

The blow-up chart map fixes constants C a with a ∈ k[X].

theorem blowupChartMap_injective (k : Type u_1) [CommRing k] [IsDomain k] : Function.Injective ⇑(blowupChartMap k)

The blow-up chart map is injective over a domain k; reflects that the affine chart is birational to the affine plane.