NYLL
Module

AbelianPrimeToTateComparison.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianPrimeToTateComparison
9 declarations indexed from sourceView source ↗

Module documentation

The actual prime-to-p fundamental group and Tate module

The kernel of all invertible multiplication coordinates is the actual residual core for finite groups of order prime to the characteristic. One inclusion uses the actual finite torsion groups and Cauchy's theorem. The other uses the actual image of the multiplication-cover fundamental group and powers in finite Sigma quotients. No p-primary part is discarded by hypothesis.

Imports11
Imported by1

Declarations

theorem

sigmaNumber_of_unitIndex

L43 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.sigmaNumber_of_unitIndex
Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
section Indices
variable (p : ℕ) [CharP K p]
Lean source · statement
theorem sigmaNumber_of_unitIndex (n : unitIndices K) :
    FiniteGroupClass.IsSigmaNumber ({p}ᶜ : Set ℕ) (n.1 : ℕ)
theorem

mem_unitIndices_iff_coprime

L54 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.mem_unitIndices_iff_coprime
Documentation

The invertible positive indices are precisely those prime to the characteristic.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
section Indices
variable (p : ℕ) [CharP K p]
variable [Fact p.Prime]
Lean source · statement
theorem mem_unitIndices_iff_coprime (n : ℕ+) :
    n ∈ unitIndices K ↔ (n : ℕ).Coprime p
theorem

isUnit_of_sigmaNumber

L60 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.isUnit_of_sigmaNumber
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
section Indices
variable (p : ℕ) [CharP K p]
variable [Fact p.Prime]
Lean source · statement
theorem isUnit_of_sigmaNumber (n : ℕ)
    (hn : FiniteGroupClass.IsSigmaNumber ({p}ᶜ : Set ℕ) n) : IsUnit (n : K)
instance

(anonymous instance)

L74 ↗
Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
variable [IsSepClosed K] {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  (p : ℕ) [Fact p.Prime] [CharP K p]
Lean source · statement
instance (n : ℕ+) : TopologicalSpace (torsionLevel (G.AlgPoints hc K) n)
instance

(anonymous instance)

L77 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
variable [IsSepClosed K] {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  (p : ℕ) [Fact p.Prime] [CharP K p]
local instance (n : ℕ+) : TopologicalSpace (torsionLevel (G.AlgPoints hc K) n) :=
  FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
instance (n : ℕ+) : DiscreteTopology (torsionLevel (G.AlgPoints hc K) n)
theorem

toTateHom_ker_eq_residualCore

L81 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.toTateHom_ker_eq_residualCore
Documentation

The kernel of the actual compatible-family map is precisely the actual prime-to-p residual core of the original fundamental group.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
variable [IsSepClosed K] {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  (p : ℕ) [Fact p.Prime] [CharP K p]
local instance (n : ℕ+) : TopologicalSpace (torsionLevel (G.AlgPoints hc K) n) :=
  FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel (G.AlgPoints hc K) n) := ⟨rfl⟩
Lean source · statement
theorem toTateHom_ker_eq_residualCore :
    (toTateHom G hc).toMonoidHom.ker =
      proCResidualCore (FiniteGroupClass.sigmaGroup ({p}ᶜ : Set ℕ))
        π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)
def

fundamentalGroupPrimeToEquivTate

L112 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fundamentalGroupPrimeToEquivTate
Documentation

The maximal prime-to-p quotient of the actual etale fundamental group is the inverse limit of the actual torsion points at all prime-to-p indices.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
variable [IsSepClosed K] {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  (p : ℕ) [Fact p.Prime] [CharP K p]
local instance (n : ℕ+) : TopologicalSpace (torsionLevel (G.AlgPoints hc K) n) :=
  FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel (G.AlgPoints hc K) n) := ⟨rfl⟩
Lean source · statement
def fundamentalGroupPrimeToEquivTate :
    (π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1) ⧸
      proCResidualCore (FiniteGroupClass.sigmaGroup ({p}ᶜ : Set ℕ))
        π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) ≃ₜ*
      Multiplicative (RestrictedTateModule (G.AlgPoints hc K) (unitIndices K))
theorem

fundamentalGroupPrimeToEquivTate_projection

L142 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fundamentalGroupPrimeToEquivTate_projection
Documentation

Every coordinate is the action on the actual unit of the actual multiplication fibre.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
variable [IsSepClosed K] {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  (p : ℕ) [Fact p.Prime] [CharP K p]
local instance (n : ℕ+) : TopologicalSpace (torsionLevel (G.AlgPoints hc K) n) :=
  FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel (G.AlgPoints hc K) n) := ⟨rfl⟩
Lean source · statement
theorem fundamentalGroupPrimeToEquivTate_projection
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) (n : unitIndices K) :
    RestrictedTateModule.projection (G.AlgPoints hc K) (unitIndices K) n
      (Multiplicative.toAdd (fundamentalGroupPrimeToEquivTate G hc p
        (QuotientGroup.mk'
          (proCResidualCore (FiniteGroupClass.sigmaGroup ({p}ᶜ : Set ℕ))
            π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) g))) = monodromy G hc n g
def

fundamentalGroupPrimeToEquivTateAt

L154 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fundamentalGroupPrimeToEquivTateAt
Documentation

At any separably closed geometric basepoint, the same actual prime-to-p Tate module describes the maximal prime-to-p quotient. The basepoint comparison is chosen internally from the actual fibre-functor comparison theorem.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open ProCGroups ProCGroups.ProC
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
variable [IsSepClosed K] {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
  (p : ℕ) [Fact p.Prime] [CharP K p]
local instance (n : ℕ+) : TopologicalSpace (torsionLevel (G.AlgPoints hc K) n) :=
  FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel (G.AlgPoints hc K) n) := ⟨rfl⟩
Lean source · statement
def fundamentalGroupPrimeToEquivTateAt
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ A) :
    (π₁ᵉᵗ(xi) ⧸ proCResidualCore (FiniteGroupClass.sigmaGroup ({p}ᶜ : Set ℕ)) π₁ᵉᵗ(xi)) ≃ₜ*
      Multiplicative (RestrictedTateModule (G.AlgPoints hc K) (unitIndices K))

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