Module

FiberFunctorComparison.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.FiberFunctorComparison

2 declarations indexed from sourceView source ↗

Module documentation

Comparison of exact functors on a Galois category

An exact functor from a Galois category to finite sets is isomorphic to any chosen fiber functor. As a consequence, exact functors between Galois categories commute with fiber functors up to isomorphism.

Imports2

Imported by3

theorem

nonempty_iso_of_exact

L31 ↗

CategoryTheory.PreGaloisCategory.nonempty_iso_of_exact

Documentation

Any exact finite-set-valued functor on a Galois category is isomorphic to a chosen fiber functor.

Source context 6 commands

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

universe 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]

Lean source · statement

theorem nonempty_iso_of_exact
    (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (P : C ⥤ FintypeCat.{w})
    [PreservesFiniteLimits P] [PreservesFiniteColimits P] :
    Nonempty (F ≅ P)

theorem

nonempty_iso_comp_of_exact

L73 ↗

CategoryTheory.PreGaloisCategory.nonempty_iso_comp_of_exact