Finite étale covers are invariant under universal homeomorphisms

An integral, universally injective, surjective morphism induces an equivalence of finite étale cover categories and hence the expected pointed fundamental-group isomorphism.

Nilpotent structure and purely inseparable changes can alter a scheme without altering its finite covering theory. This permits passage to reduced schemes or purely inseparable models in fundamental-group calculations, even though constructions involving the full structure sheaf may change. Known as topological invariance of finite étale covers, the result is formulated for universal homeomorphisms in the Stacks Project.

Mathematical statement

Let $f:X\to Y$ be integral, universally injective, and surjective. Pullback induces an equivalence $$f^*:\operatorname{FinEt}(Y)\simeq\operatorname{FinEt}(X).$$ Such a morphism is a universal homeomorphism.

If $X$ and $Y$ are connected and $\xi:\operatorname{Spec}\Omega\to X$ is a geometric point, with $\Omega$ separably closed, the induced homomorphism is a topological group isomorphism $$\pi_1^{\mathrm{et}}(X,\xi)\cong\pi_1^{\mathrm{et}}(Y,f\xi).$$ Its underlying map is exactly the usual fundamental-group homomorphism associated with $f$.

Lean code

`AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_universalHomeomorphism`

Published library source ↗Same source in NYLL ↗

theorem pullback_isEquivalence_of_universalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (FiniteEtale.pullback f).IsEquivalence

In-scope Lean context

noncomputable section

open CategoryTheory Limits

universe u

namespace AlgebraicGeometry.FiniteEtale

attribute [local instance] finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism

Full declaration and proof

/-- Pullback along a universal homeomorphism is an equivalence on finite
étale covers, with no finiteness assumptions on the schemes. -/
@[stacks 0BQN]
theorem pullback_isEquivalence_of_universalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (FiniteEtale.pullback f).IsEquivalence := by
  let P : MorphismProperty Scheme.{u} := @IsFinite ⊓ @Etale
  have hP : (MorphismProperty.Over.pullback P ⊤ f).IsEquivalence := {
    faithful := pullback_faithful_of_integral_universallyInjective_surjective f
    full := pullback_full_of_integral_universallyInjective_surjective f
    essSurj := pullback_essSurj_of_integral_universallyInjective_surjective f
  }
  have htransport (Q : MorphismProperty Scheme.{u}) [Q.IsStableUnderBaseChange]
      (hQ : Q = (@IsFiniteEtale : MorphismProperty Scheme.{u}))
      (h : (MorphismProperty.Over.pullback Q ⊤ f).IsEquivalence) :
      (FiniteEtale.pullback f).IsEquivalence := by
    subst Q
    exact h
  exact htransport P IsFiniteEtale.eq_inf.symm hP

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

Mathematical statement

Lean code

AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_universalHomeomorphism

References

`AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_universalHomeomorphism`