Module

AbelianTateComparison.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianTateComparison

4 declarations indexed from sourceView source ↗

Module documentation

The actual full Tate module and the fundamental group of an abelian variety

Unit monodromy on the actual multiplication covers identifies the fundamental group with compatible families of actual torsion points. The group law is proved using deck translations, and the bijection and topology come from cofinality of the multiplication covers and compactness.

Imports8

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianTateFamilies
Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationMonodromyGroup
Nyll.EtaleFundamentalGroups.GeometricFiber.BasePoint
Nyll.EtaleFundamentalGroups.GeometricFiber.FundamentalGroup
Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.CategoryTheory.Galois.Topology
Nyll.ProCGroups.Abelian.FullTateModule
Nyll.ProCGroups.Topologies.ContinuousMulEquiv

Imported by4

def

fundamentalGroupToFullTateHom

L38 ↗

GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupToFullTateHom

Documentation

The actual compatible torsion family of unit monodromy, as a continuous group homomorphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · full declaration

def fundamentalGroupToFullTateHom :
    π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1) →ₜ*
      Multiplicative (ProCGroups.FullTateModule (G.AlgPoints hc K)) where
  toFun g := Multiplicative.ofAdd (G.fundamentalGroupToFullTate hc g)
  map_one' := by
    apply congrArg Multiplicative.ofAdd
    apply Subtype.ext
    funext n
    exact G.multiplicationMonodromy_one hc n
  map_mul' g h := by
    apply congrArg Multiplicative.ofAdd
    apply Subtype.ext
    funext n
    exact G.multiplicationMonodromy_mul hc n g h
  continuous_toFun := G.fundamentalGroupToFullTate_continuous hc

def

fundamentalGroupEquivFullTate

L57 ↗

GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupEquivFullTate

Documentation

The etale fundamental group of a proper smooth geometrically connected commutative group over an algebraically closed field of characteristic zero is its actual full Tate module, with the inverse-limit topology.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · statement

def fundamentalGroupEquivFullTate [GeometricallyConnected f] :
    π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1) ≃ₜ*
      Multiplicative (ProCGroups.FullTateModule (G.AlgPoints hc K))

theorem

fundamentalGroupEquivFullTate_projection

L68 ↗

GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupEquivFullTate_projection

Documentation

At every positive integer, the comparison is the actual action on the unit of the multiplication-cover fibre, identified with its torsion point.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · statement

theorem fundamentalGroupEquivFullTate_projection [GeometricallyConnected f]
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) (n : ℕ+) :
    ProCGroups.FullTateModule.projection (G.AlgPoints hc K) n
        (Multiplicative.toAdd (G.fundamentalGroupEquivFullTate hc g)) =
      G.multiplicationMonodromy hc n g

def

fundamentalGroupEquivFullTateAt

L78 ↗

GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupEquivFullTateAt

Documentation

At any separably closed geometric basepoint, the fundamental group is topologically isomorphic to the actual full Tate module of the original group of algebraic points. The basepoint comparison is chosen internally.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)

Lean source · statement

def fundamentalGroupEquivFullTateAt [GeometricallyConnected f]
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ A) :
    π₁ᵉᵗ(xi) ≃ₜ* Multiplicative (ProCGroups.FullTateModule (G.AlgPoints hc K))

Module documentation

The actual full Tate module and the fundamental group of an abelian variety

Declarations

fundamentalGroupToFullTateHom

fundamentalGroupEquivFullTate

fundamentalGroupEquivFullTate_projection

fundamentalGroupEquivFullTateAt