Module

ConnectedActions.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.ConnectedActions

1 declaration indexed from sourceView source ↗

Module documentation

Connected objects and transitive fiber actions

For a fiber functor on a Galois category, an object with nonempty fiber is connected if the canonical fundamental-group action on its fiber is pretransitive.

Imports1

Mathlib.CategoryTheory.Galois.Action

Imported by7

theorem

isConnected_of_isPretransitive

L34 ↗

CategoryTheory.PreGaloisCategory.FiberFunctor.isConnected_of_isPretransitive

Documentation

An object with nonempty fiber is connected if the canonical Aut F-action on its fiber is pretransitive.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
open Limits _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]

Lean source · statement

theorem FiberFunctor.isConnected_of_isPretransitive
    (X : C) [Nonempty (F.obj X)]
    [MulAction.IsPretransitive (Aut F) (F.obj X)] :
    IsConnected X

Module documentation

Connected objects and transitive fiber actions

Declarations

isConnected_of_isPretransitive