GoodReductionJacobian.RelativeGroupLaw.character_factors_multiplicationMonodromy
A character of exponent dividing n is evaluated on the actual n-torsion displacement of the multiplication cover.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry
namespace GoodReductionJacobian.RelativeGroupLawLean source · statement
theorem character_factors_multiplicationMonodromy
{K : Type} [Field K] [IsAlgClosed K] [CharZero K]
{J : Scheme} {b : J ⟶ Spec (.of K)}
[IsProper b] [Smooth b] [GeometricallyConnected b]
(G : RelativeGroupLaw K b) (hc : G.IsCommutative)
{H : Type} [AddCommGroup H] (n : ℕ+)
(χ : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1) →* Multiplicative H)
(hH : ∀ a : H, (n : ℕ) • a = 0) :
∃ ψ : ProCGroups.torsionLevel (G.AlgPoints hc K) n →+ H,
∀ g, ψ (G.multiplicationMonodromy hc n g) = (χ g).toAdd