Cubic surfaces

9 fully proved

Algebraic Geometry

StructureCubic surface#✓fully proved

A cubic surface over a field \(k\) is a nonzero homogeneous polynomial \(f \in k[x_0, x_1, x_2, x_3]\) of degree \(3\) in the four homogeneous coordinates of \(\mathbb{P}^3\), its defining equation. The surface it describes is the projective zero locus \(V(f) \subseteq \mathbb{P}^3\).

@[ext]
structure CubicSurface where
  /-- The homogeneous cubic form cutting out the surface. -/
  defining : MvPolynomial (Fin 4) k
  /-- The defining form has degree `3`. -/
  isHomogeneous : defining.IsHomogeneous 3
  /-- The defining form is not identically zero, so it cuts out a genuine hypersurface. -/
  defining_ne_zero : defining ≠ 0

Used by 8

Used byVanishing partial derivatives force the cubic to vanish when \(3 \neq 0\) · Fermat cubic surface · The partial derivatives of a cubic form are quadratic · Singular point of a cubic surface · Singular points via partial derivatives · Smooth cubic surface · The defining cubic has total degree three · Triple plane

Cubic Surface

LemmaThe defining cubic has total degree three#✓fully proved

The defining cubic form of a cubic surface over a field \(k\) has total degree exactly \(3\).

lemma totalDegree_defining (S : CubicSurface k) : S.defining.totalDegree = 3

Uses 1

Statement usesCubic surface

LemmaThe partial derivatives of a cubic form are quadratic#✓fully proved

Let \(S\) be a cubic surface over a field \(k\) with defining cubic form \(f \in k[x_0, x_1, x_2, x_3]\). For each \(i \in \{0, 1, 2, 3\}\), the partial derivative \(\partial f / \partial x_i\) is homogeneous of degree \(2\).

lemma isHomogeneous_pderiv (S : CubicSurface k) (i : Fin 4) :
    (pderiv i S.defining).IsHomogeneous 2

Uses 1

Statement usesCubic surface

DefinitionSingular point of a cubic surface#✓fully proved

Let \(S\) be a cubic surface over a field \(k\) with defining cubic form \(f \in k[x_0, x_1, x_2, x_3]\). A point \(x \in k^4\) is a singular point of the affine cone over \(S\) when \(f(x) = 0\) and \(\partial f / \partial x_i\) vanishes at \(x\) for every \(i \in \{0, 1, 2, 3\}\).

Over an algebraically closed field, \(S\) is a smooth projective surface exactly when the origin is its only such point.

def IsSingularPoint (S : CubicSurface k) (x : Fin 4 → k) : Prop :=
  aeval x S.defining = 0 ∧ ∀ i, aeval x (pderiv i S.defining) = 0

Uses 1 · Used by 2

Statement usesCubic surface

Used bySingular points via partial derivatives · Smooth cubic surface

DefinitionSmooth cubic surface#✓fully proved

Let \(k\) be an algebraically closed field and \(S\) a cubic surface over \(k\) with defining cubic form \(f \in k[x_0, x_1, x_2, x_3]\). The surface \(S\) is smooth when every point \(x \in k^4\) at which \(f\) and all its partial derivatives \(\partial f / \partial x_i\) vanish is the origin, that is, when the origin is the only singular point of the affine cone over \(S\).

This is the Jacobian criterion for smoothness of the projective surface \(V(f) \subseteq \mathbb{P}^3\) cut out by \(f\).

def IsSmooth [IsAlgClosed k] (S : CubicSurface k) : Prop :=
  ∀ x : Fin 4 → k, S.IsSingularPoint x → x = 0

Uses 2

Statement usesCubic surface · Singular point of a cubic surface

LemmaVanishing partial derivatives force the cubic to vanish when \(3 \neq 0\)#✓fully proved

Let \(S\) be a cubic surface over a field \(k\) in which \(3 \neq 0\), and let \(f \in k[x_0, x_1, x_2, x_3]\) be its defining cubic form. If \(x \in k^4\) is a point at which every partial derivative \(\partial f / \partial x_i\) vanishes, then \(f(x) = 0\).

This follows from Euler's identity \(\sum_i x_i \, \partial f / \partial x_i = 3 f\).

lemma aeval_defining_eq_zero_of_pderiv (h3 : (3 : k) ≠ 0) (S : CubicSurface k)
    {x : Fin 4 → k} (hx : ∀ i, aeval x (pderiv i S.defining) = 0) :
    aeval x S.defining = 0

Uses 1 · Used by 1

Statement usesCubic surface

Used bySingular points via partial derivatives

LemmaSingular points via partial derivatives#✓fully proved

Let \(S\) be a cubic surface over a field \(k\) in which \(3 \neq 0\), and let \(f \in k[x_0, x_1, x_2, x_3]\) be its defining cubic form. A point \(x \in k^4\) is a singular point of the affine cone over \(S\) if and only if every partial derivative \(\partial f / \partial x_i\) vanishes at \(x\).

The condition \(f(x) = 0\) in the definition of a singular point is then automatic, by Euler's identity.

lemma isSingularPoint_iff (h3 : (3 : k) ≠ 0) (S : CubicSurface k) (x : Fin 4 → k) :
    S.IsSingularPoint x ↔ ∀ i, aeval x (pderiv i S.defining) = 0

Uses 3

Statement usesCubic surface · Singular point of a cubic surface

Proof usesVanishing partial derivatives force the cubic to vanish when \(3 \neq 0\)

Algebraic Geometry

DefinitionFermat cubic surface#✓fully proved

Over a field \(k\), the Fermat cubic surface is the cubic surface in \(\mathbb{P}^3\) with defining cubic form \(x_0^3 + x_1^3 + x_2^3 + x_3^3\).

It is smooth when the characteristic of \(k\) is not \(3\).

noncomputable def fermatCubicSurface : CubicSurface k where
  defining := X 0 ^ 3 + X 1 ^ 3 + X 2 ^ 3 + X 3 ^ 3
  isHomogeneous := by
    have h : ∀ i : Fin 4, ((X i : MvPolynomial (Fin 4) k) ^ 3).IsHomogeneous 3 := fun i => by
      simpa using (isHomogeneous_X k i).pow 3
    exact (((h 0).add (h 1)).add (h 2)).add (h 3)
  defining_ne_zero := by
    intro h
    have := congrArg (aeval (![1, 0, 0, 0] : Fin 4 → k)) h
    simp at this

Uses 1

Statement usesCubic surface

DefinitionTriple plane#✓fully proved

Over a field \(k\), the triple plane is the cubic surface in \(\mathbb{P}^3\) with defining cubic form \(x_0^3 \in k[x_0, x_1, x_2, x_3]\), that is, the plane \(x_0 = 0\) counted three times.

It is non-reduced, and every point of the plane \(x_0 = 0\) is a singular point.

noncomputable def triplePlane : CubicSurface k where
  defining := X 0 ^ 3
  isHomogeneous := by simpa using (isHomogeneous_X k 0).pow 3
  defining_ne_zero := pow_ne_zero 3 (X_ne_zero 0)

Uses 1

Statement usesCubic surface

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.