NYLL
Module

AbelianMultiplicationMonodromy.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianMultiplicationMonodromy
6 declarations indexed from sourceView source ↗

Module documentation

Separation by actual multiplication monodromy

Evaluation at the unit of each multiplication cover gives a surjective continuous map to its actual torsion fibre. The collection of these maps separates the actual fundamental group: commutativity and transitivity recover the whole fibre action from its value at the unit, and cofinality then detects every Galois fibre.

Imports9
Imported by6

Declarations

def

multiplicationCoverUnit

L41 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverUnit
Documentation

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

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def multiplicationCoverUnit (n : ℕ+) :
    (fiber (G.one (𝟙 (Spec (.of K)))).1).obj (G.multiplicationCover hc n)
def

multiplicationMonodromy

L46 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationMonodromy
Documentation

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

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def multiplicationMonodromy (n : ℕ+)
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    ProCGroups.torsionLevel (G.AlgPoints hc K) n
theorem

multiplicationMonodromy_surjective

L52 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationMonodromy_surjective
Documentation

Connectedness of the multiplication cover makes unit evaluation surjective.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem multiplicationMonodromy_surjective (n : ℕ+) :
    Function.Surjective (G.multiplicationMonodromy hc n)
instance

(anonymous instance)

L64 ↗
Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n)
theorem

multiplicationMonodromy_continuous

L69 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationMonodromy_continuous
Documentation

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

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
omit [GeometricallyConnected f] in
Lean source · statement
theorem multiplicationMonodromy_continuous (n : ℕ+) :
    Continuous (G.multiplicationMonodromy hc n)
theorem

fundamentalGroup_ext_of_multiplicationMonodromy

L76 ↗
GoodReductionJacobian.RelativeGroupLaw.fundamentalGroup_ext_of_multiplicationMonodromy
Documentation

All actual multiplication fibres together detect the fundamental group.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f] [GeometricallyConnected f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
local instance (n : ℕ+) : TopologicalSpace (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ProCGroups.FullTateModule.torsionLevelTopology (G.AlgPoints hc K) n
Lean source · statement
theorem fundamentalGroup_ext_of_multiplicationMonodromy
    (g h : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1))
    (hgh : ∀ n : ℕ+, G.multiplicationMonodromy hc n g = G.multiplicationMonodromy hc n h) :
    g = h

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