NYLL
Module

AbelianUnitMonodromy.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianUnitMonodromy
14 declarations indexed from sourceView source ↗

Module documentation

Monodromy at actual torsion points in arbitrary characteristic

For every invertible positive integer, the actual multiplication fibre is a torsor under its torsion points. Deck translations prove that unit monodromy is an additive map to the actual torsion group.

Imports11
Imported by4

Declarations

theorem

scalarIdentity_specMap

L42 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.scalarIdentity_specMap
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem scalarIdentity_specMap :
    Spec.map (CommRingCat.ofHom (algebraMap K K)) = 𝟙 (Spec (CommRingCat.of K))
def

torsionPointSection

L48 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.torsionPointSection
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def torsionPointSection (n : unitIndices K)
    (t : ProCGroups.torsionLevel (G.AlgPoints hc K) n.1) :
    SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f
theorem

torsionPointSection_isTorsion

L53 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.torsionPointSection_isTorsion
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem torsionPointSection_isTorsion (n : unitIndices K)
    (t : ProCGroups.torsionLevel (G.AlgPoints hc K) n.1) :
    G.IsTorsionPoint (𝟙 (Spec (CommRingCat.of K))) (n.1 : ℕ)
      (torsionPointSection G hc n t)
def

unit

L75 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.unit
Documentation

The unit in the actual geometric fibre of the multiplication cover.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
Lean source · statement
def unit (n : unitIndices K) :
    (fiber (G.one (𝟙 (Spec (.of K)))).1).obj (cover G hc n)
def

monodromy

L80 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy
Documentation

Evaluation of actual monodromy at the unit, expressed in actual torsion points.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
Lean source · statement
def monodromy (n : unitIndices K)
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    ProCGroups.torsionLevel (G.AlgPoints hc K) n.1
theorem

monodromy_surjective

L86 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy_surjective
Documentation

Connectedness of the multiplication cover makes unit evaluation surjective.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
Lean source · statement
theorem monodromy_surjective [GeometricallyConnected f] (n : unitIndices K) :
    Function.Surjective (monodromy G hc n)
instance

(anonymous instance)

L98 ↗
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
Lean source · statement
instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n)
theorem

monodromy_continuous

L102 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy_continuous
Documentation

Unit evaluation is continuous for the discrete topology on actual torsion points.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
theorem monodromy_continuous (n : unitIndices K) :
    Continuous (monodromy G hc n)
def

torsionDeckTranslation

L108 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.torsionDeckTranslation
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
def torsionDeckTranslation (n : unitIndices K)
    (t : ProCGroups.torsionLevel (G.AlgPoints hc K) n.1) :
    Aut (cover G hc n)
theorem

fiberEquiv_map_torsionDeckTranslation

L115 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fiberEquiv_map_torsionDeckTranslation
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
theorem fiberEquiv_map_torsionDeckTranslation (n : unitIndices K)
    (t : ProCGroups.torsionLevel (G.AlgPoints hc K) n.1)
    (z : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (cover G hc n)) :
    fiberEquivTorsion G hc n
        ((FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).map
          (torsionDeckTranslation G hc n t).hom z) =
      fiberEquivTorsion G hc n z + t
theorem

fiberEquivTorsion_smul

L167 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.fiberEquivTorsion_smul
Documentation

Actual monodromy on every point of a multiplication fibre is addition by its value at the unit, under the actual torsion comparison.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
theorem fiberEquivTorsion_smul (n : unitIndices K)
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (CommRingCat.of K)))).1))
    (z : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (cover G hc n)) :
    fiberEquivTorsion G hc n (g • z) =
      monodromy G hc n g + fiberEquivTorsion G hc n z
theorem

monodromy_one

L194 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy_one
Documentation

Unit evaluation sends the identity of the actual fundamental group to zero.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
theorem monodromy_one (n : unitIndices K) :
    monodromy G hc n 1 = 0
theorem

monodromy_mul

L202 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy_mul
Documentation

Unit evaluation sends the actual fundamental-group product to addition in the actual torsion subgroup of algebraic points.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
theorem monodromy_mul (n : unitIndices K)
    (g h : π₁ᵉᵗ((G.one (𝟙 (Spec (CommRingCat.of K)))).1)) :
    monodromy G hc n (g * h) =
      monodromy G hc n g + monodromy G hc n h
def

monodromyHom

L212 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromyHom
Documentation

Unit evaluation as a continuous homomorphism to the actual finite torsion group.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.FiniteEtale
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsSepClosed K] [IsProper f] [Smooth f]
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · full declaration
def monodromyHom (n : unitIndices K) :
    π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1) →ₜ*
      Multiplicative (ProCGroups.torsionLevel (G.AlgPoints hc K) n.1) where
  toFun g := Multiplicative.ofAdd (monodromy G hc n g)
  map_one' := congrArg Multiplicative.ofAdd (monodromy_one G hc n)
  map_mul' g h := congrArg Multiplicative.ofAdd (monodromy_mul G hc n g h)
  continuous_toFun := monodromy_continuous G hc n

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