Nyll.JacobianVarieties.Albanese.GenusOneTateComparison

Module documentation

The full Tate module comparison for an arbitrary proper genus-one curve

A closed point supplies a rational basepoint internally. The actual coherent genus comparison and Abel--Jacobi isomorphism then identify the original curve with its constructed Albanese variety. Pullback of finite etale covers transports the fundamental group to the actual full Tate module of its algebraic points.

theorem

exists_fullTate_equiv_of_finrank_H1_eq_one

L36 ↗

JacobianVarieties.Albanese.exists_fullTate_equiv_of_finrank_H1_eq_one

Documentation

A proper smooth integral curve of coherent genus one has fundamental group isomorphic to the actual full Tate module of its constructed Albanese variety. No rational basepoint, curve model, group law, or comparison is assumed.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open AlgebraicGeometry.FiniteEtale
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_fullTate_equiv_of_finrank_H1_eq_one
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    (X : Scheme) [IsIntegral X] (c : X ⟶ Spec (.of K))
    [IsProper c] [SmoothOfRelativeDimension 1 c] (V : X.TwoAffineOpenCover)
    (hg : Module.finrank K (V.structureSheafSections c).H1 = 1) :
    ∃ (A : Scheme) (f : A ⟶ Spec (.of K)) (G : RelativeGroupLaw K f)
      (hc : G.IsCommutative), Smooth f ∧ IsProper f ∧ GeometricallyConnected f ∧
      Nonempty (X ≅ A) ∧
      ∀ (Ω : Type) [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X),
        Nonempty (π₁ᵉᵗ(xi) ≃ₜ* Multiplicative (ProCGroups.FullTateModule (G.AlgPoints hc K)))

Module documentation

The full Tate module comparison for an arbitrary proper genus-one curve

Declarations

exists_fullTate_equiv_of_finrank_H1_eq_one