theorem · Étale Fundamental Groups and Cohomology

Uniqueness up to isomorphism of a finite-action fiber functor

An exact finite-set-valued functor on finite continuous group actions is isomorphic to the forgetful functor.

Fiber functors play the role of base points in a category of covers, and their automorphisms retain the fundamental-group information. The isomorphism here need not be canonical: identifying a fiber functor up to isomorphism does not choose a preferred identification. This distinction is foundational in the Galois-category theory of SGA 1, with the finite-action version recorded in the Stacks Project.

EtaleFundamentalGroupsAndCohomology on GitHub ↗

Mathematical statement

Let $G$ be a topological group and let $$F:\mathbf{FinCont}(G)\longrightarrow\mathbf{FinSet}$$ preserve finite limits and finite colimits. If $U$ denotes the usual forgetful functor, the theorem proves that a natural isomorphism $U\cong F$ exists.

The group need not be profinite, compact, or Hausdorff. The category consists of finite sets carrying continuous actions. The conclusion is existence of an isomorphism; it does not assert a unique or canonical choice.

Lean code

`CategoryTheory.FiniteContinuousAction.nonempty_iso_forget_of_exact`

Published library source ↗Same source in NYLL ↗

theorem nonempty_iso_forget_of_exact
    (F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
    [PreservesFiniteLimits F] [PreservesFiniteColimits F] :
    Nonempty
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat ≅ F)

In-scope Lean context

universe u

noncomputable section

open CategoryTheory Limits

open scoped FintypeCatDiscrete

namespace CategoryTheory.FiniteContinuousAction

variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Full declaration and proof

@[stacks 0BMV]
theorem nonempty_iso_forget_of_exact
    (F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
    [PreservesFiniteLimits F] [PreservesFiniteColimits F] :
    Nonempty
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat ≅ F) := by
  let t := fiberComparison G F
  let (X : ContAction FintypeCat.{u} G) :
      IsIso (t.app X) :=
    (ConcreteCategory.isIso_iff_bijective
      (t.app X)).mpr
        (fiberComparison_bijective G F X)
  let : IsIso t :=
    NatIso.isIso_of_isIso_app t
  exact ⟨asIso t⟩

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)

References

A. Grothendieck (director), with two exposés by M. Raynaud. Revêtements étales et groupe fondamental (SGA 1). Séminaire de Géométrie Algébrique du Bois Marie 1960–61. Société Mathématique de France, Documents Mathématiques 3, xviii + 327, 2003. Revised and annotated edition of the seminar volume first published in 1971 as Lecture Notes in Mathematics 224.
The Stacks Project Authors. Lemma 58.3.4: Fiber functors on finite continuous group actions. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.

Published source: 470c51fc.

← All selected results in Étale Fundamental Groups and Cohomology