Weil conjectures in terms of point counts

weil_conjectures

Submitter: Junyan Xu.

Notes: Unavailable.

Source: P. Deligne, 'La conjecture de Weil. I', Publications Mathématiques de l'Institut des Hautes Études Scientifiques, Volume 43, pages 273–307 (1974), https://www.numdam.org/item/PMIHES_1974__43__273_0.pdf. See also references in the Lean file.

Informal solution: Deligne's proof of the Riemann hypothesis in Weil I was based upon combining Grothendieck's ℓ-adic cohomological theory of L-functions, the monodromy theory of Lefschetz pencils, and Deligne's own stunning transposition to the function field case of Rankin's method of 'squaring'. Deligne's proof of Weil II is generally regarded as being much deeper and more difficult than his proof of Weil I, but in the spring of 1984, Laumon found a significant simplification based upon Fourier transform ideas. Katz's lectures present a further simplification of Laumon's simplification of Deligne's proof of Weil II. A purely p-adic proof using rigid cohomology is available from the paper by Kedlaya.

theorem declaration uses `sorry`weil_conjectures (F : Type*) [Finite F] [Field F]
    (X : Over (Spec (.of F))) [GeometricallyIrreducible X.hom] [IsProper X.hom]
    (d : ℕ) [SmoothOfRelativeDimension d X.hom] :
    ∃ A : ℕ → Multiset ℂ, A 0 = {1} ∧
      (∀ i ≤ 2 * d, A (2 * d - i) = (A i).map (Nat.card F ^ d / · : ℂ → ℂ) ∧
        (∀ φ : ℂ ≃+* ℂ, (A i).map φ = A i) ∧
        ∀ α ∈ A i, IsIntegral ℤ α ∧ ‖α‖ = √(Nat.card F ^ i)) ∧
      ∀ (E : Type _) [Field E] [Algebra F E] [FiniteDimensional F E],
        Nat.card (.mk (Spec.map <| CommRingCat.ofHom <| algebraMap F E) ⟶ X) =
        ∑ i ∈ Finset.Iic (2 * d), (-1) ^ i * ((A i).map (· ^ Module.finrank F E)).sum := byF:Type u_1inst✝⁴:Finite Finst✝³:Field FX:Over (Spec (CommRingCat.of F))inst✝²:GeometricallyIrreducible X.hominst✝¹:IsProper X.homd:ℕinst✝:SmoothOfRelativeDimension d X.hom⊢ ∃ A,
  A 0 = {1} ∧
    (∀ i ≤ 2 * d,
        A (2 * d - i) = Multiset.map (fun x => ↑(Nat.card F) ^ d / x) (A i) ∧
          (∀ (φ : ℂ ≃+* ℂ), Multiset.map (⇑φ) (A i) = A i) ∧
            ∀ α ∈ A i, _root_.IsIntegral ℤ α ∧ ‖α‖ = √(↑(Nat.card F) ^ i)) ∧
      ∀ (E : Type u_1) [inst : Field E] [inst_1 : Algebra F E] [FiniteDimensional F E],
        ↑(Nat.card (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap F E))) ⟶ X)) =
          ∑ i ∈ Finset.Iic (2 * d), (-1) ^ i * (Multiset.map (fun x => x ^ Module.finrank F E) (A i)).sum
  sorryAll goals completed! 🐙

Solved by

Not yet solved.