Documentation

TauCeti.RingTheory.Node.ExceptionalFiber

The exceptional fibre of blowing up a node at its closed point #

Let A be a local ring whose maximal ideal is generated by two elements x, y satisfying a quadratic relation a x² + b x y + y² = 0, with x a nonzerodivisor and 𝔪 not principal. This models the local ring at a node: by TauCeti.exists_hypersurface_presentation_of_formallyUnramified the local ring there is P ⧸ (f) for a local ring P with two coordinates and f with nondegenerate quadratic part a s² + b s t + c t², and when c is a unit, dividing by c gives a relation of the above shape. Let A[𝔪/x] be the affine blowup algebra of 𝔪 at x, the ring of the chart D₊(x) of the blowup of Spec A at its closed point.

In A[𝔪/x] the fraction w = y/x satisfies w² + b w + a = 0, and A[𝔪/x] = A + A w is a finite A-module. Its fibre over the closed point is therefore a quotient of κ[W] ⧸ (W² + b W + a), where κ is the residue field and a, b are read in κ. It is the whole of it: if the fibre had dimension at most one over κ, Nakayama's lemma would give A[𝔪/x] = A, so y/x ∈ A and 𝔪 = (x) would be principal. Hence

κ ⊗[A] A[𝔪/x] ≃ κ[W] ⧸ (W² + b W + a),

a κ-algebra of dimension two, which is étale over κ when the discriminant b² - 4a is a unit. Geometrically, W is the slope y/x of a tangent direction at the closed point, and the roots of W² + b W + a are the slopes of the two lines of the tangent cone a x² + b x y + y² = 0, the tangent directions of the two branches through the node. When b² - 4a is a unit they are distinct, and rational over κ or conjugate over a separable quadratic extension of κ.

Since y² = -x (a x + b y) lies in x 𝔪, the chart Spec A[𝔪/x] is the whole blowup (TauCeti.AlgebraicGeometry.isIso_affineBlowupι_of_sq_mem). Thus the inverse image of the closed point in the blowup of Spec A at the closed point is finite étale of degree two over it.

Main results #

References #

source
theorem TauCeti.divBy_sq_add_mul_add_eq_zero {A : Type u_1} [CommRing A] {x y a b : A} (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away x S] (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) :
Localization.divBy y x ^ 2 + (algebraMap A S) b * Localization.divBy y x + (algebraMap A S) a = 0

In the chart A[𝔪/x], the relation a x² + b x y + y² = 0 becomes the monic quadratic relation w² + b w + a = 0 for w = y/x.

source
theorem TauCeti.toSubmodule_affineBlowup_eq_span {A : Type u_1} [CommRing A] {x y a b : A} {S : Type u_2} [CommRing S] [Algebra A S] [IsLocalization.Away x S] {I : Ideal A} (hI : I = Ideal.span {x, y}) (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) :
Subalgebra.toSubmodule (I.affineBlowup x S) = Submodule.span A {1, Localization.divBy y x}

The chart of the blowup is spanned by 1 and y/x. If I = (x, y) and a x² + b x y + y² = 0, the affine blowup algebra A[I/x] is the A-submodule of the localization spanned by 1 and y/x.

source
theorem TauCeti.finite_affineBlowup {A : Type u_1} [CommRing A] {x y a b : A} {S : Type u_2} [CommRing S] [Algebra A S] [IsLocalization.Away x S] {I : Ideal A} (hI : I = Ideal.span {x, y}) (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) :
Module.Finite A ↥(I.affineBlowup x S)

The chart of the blowup is finite. If I = (x, y) and a x² + b x y + y² = 0, the affine blowup algebra A[I/x] is a finite A-module.

source
theorem TauCeti.finrank_tensor_affineBlowup {A : Type u_1} [CommRing A] {x y a b : A} {S : Type u_2} [CommRing S] [Algebra A S] [IsLocalization.Away x S] [IsLocalRing A] (hm : IsLocalRing.maximalIdeal A = Ideal.span {x, y}) (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) (hx : x ∈ nonZeroDivisors A) (hprin : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal A)) :
Module.finrank (IsLocalRing.ResidueField A) (TensorProduct A (IsLocalRing.ResidueField A) ↥((IsLocalRing.maximalIdeal A).affineBlowup x S)) = 2

The exceptional fibre of the chart has dimension two. Let 𝔪 = (x, y) be generated by a nonzerodivisor x and an element y with a x² + b x y + y² = 0, and suppose that 𝔪 is not principal. Then the fibre κ ⊗[A] A[𝔪/x] of the chart A[𝔪/x] of the blowup at the closed point has dimension two over the residue field κ.

source
noncomputable def TauCeti.adjoinRootEquivTensorAffineBlowup {A : Type u_1} [CommRing A] {x y a b : A} {S : Type u_2} [CommRing S] [Algebra A S] [IsLocalization.Away x S] [IsLocalRing A] (hm : IsLocalRing.maximalIdeal A = Ideal.span {x, y}) (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) (hx : x ∈ nonZeroDivisors A) (hprin : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal A)) :
AdjoinRoot (Polynomial.X ^ 2 + Polynomial.C ((IsLocalRing.residue A) b) * Polynomial.X + Polynomial.C ((IsLocalRing.residue A) a)) ≃ₐ[IsLocalRing.ResidueField A] TensorProduct A (IsLocalRing.ResidueField A) ↥((IsLocalRing.maximalIdeal A).affineBlowup x S)

The exceptional fibre of blowing up a node. Let 𝔪 = (x, y) be generated by a nonzerodivisor x and an element y with a x² + b x y + y² = 0, and suppose that 𝔪 is not principal. Then the fibre κ ⊗[A] A[𝔪/x] of the chart A[𝔪/x] of the blowup at the closed point is κ[W] ⧸ (W² + b W + a), with W corresponding to 1 ⊗ y/x.

Instances For
    source
    @[simp]
    theorem TauCeti.adjoinRootEquivTensorAffineBlowup_root {A : Type u_1} [CommRing A] {x y a b : A} {S : Type u_2} [CommRing S] [Algebra A S] [IsLocalization.Away x S] [IsLocalRing A] (hm : IsLocalRing.maximalIdeal A = Ideal.span {x, y}) (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) (hx : x ∈ nonZeroDivisors A) (hprin : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal A)) :
    (adjoinRootEquivTensorAffineBlowup hm hrel hx hprin) (AdjoinRoot.root (Polynomial.X ^ 2 + Polynomial.C ((IsLocalRing.residue A) b) * Polynomial.X + Polynomial.C ((IsLocalRing.residue A) a))) = 1 ⊗ₜ[A] ⟨Localization.divBy y x, ⋯⟩

    The isomorphism adjoinRootEquivTensorAffineBlowup sends the root W to 1 ⊗ y/x.

    source
    theorem TauCeti.etale_tensor_affineBlowup {A : Type u_1} [CommRing A] {x y a b : A} {S : Type u_2} [CommRing S] [Algebra A S] [IsLocalization.Away x S] [IsLocalRing A] (hm : IsLocalRing.maximalIdeal A = Ideal.span {x, y}) (hrel : a * x ^ 2 + b * x * y + y ^ 2 = 0) (hd : IsUnit (discrim a b 1)) :
    Algebra.Etale (IsLocalRing.ResidueField A) (TensorProduct A (IsLocalRing.ResidueField A) ↥((IsLocalRing.maximalIdeal A).affineBlowup x S))

    The exceptional fibre of blowing up a node is étale. Let 𝔪 = (x, y) with a x² + b x y + y² = 0. If the discriminant b² - 4a is a unit, the fibre κ ⊗[A] A[𝔪/x] of the chart A[𝔪/x] of the blowup at the closed point is étale over the residue field κ: it is a quotient of the étale algebra κ[W] ⧸ (W² + b W + a).