GoodReductionJacobian.RelativeGroupLaw.natCard_torsionLevel_eq_pow
A positive multiplication kernel of a proper smooth commutative group scheme of dimension d has exactly n ^ (2 * d) algebraic points in characteristic zero.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer
namespace GoodReductionJacobian.RelativeGroupLawLean source · statement
theorem natCard_torsionLevel_eq_pow
{K : Type} [Field K] [IsAlgClosed K] [CharZero K]
{A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
(G : RelativeGroupLaw K f) (hc : G.IsCommutative)
(hA : AbelianSchemePropertyBundle K f)
(d : ℕ) [SmoothOfRelativeDimension d f] (n : ℕ+) :
Nat.card (ProCGroups.torsionLevel (G.AlgPoints hc K) n) =
(n : ℕ) ^ (2 * d)