Module

FiberFunctorExactness.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.FiberFunctorExactness

1 declaration indexed from sourceView source ↗

Module documentation

Exactness of fiber functors

Fiber functors from Galois categories preserve finite colimits. This follows from the equivalence with finite continuous actions and exactness of the underlying-set functor on those actions.

Imports2

Mathlib.CategoryTheory.Galois.Equivalence
Nyll.EtaleFundamentalGroups.ContinuousActions.FiniteLimitsAndColimits

Imported by2

instance

preservesFiniteColimits

L35 ↗

CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteColimits

Documentation

A fiber functor from a Galois category preserves finite colimits.

Source context 8 commands

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

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

Lean source · statement

instance preservesFiniteColimits :
    PreservesFiniteColimits F

Module documentation

Exactness of fiber functors

Declarations

preservesFiniteColimits