NYLL
Module

AbelianUnitTateFamilies.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianUnitTateFamilies
8 declarations indexed from sourceView source ↗

Module documentation

Actual compatible torsion families at invertible indices

Unit monodromy gives actual compatible torsion points. Every such family is realized by compactness: any finite set of its coordinates is realized at the product of their indices, which remains invertible in the ground field.

Imports5
Imported by2

Declarations

theorem

transition_unit

L35 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.transition_unit
Documentation

The actual multiplication transition preserves the distinguished unit fibre point.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem transition_unit (n m : unitIndices K) :
    (fiber (G.one (𝟙 (Spec (.of K)))).1).map (transition G hc n m)
      (unit G hc (n * m)) = unit G hc n
theorem

monodromy_compatible

L44 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy_compatible
Documentation

Monodromy is compatible with the actual full Tate transition, without choosing independent identifications of the torsion levels.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem monodromy_compatible (n m : unitIndices K)
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    ProCGroups.torsionTransition (G.AlgPoints hc K) n.1 m.1
      (monodromy G hc (n * m) g) = monodromy G hc n g
def

toTate

L56 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.toTate
Documentation

The actual compatible family of torsion points obtained by unit monodromy.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def toTate
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    ProCGroups.RestrictedTateModule (G.AlgPoints hc K) (unitIndices K)
instance

(anonymous instance)

L62 ↗
Source context 6 commands

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

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

(anonymous instance)

L65 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth 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
instance (n : ℕ+) : DiscreteTopology (ProCGroups.torsionLevel (G.AlgPoints hc K) n)
theorem

toTate_continuous

L69 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.toTate_continuous
Documentation

The compatible-family map is continuous in the actual full Tate topology.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth 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
local instance (n : ℕ+) : DiscreteTopology (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ⟨rfl⟩
Lean source · statement
theorem toTate_continuous :
    Continuous (toTate G hc)
theorem

toTate_surjective

L75 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.toTate_surjective
Documentation

Compactness realizes every actual compatible torsion family simultaneously.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth 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
local instance (n : ℕ+) : DiscreteTopology (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ⟨rfl⟩
Lean source · statement
theorem toTate_surjective [GeometricallyConnected f] :
    Function.Surjective (toTate G hc)
def

toTateHom

L111 ↗
GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.toTateHom
Documentation

Actual unit monodromy as a continuous homomorphism to compatible torsion families.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication
variable {K : Type} [Field K] [IsSepClosed K]
  {A : Scheme} {f : A ⟶ Spec (.of K)} [IsProper f] [Smooth 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
local instance (n : ℕ+) : DiscreteTopology (ProCGroups.torsionLevel (G.AlgPoints hc K) n) :=
  ⟨rfl⟩
Lean source · full declaration
def toTateHom :
    π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1) →ₜ*
      Multiplicative (ProCGroups.RestrictedTateModule (G.AlgPoints hc K) (unitIndices K)) where
  toFun g := Multiplicative.ofAdd (toTate G hc g)
  map_one' := by
    apply congrArg Multiplicative.ofAdd
    apply Subtype.ext
    funext n
    exact monodromy_one G hc n
  map_mul' g h := by
    apply congrArg Multiplicative.ofAdd
    apply Subtype.ext
    funext n
    exact monodromy_mul G hc n g h
  continuous_toFun := toTate_continuous G hc

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