Module

AbelianUnitMonodromyKernel.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AbelianUnitMonodromyKernel

2 declarations indexed from sourceView source ↗

Module documentation

The kernel of actual multiplication monodromy

The stabilizer of the actual unit point is the image of the fundamental group of the multiplication cover. The actual pointed map of multiplication induces the corresponding power map on the fundamental group.

Imports5

Imported by2

theorem

unit_eq_liftedPoint

L33 ↗

GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.unit_eq_liftedPoint

Documentation

The distinguished torsion-fibre unit is the actual lift of the unit section.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.FiniteEtale
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 unit_eq_liftedPoint (n : unitIndices K) :
    unit G hc n =
      (fiberObjEquivHom (G.one (𝟙 (Spec (.of K)))).1 (cover G hc n)).symm
        (Over.homMk (G.one (𝟙 (Spec (.of K)))).1 (G.unit_comp_schemeNsmul (n.1 : ℕ)))

theorem

monodromy_eq_zero_iff_exists_pow

L59 ↗

GoodReductionJacobian.RelativeGroupLaw.UnitMultiplication.monodromy_eq_zero_iff_exists_pow