def projectiveEquiv (n : ℕ) : Setoid { v : Fin n → ℚ // v ≠ 0 }

def ProjectiveSpace (n : ℕ) : Type

def projectiveRatPoints (n : ℕ) (eqs : Set (MvPolynomial (Fin n) ℚ)) : Type

structure IrreducibleCurveOverQ : Type

• n : ℕ
• definingEquations : Set (MvPolynomial (Fin self.n) ℚ)
• genus : ℕ
• isHomogeneous (f : MvPolynomial (Fin self.n) ℚ) : f ∈ self.definingEquations → ∃ (d : ℕ), f.IsHomogeneous d
• isIrreducible : (Ideal.span self.definingEquations).IsPrime
• isCurve : ringKrullDim (MvPolynomial (Fin self.n) ℚ ⧸ Ideal.span self.definingEquations) = 2
• genus_of_plane_curve : self.definingEquations.ncard = 1 → self.n = 3 → ∃ (d : ℕ), ∃ f ∈ self.definingEquations, f.IsHomogeneous d ∧ self.genus = (d - 1) * (d - 2) / 2

def IrreducibleCurveOverQ.ratPoints (C : IrreducibleCurveOverQ) : Type

theorem faltings_theorem (C : IrreducibleCurveOverQ) (hg : C.genus > 1) : Finite C.ratPoints