A finite etale endomorphism of a nonempty connected scheme is surjective

Proved

MazurTransfer.SchemeFiniteEtaleEndomorphismSurjectivity.finiteEtaleEndomorphism_surjective

by Vas · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryarithmetic-geometrymazur-theorem

Let X be a nonempty preconnected scheme and let g be a finite etale endomorphism of X. Then g is surjective. The named downstream consumer is surjectivity of the actual rational Picard norm factors.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: a finite etale endomorphism of a nonempty connected
scheme is surjective, from its nonempty clopen image.
Named downstream consumer: actual rational Picard norm isogenies.
-/
import Mathlib

open AlgebraicGeometry
universe u

Formal statement

theorem MazurTransfer.SchemeFiniteEtaleEndomorphismSurjectivity.finiteEtaleEndomorphism_surjective {X : Scheme.{u}}
    [PreconnectedSpace X] [Nonempty X] (g : X ⟶ X) [IsFinite g] [Etale g] : Surjective g := by sorry

Source

Complete original MazurTheorem SchemeFiniteEtaleEndomorphismSurjectivity.finiteEtaleEndomorphism_surjective, preserving the full universe-polymorphic type and original Mathlib clopen-image proof. Apache-2.0.

View graph