NYLL
Module

TateModule.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.TateModule
6 declarations indexed from sourceView source ↗

Module documentation

The full Tate module of algebraic points

The actual torsion levels of the additive group of algebraic points identify with points of the multiplication kernel. For a proper smooth commutative group scheme over an algebraically closed field of characteristic zero, these kernels are finite étale. Thus the full Tate module has finite levels and is compact in its canonical topology. Its Hausdorff, totally disconnected, and torsion-free structures are supplied by the general full Tate construction.

Imports9
Imported by6

Declarations

theorem

comp_nsmul_idPoint

L40 ↗
GoodReductionJacobian.RelativeGroupLaw.comp_nsmul_idPoint
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem comp_nsmul_idPoint {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of K))
    (n : ℕ) (x : SchemeHomOver t f) :
    NeronModelInfra.schemeHomOverComp x (G.nsmul f n idPoint) = G.nsmul t n x
def

torsionSubsetChangeBase

L51 ↗
GoodReductionJacobian.RelativeGroupLaw.torsionSubsetChangeBase
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · full declaration
def torsionSubsetChangeBase (n : ℕ)
    (t t' : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of K)) (h : t = t') :
    G.torsionSubset t n ≃ G.torsionSubset t' n where
  toFun x := ⟨⟨x.1.1, x.1.2.trans h⟩, by
    subst t'
    exact x.2⟩
  invFun x := ⟨⟨x.1.1, x.1.2.trans h.symm⟩, by
    subst t'
    exact x.2⟩
  left_inv x := by
    apply Subtype.ext
    apply Subtype.ext
    rfl
  right_inv x := by
    apply Subtype.ext
    apply Subtype.ext
    rfl
def

torsionLevelEquivSchemeKerPoints

L71 ↗
GoodReductionJacobian.RelativeGroupLaw.torsionLevelEquivSchemeKerPoints
Documentation

The actual torsion subgroup of algebraic points is the point set of the scheme theoretic multiplication kernel.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def torsionLevelEquivSchemeKerPoints (n : ℕ+) :
    ProCGroups.torsionLevel (G.AlgPoints hc K) n ≃
      SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) (G.schemeKerStr (n : ℕ))
theorem

torsionLevelEquivSchemeKerPoints_comp_fst

L96 ↗
GoodReductionJacobian.RelativeGroupLaw.torsionLevelEquivSchemeKerPoints_comp_fst
Documentation

The scheme-kernel comparison preserves the underlying point of the group scheme.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem torsionLevelEquivSchemeKerPoints_comp_fst (n : ℕ+)
    (x : ProCGroups.torsionLevel (G.AlgPoints hc K) n) :
    (G.torsionLevelEquivSchemeKerPoints hc n x).1 ≫
        pullback.fst (G.schemeNsmul (n : ℕ)) (G.one (𝟙 (Spec (CommRingCat.of K)))).1 =
      (AlgPoints.toPoint x.1).1
theorem

finite_torsionLevel

L106 ↗
GoodReductionJacobian.RelativeGroupLaw.finite_torsionLevel
Documentation

Properness and smoothness make every positive torsion level finite in characteristic zero, without any separate finiteness hypothesis on points.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem finite_torsionLevel [IsAlgClosed K] [CharZero K] [IsProper f]
    (d : ℕ) [SmoothOfRelativeDimension d f] (n : ℕ+) :
    Finite (ProCGroups.torsionLevel (G.AlgPoints hc K) n)
theorem

compactSpace_fullTateModule

L124 ↗
GoodReductionJacobian.RelativeGroupLaw.compactSpace_fullTateModule
Documentation

The full Tate module of actual algebraic points is compact.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem compactSpace_fullTateModule [IsAlgClosed K] [CharZero K] [IsProper f]
    (d : ℕ) [SmoothOfRelativeDimension d f] :
    CompactSpace (ProCGroups.FullTateModule (G.AlgPoints hc K))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.