Line arrangements in the projective plane

TheoremTwo distinct lines meet in their cross product#✓fully proved

Let \(K\) be a field and let \(v \ne w\) be two distinct points of the projective plane \(\mathbb{P}(K^3)\). Call two points orthogonal when the dot product of representative vectors in \(K^3\) vanishes, and let \(v \times w\) be the point spanned by the cross product of representatives of \(v\) and \(w\), which is nonzero since \(v \ne w\). Then a point \(p\) equals \(v \times w\) if and only if \(p\) is orthogonal to both \(v\) and \(w\). Reading points as coordinate vectors of lines, this says that two distinct lines meet exactly in their cross product, and dually that two distinct points lie on exactly one line.

theorem eq_cross_iff {p v w : ℙ K (Fin 3 → K)} (h : v ≠ w) :
    p = cross v w ↔ p.orthogonal v ∧ p.orthogonal w

Used by 1

Used bySingular points lie on two distinct lines

StructureLine arrangement#✓fully proved

A line arrangement in the projective plane over a field \(K\) is a finite set of at least two lines, each line recorded by its coordinate vector, a point of the dual projective plane \(\mathbb{P}(K^3)\).

A point \(p\) lies on the line with coordinate vector \(\ell\) when the dot product of representatives of \(p\) and \(\ell\) vanishes.

@[ext]
structure LineArrangement (K : Type*) [Field K] where
  /-- The lines of the arrangement. -/
  lines : Finset (ℙ K (Fin 3 → K))
  /-- An arrangement has at least two lines. -/
  two_le_card : 2 ≤ lines.card

Used by 7

Used byHarbourne constant of a line arrangement · Singular points are the points of multiplicity at least two · Singular points lie on two distinct lines · Multiplicity of a point in a line arrangement · Multiplicity is at most the number of lines · Singular points of a line arrangement · Every line arrangement has a singular point

DefinitionMultiplicity of a point in a line arrangement#✓fully proved

Let \(A\) be a line arrangement in the projective plane over a field. The multiplicity \(m_p\) of a point \(p\) in \(A\) is the number of lines of \(A\) through \(p\), that is, of lines of \(A\) whose coordinate vector has zero dot product with a representative of \(p\).

noncomputable def multiplicity (p : ℙ K (Fin 3 → K)) : ℕ :=
  (A.lines.filter fun ℓ => p.orthogonal ℓ).card

Uses 1 · Used by 3

Statement usesLine arrangement

Used byHarbourne constant of a line arrangement · Singular points are the points of multiplicity at least two · Multiplicity is at most the number of lines

DefinitionSingular points of a line arrangement#✓fully proved

The singular points of a line arrangement \(A\) in the projective plane over a field form the finite set of intersection points of pairs of distinct lines of \(A\), where two distinct lines with coordinate vectors \(\ell\) and \(\ell'\) meet in the point spanned by the cross product \(\ell \times \ell'\) of their representatives.

noncomputable def singularPoints : Finset (ℙ K (Fin 3 → K)) :=
  A.lines.offDiag.image fun ℓ => Projectivization.cross ℓ.1 ℓ.2

Uses 1 · Used by 4

Statement usesLine arrangement

Used byHarbourne constant of a line arrangement · Singular points are the points of multiplicity at least two · Singular points lie on two distinct lines · Every line arrangement has a singular point

TheoremSingular points lie on two distinct lines#✓fully proved

Let \(A\) be a line arrangement in the projective plane over a field. A point \(p\) is a singular point of \(A\) if and only if there are two distinct lines of \(A\) that both pass through \(p\).

theorem mem_singularPoints_iff_exists {p : ℙ K (Fin 3 → K)} :
    p ∈ A.singularPoints ↔
      ∃ ℓ ∈ A.lines, ∃ ℓ' ∈ A.lines, ℓ ≠ ℓ' ∧ p.orthogonal ℓ ∧ p.orthogonal ℓ'

Uses 3 · Used by 2

Statement usesLine arrangement · Singular points of a line arrangement

Proof usesTwo distinct lines meet in their cross product

Used bySingular points are the points of multiplicity at least two · Every line arrangement has a singular point

TheoremSingular points are the points of multiplicity at least two#✓fully proved

Let \(A\) be a line arrangement in the projective plane over a field. A point \(p\) is a singular point of \(A\) if and only if its multiplicity \(m_p\) in \(A\), the number of lines of \(A\) through \(p\), satisfies \(m_p \ge 2\).

theorem mem_singularPoints_iff {p : ℙ K (Fin 3 → K)} :
    p ∈ A.singularPoints ↔ 2 ≤ A.multiplicity p

Uses 4

Statement usesLine arrangement · Multiplicity of a point in a line arrangement · Singular points of a line arrangement

Proof usesSingular points lie on two distinct lines

TheoremMultiplicity is at most the number of lines#✓fully proved

Let \(A\) be an arrangement of \(d\) lines in the projective plane over a field. Every point \(p\) has multiplicity \(m_p \le d\) in \(A\).

theorem multiplicity_le_card (p : ℙ K (Fin 3 → K)) : A.multiplicity p ≤ A.lines.card

Uses 2

Statement usesLine arrangement · Multiplicity of a point in a line arrangement

TheoremEvery line arrangement has a singular point#✓fully proved

Every line arrangement in the projective plane over a field has at least one singular point, since any two of its distinct lines meet.

theorem singularPoints_nonempty : A.singularPoints.Nonempty

Uses 3

Statement usesLine arrangement · Singular points of a line arrangement

Proof usesSingular points lie on two distinct lines

DefinitionHarbourne constant of a line arrangement#✓fully proved

Let \(A\) be an arrangement of \(d\) lines in the projective plane over a field, let \(S\) be its set of singular points, with \(s\) elements, and let \(m_p\) be the multiplicity of a point \(p\) in \(A\). The Harbourne constant of \(A\) is the real number

\[H(A) = \frac{d^2 - \sum_{p \in S} m_p^2}{s}.\]

Every arrangement has a singular point, so \(s \ge 1\). The number \(H(A)\) is the self-intersection of the strict transform of the arrangement on the blow-up of its singular points, divided by \(s\).

noncomputable def hConstant : ℝ :=
  ((A.lines.card : ℝ) ^ 2 - ∑ p ∈ A.singularPoints, (A.multiplicity p : ℝ) ^ 2) /
    A.singularPoints.card

Uses 3

Statement usesLine arrangement · Multiplicity of a point in a line arrangement · Singular points of a line arrangement

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.