Five criteria for surjectivity on fundamental groups

Mathematical statement

Let $\mathcal C,\mathcal C'$ be Galois categories with fiber functors $F,F'$. Suppose $H:\mathcal C\to\mathcal C'$ preserves a terminal object and is equipped with $F'\circ H\cong F$. It induces $$h:\operatorname{Aut}(F')\longrightarrow\operatorname{Aut}(F).$$

The following are equivalent: $h$ is surjective; $H$ is fully faithful; $H$ sends connected objects to connected objects; every connected $X$ for which $H(X)$ has a section has a section; and, for every $X$, the induced map $$\operatorname{Hom}(1,X)\longrightarrow\operatorname{Hom}(1',H(X))$$ is bijective. Here a section is a morphism from the terminal object.

Lean code

`CategoryTheory.PreGaloisCategory.autHomOfCompIso_surjective_tfae`

Published library source ↗Same source in NYLL ↗

theorem autHomOfCompIso_surjective_tfae
    [PreservesLimitsOfShape (Discrete PEmpty.{1}) H]
    (t : H ⋙ F' ≅ F) :
    List.TFAE [
      Function.Surjective (autHomOfCompIso H t),
      Nonempty H.FullyFaithful,
      ∀ X : C, IsConnected X → IsConnected (H.obj X),
      ∀ X : C, IsConnected X →
        Nonempty (⊤_ C' ⟶ H.obj X) → Nonempty (⊤_ C ⟶ X),
      ∀ X : C, Function.Bijective
        (fun f : (⊤_ C ⟶ X) ↦
          (PreservesTerminal.iso H).inv ≫ H.map f)] := by
  tfae_have 1 → 2 :=
    surjective_implies_fullyFaithful F F' H t
  tfae_have 1 → 3 :=
    surjective_implies_connected F F' H t
  tfae_have 2 → 5 :=
    fullyFaithful_implies_points H
  tfae_have 5 → 4 :=
    points_imply_point_lifting H
  tfae_have 3 → 4 :=
    connected_implies_point_lifting F F' H t
  tfae_have 4 → 1 :=
    point_lifting_implies_surjective F F' H t
  tfae_finish

In-scope Lean context

@[expose] public section

universe g g' u₁ u₂ v₁ v₂ w

noncomputable section

open CategoryTheory Limits

open scoped FintypeCatDiscrete

namespace CategoryTheory.PreGaloisCategory

variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]

variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']

variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]

variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']

variable (H : C ⥤ C')

Full declaration and proof

/--
The five equivalent surjectivity criteria for the homomorphism on fundamental
groups induced by a functor of Galois categories.
-/
@[stacks 0BN6]
theorem autHomOfCompIso_surjective_tfae
    [PreservesLimitsOfShape (Discrete PEmpty.{1}) H]
    (t : H ⋙ F' ≅ F) :
    List.TFAE [
      Function.Surjective (autHomOfCompIso H t),
      Nonempty H.FullyFaithful,
      ∀ X : C, IsConnected X → IsConnected (H.obj X),
      ∀ X : C, IsConnected X →
        Nonempty (⊤_ C' ⟶ H.obj X) → Nonempty (⊤_ C ⟶ X),
      ∀ X : C, Function.Bijective
        (fun f : (⊤_ C ⟶ X) ↦
          (PreservesTerminal.iso H).inv ≫ H.map f)] := by
  tfae_have 1 → 2 :=
    surjective_implies_fullyFaithful F F' H t
  tfae_have 1 → 3 :=
    surjective_implies_connected F F' H t
  tfae_have 2 → 5 :=
    fullyFaithful_implies_points H
  tfae_have 5 → 4 :=
    points_imply_point_lifting H
  tfae_have 3 → 4 :=
    connected_implies_point_lifting F F' H t
  tfae_have 4 → 1 :=
    point_lifting_implies_surjective F F' H t
  tfae_finish

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

The Stacks Project Authors. Lemma 58.4.1: Functors and homomorphisms of fundamental groups. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.