Pappus's hexagon theorem over any commutative ring

Points are homogeneous coordinate vectors in R³, collinearity is the vanishing of the triple product and the meet of two lines is a cross product of cross products. If A, B, C are collinear and a, b, c are collinear, the meets of Ab, aB, of Ac, aC and of Bc, bC are collinear (Theorem of the Day). It holds over any commutative ring with no non-degeneracy hypothesis: the triple product of the meets is c₁·det[A,B,C] + c₂·det[a,b,c] with integer polynomial cofactors of degree 9, found by a Gröbner basis computation and checked by linear_combination.

Main results

• Pappus.pappus: Pappus's hexagon theorem in homogeneous coordinates over any commutative ring

References

• R. Whitty, Theorem of the Day, «Pappus' Theorem» (GeometryAndTrigonometry/Pappus).
• Pappus of Alexandria, Collection, Book VII (c. 320 AD).

theorem Pappus.pappus {R : Type u_1} [CommRing R] (A B C a b c : Fin 3 → R) (h₁ : A ⬝ᵥ (crossProduct B) C = 0) (h₂ : a ⬝ᵥ (crossProduct b) c = 0) : (crossProduct ((crossProduct A) b)) ((crossProduct a) B) ⬝ᵥ (crossProduct ((crossProduct ((crossProduct A) c)) ((crossProduct a) C))) ((crossProduct ((crossProduct B) c)) ((crossProduct b) C)) = 0

Pappus's hexagon theorem. If A, B, C are collinear and a, b, c are collinear (vanishing triple products), then the meets Ab ∩ aB, Ac ∩ aC, Bc ∩ bC are collinear. Over any commutative ring, without non-degeneracy hypotheses.