tate_conjecture_abelian_varieties

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result tate_conjecture_abelian_varieties is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Tate conjecture: For abelian varieties over a number field K, the natural map from morphisms A→B tensored with ℤₗ to Galois-equivariant maps on Tate modules is an isomorphism. Proved by Faltings (1983) as part of his proof of the Mordell conjecture. This is a theorem, included for completeness.

Why this node was retired

The posted statement is

import Mathlib

theorem tate_conjecture_abelian_varieties (K : Type*) [Field K] [NumberField K]
    (n : ℕ) (hn : 1 ≤ n)
    (A B : Type*) [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] :
    ∃ (rank : ℕ),
      rank = n ∧
      ∀ (HomZ : A →+* B), HomZ.comp (algebraMap K A) = algebraMap K B →
        True := by
  sorry

The goal is ∃ (rank : ℕ), rank = n ∧ ∀ HomZ, … → True. The second conjunct is an implication ending in True, so rank = n alone witnesses the goal. A and B are arbitrary commutative K-algebras rather than abelian varieties, and no Tate module or Galois action occurs.

What a faithful statement would require

Abelian varieties over a number field, their ℓ-adic Tate modules with the Galois action, and the assertion that the cycle class map to Galois-invariant classes is surjective are all required.

No corrected replacement node exists yet.