Divisibility of connected commutative group points

Open

PhilipponMultiplicity.connected_group_points_nsmul_surjective

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryalgebraic-groupsphilippon-multiplicityproof-frontier

Let $G$ be a connected commutative algebraic group over a Philippon base field $K$ (isometrically isomorphic to $\mathbb C$ or $\mathbb C_p$ ). For every positive integer $n$ , multiplication by $n$ is surjective on $G(K)$ :

\forall g\in G(K),\quad\exists h\in G(K),\quad nh=g.

This divisibility property lets the degree-invariance reduction rule out nontrivial actions of the point group on finite groups and finite-rank integral lattices.

Formalization Note. The group is the actual finite product of locally closed embedded groups, and connectedness uses its induced Zariski topology. This is the characteristic-zero specialization of Garnek, Lemma 1.1.2, expressed in the repository's embedded-group interface. Its geometric proof in that interface remains Open. No division operation is included in the definitions.

Verified local-to-global reduction. The accepted sketch proves that nonempty interior of a homomorphism's image implies surjectivity into a connected group with continuous translations. It reuses the actual polynomial translation-continuity proofs for the Zariski topology and proves that prime divisibility implies divisibility by every positive integer.

The sole Open dependency is local prime divisibility: each prime multiplication image must contain a nonempty Zariski-open set. This geometric child does not assume connectedness, global divisibility, or a regular choice of roots. Its construction remains Open; propagation through connectedness and prime factors is proved.

Preamble

import Definitions.Def_PhilipponMultiplicity_Support
import Definitions.Def_PhilipponMultiplicity_SectionThree

set_option autoImplicit false
open scoped BigOperators Topology

Formal statement

namespace PhilipponMultiplicity

theorem connected_group_points_nsmul_surjective
    (K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K)
    (G : EmbeddedGroupProduct K)
    (hconnected : @_root_.IsConnected _ G.zariskiTopology Set.univ) :
    ∀ n : ℕ, 0 < n → Function.Surjective (fun g : G.Point => n • g) := by sorry

end PhilipponMultiplicity

Source

J. Garnek, Abelian varieties over p-adic fields, doctoral dissertation, Adam Mickiewicz University (2020), Lemma 1.1.2 and its differential proof, p.16. https://jgarnek.faculty.wmi.amu.edu.pl/papers/phd_final.pdf . Characteristic-zero specialization to Philippon base fields and the repository embedded-group interface; not a verbatim transcription.

View graph