Prime multiplication has a Zariski-open set of divisible points

Open

PhilipponMultiplicity.prime_nsmul_range_has_nonempty_interior

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

algebraic-geometryalgebraic-groupsphilippon-multiplicityproof-frontier

Let $G$ be a commutative algebraic group over a Philippon base field $K$ (isometrically isomorphic to $\mathbb C$ or $\mathbb C_p$ ), and let $\ell$ be a prime integer. The image of multiplication by $\ell$ contains a nonempty Zariski-open subset of $G(K)$ :

\operatorname{Int}_{\mathrm{Zar}}\{\ell x:x\in G(K)\}\ne\varnothing.

Equivalently, there is a nonempty Zariski-open set $U\subseteq G(K)$ such that every point of $U$ is divisible by $\ell$ in $G(K)$ . Connectedness is not assumed. This local input supports the separate checked passage to global divisibility on a connected group.

Formalization Note. An accepted sketch reduces this assertion to constructibility of the multiplication image and nonempty interior of its Zariski closure. The passage from these two assertions to the original interior conclusion is proved for arbitrary topological spaces by a boundary argument. The two geometric statements in the concrete embedded-group interface remain Open. Connectedness and a regular choice of roots are not assumed; zero-dimensional groups are included.

Preamble

import Definitions.Def_PhilipponMultiplicity_Geometry
set_option autoImplicit false

Formal statement

namespace PhilipponMultiplicity

theorem prime_nsmul_range_has_nonempty_interior
    (K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K)
    (G : EmbeddedGroupProduct K) (p : ℕ) (hp : p.Prime) :
    (@interior _ G.zariskiTopology (Set.range (fun x : G.Point => p • x))).Nonempty := by sorry

end PhilipponMultiplicity

Source

J. Garnek, Abelian varieties over p-adic fields, doctoral dissertation (2020), Lemma 1.1.2 and its differential argument, p.16: https://jgarnek.faculty.wmi.amu.edu.pl/papers/phd_final.pdf . The Stacks Project, Proposition 59.26.2(9), tag 03PA, openness of etale morphisms: https://stacks.math.columbia.edu/tag/03PA . Auxiliary local-image consequence for prime multiplication in characteristic zero, without connectedness. Constructing the multiplication morphism, proving its local etaleness, and relating its image to the concrete group-point topology remain Open.

View graph