NYLL
Module

AbelianTateFamilies.lean

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

Module documentation

Actual compatible torsion families from the fundamental group

The maps of multiplication covers give compatibility of monodromy at every positive torsion level. Compactness then realizes every compatible family: finitely many prescribed coordinates are realized at the product of their indices. Separation by multiplication covers gives injectivity.

Imports8
Imported by2

Declarations

theorem

multiplicationCoverTransition_unit

L39 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverTransition_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
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem multiplicationCoverTransition_unit (n m : ℕ+) :
    (fiber (G.one (𝟙 (Spec (.of K)))).1).map (G.multiplicationCoverTransition hc n m)
      (G.multiplicationCoverUnit hc (n * m)) = G.multiplicationCoverUnit hc n
theorem

multiplicationMonodromy_compatible

L48 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationMonodromy_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
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem multiplicationMonodromy_compatible (n m : ℕ+)
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    ProCGroups.torsionTransition (G.AlgPoints hc K) n m
      (G.multiplicationMonodromy hc (n * m) g) = G.multiplicationMonodromy hc n g
def

fundamentalGroupToFullTate

L60 ↗
GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupToFullTate
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
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def fundamentalGroupToFullTate
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    ProCGroups.FullTateModule (G.AlgPoints hc K)
theorem

fundamentalGroupToFullTate_injective

L67 ↗
GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupToFullTate_injective
Documentation

The constructed compatible-family map separates fundamental-group elements.

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 BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
  {A : Scheme} {f : A ⟶ Spec (.of K)}
  [IsProper f] [Smooth f]
  (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
theorem fundamentalGroupToFullTate_injective [GeometricallyConnected f] :
    Function.Injective (G.fundamentalGroupToFullTate hc)
instance

(anonymous instance)

L74 ↗
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 BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero 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)

L77 ↗
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 BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero 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

fundamentalGroupToFullTate_continuous

L81 ↗
GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupToFullTate_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
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero 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 fundamentalGroupToFullTate_continuous :
    Continuous (G.fundamentalGroupToFullTate hc)
theorem

fundamentalGroupToFullTate_surjective

L87 ↗
GoodReductionJacobian.RelativeGroupLaw.fundamentalGroupToFullTate_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
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale
open scoped FintypeCatDiscrete BigOperators
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] [IsAlgClosed K] [CharZero 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 fundamentalGroupToFullTate_surjective [GeometricallyConnected f] :
    Function.Surjective (G.fundamentalGroupToFullTate hc)

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