NYLL
Module

AbelianMultiplicationMonodromyGroup.lean

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

Module documentation

Additivity of actual multiplication monodromy

The torsion comparison preserves the underlying scheme point. Translation by that same point therefore acts on the actual geometric fibre by torsion addition. Naturality of a fibre-functor automorphism against these deck translations makes its action translation by its value at the unit. Thus unit evaluation sends the fundamental-group product to actual torsion addition.

Imports12
Imported by4

Declarations

theorem

scalarIdentity_specMap

L41 ↗
GoodReductionJacobian.RelativeGroupLaw.scalarIdentity_specMap
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (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.torsionPointSection
Documentation

The actual torsion point, with the identity spectrum map as base.

Source context 7 commands

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

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

torsionPointSection_isTorsion

L55 ↗
GoodReductionJacobian.RelativeGroupLaw.torsionPointSection_isTorsion
Documentation

The section underlying an algebraic torsion point is annihilated by the same multiplication map.

Source context 7 commands

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

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

torsionDeckTranslation

L75 ↗
GoodReductionJacobian.RelativeGroupLaw.torsionDeckTranslation
Documentation

The deck translation of the multiplication cover defined by an actual torsion point.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
Lean source · statement
def torsionDeckTranslation [CharZero K] [IsProper f] [Smooth f] (n : ℕ+)
    (t : ProCGroups.torsionLevel (G.AlgPoints hc K) n) :
    Aut (G.multiplicationCover hc n)
theorem

fiberEquiv_map_torsionDeckTranslation

L85 ↗
GoodReductionJacobian.RelativeGroupLaw.fiberEquiv_map_torsionDeckTranslation
Documentation

The torsion-fibre comparison carries the actual deck translation to addition by its defining point.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f]
Lean source · statement
theorem fiberEquiv_map_torsionDeckTranslation (n : ℕ+)
    (t : ProCGroups.torsionLevel (G.AlgPoints hc K) n)
    (z : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (G.multiplicationCover hc n)) :
    G.multiplicationCoverFiberEquivTorsion hc n
        ((FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).map
          (torsionDeckTranslation G hc n t).hom z) =
      G.multiplicationCoverFiberEquivTorsion hc n z + t
theorem

multiplicationCoverFiberEquivTorsion_smul

L137 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationCoverFiberEquivTorsion_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 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f]
Lean source · statement
theorem multiplicationCoverFiberEquivTorsion_smul (n : ℕ+)
    (g : π₁ᵉᵗ((G.one (𝟙 (Spec (CommRingCat.of K)))).1))
    (z : (FiniteEtale.fiber (G.one (𝟙 (Spec (CommRingCat.of K)))).1).obj
      (G.multiplicationCover hc n)) :
    G.multiplicationCoverFiberEquivTorsion hc n (g • z) =
      G.multiplicationMonodromy hc n g + G.multiplicationCoverFiberEquivTorsion hc n z
theorem

multiplicationMonodromy_one

L164 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationMonodromy_one
Documentation

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

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f]
Lean source · statement
theorem multiplicationMonodromy_one (n : ℕ+) :
    G.multiplicationMonodromy hc n 1 = 0
theorem

multiplicationMonodromy_mul

L172 ↗
GoodReductionJacobian.RelativeGroupLaw.multiplicationMonodromy_mul
Documentation

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

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue
namespace GoodReductionJacobian.RelativeGroupLaw
variable {K : Type} [Field K] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
variable (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
variable [IsAlgClosed K] [CharZero K] [IsProper f] [Smooth f]
Lean source · statement
theorem multiplicationMonodromy_mul (n : ℕ+)
    (g h : π₁ᵉᵗ((G.one (𝟙 (Spec (CommRingCat.of K)))).1)) :
    G.multiplicationMonodromy hc n (g * h) =
      G.multiplicationMonodromy hc n g + G.multiplicationMonodromy hc n h

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