Named bundles for the curve components of affine surfaces in three-space: an integral curve of a given degree on a surface, and a positive-degree component of the intersection of two surfaces.

structure CCDN.IsSurfaceCurve (f : CoordinatePolynomial 3) (I : Ideal (CoordinatePolynomial 3)) (e : ℕ) : Prop

I is an integral affine curve of degree e on the surface f = 0 in affine three-space: a height-two prime ideal containing f whose affine Hilbert function has slope e.

• isPrime : I.IsPrime

  The ideal I is prime.

• height_eq : I.height = 2

  The ideal I has height two, so it defines a curve.

• mem : f ∈ I

  The curve lies on the surface: f ∈ I.

• degree : HasAffineCurveDegree I e

  The curve has degree e.

structure CCDN.IsSectionCurve (f g : CoordinatePolynomial 3) (I : Ideal (CoordinatePolynomial 3)) (e : ℕ) extends CCDN.IsSurfaceCurve f I e : Prop

I is a curve component, of positive degree e, of the intersection of the surfaces f = 0 and g = 0 in affine three-space.

• isPrime : I.IsPrime
• height_eq : I.height = 2
• mem : f ∈ I
• degree : HasAffineCurveDegree I e
• mem_right : g ∈ I

  The curve lies on the second surface: g ∈ I.

• pos : 0 < e

  The degree e is positive.