noncomputable def nodeResolveIso (k : Type u_1) [CommRing k] : (Polynomial (Polynomial k) ⧸ Ideal.span {Polynomial.X - Polynomial.C (Polynomial.X ^ 2 - 1)}) ≃ₐ[Polynomial k] Polynomial k

Algebra isomorphism resolving a nodal singularity: the quotient k[X][Y] / ⟨Y - C(X² - 1)⟩ is isomorphic (over k[X]) to k[X].

theorem fiber_origin_dim (k : Type u_1) [Field k] : Module.finrank k (Polynomial k ⧸ Ideal.span {Polynomial.X ^ 2 - 1}) = 2

The dimension of the fibre over the origin of the node X² - 1 = 0 is 2.