Definition and basic properties of Galois categories

We define the notion of a Galois category and a fiber functor as in SGA1, following the definitions in Lenstras notes (see below for a reference).

Main definitions

• PreGaloisCategory : defining properties of Galois categories not involving a fiber functor
• FiberFunctor : a fiber functor from a PreGaloisCategory to FintypeCat
• GaloisCategory : a PreGaloisCategory that admits a FiberFunctor
• IsConnected : an object of a category is connected if it is not initial and does not have non-trivial subobjects

Implementation details

We mostly follow Def 3.1 in Lenstras notes. In axiom (G3) we omit the factorisation of morphisms in epimorphisms and monomorphisms as this is not needed for the proof of the fundamental theorem on Galois categories (and then follows from it).

References

• H. W. Lenstra. Galois theory for schemes

A category C is a PreGalois category if it satisfies all properties of a Galois category in the sense of SGA1 that do not involve a fiber functor. A Galois category should furthermore admit a fiber functor.

The only difference between [PreGaloisCategory C] (F : C ⥤ FintypeCat) [FiberFunctor F] and [GaloisCategory C] is that the former fixes one fiber functor F.

class CategoryTheory.PreGaloisCategory (C : Type u₁) [CategoryTheory.Category.{u₂, u₁} C] : Prop

Definition of a (Pre)Galois category. Lenstra, Def 3.1, (G1)-(G3)

• hasTerminal : CategoryTheory.Limits.HasTerminal C

  C has a terminal object (G1).

• hasPullbacks : CategoryTheory.Limits.HasPullbacks C

  C has pullbacks (G1).

• hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C

  C has finite coproducts (G2).

• hasQuotientsByFiniteGroups : ∀ (G : Type u₂) [inst : Group G] [inst_1 : Finite G], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C

  C has quotients by finite groups (G2).

• monoInducesIsoOnDirectSummand : ∀ {X Y : C} (i : X ⟶ Y) [inst : CategoryTheory.Mono i], ∃ (Z : C) (u : Z ⟶ Y), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))

  Every monomorphism in C induces an isomorphism on a direct summand (G3).

class CategoryTheory.PreGaloisCategory.FiberFunctor {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) : Type (max (max u₁ (u₂ + 1)) (w + 1))

Definition of a fiber functor from a Galois category. Lenstra, Def 3.1, (G4)-(G6)

• preservesTerminalObjects : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F

  F preserves terminal objects (G4).

• preservesPullbacks : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F

  F preserves pullbacks (G4).

• preservesFiniteCoproducts : CategoryTheory.Limits.PreservesFiniteCoproducts F

  F preserves finite coproducts (G5).

• preservesEpis : CategoryTheory.Functor.PreservesEpimorphisms F

  F preserves epimorphisms (G5).

• preservesQuotientsByFiniteGroups : (G : Type u₂) → [inst : Group G] → [inst_1 : Finite G] → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F

  F preserves quotients by finite groups (G5).

• reflectsIsos : CategoryTheory.ReflectsIsomorphisms F

  F reflects isomorphisms (G6).

class CategoryTheory.PreGaloisCategory.IsConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (X : C) : Prop

An object of a category C is connected if it is not initial and has no non-trivial subobjects. Lenstra, 3.12.

• notInitial : CategoryTheory.Limits.IsInitial X → False

  X is not an initial object.

• noTrivialComponent : ∀ (Y : C) (i : Y ⟶ X) [inst : CategoryTheory.Mono i], (CategoryTheory.Limits.IsInitial Y → False) → CategoryTheory.IsIso i

  X has no non-trivial subobjects.

class CategoryTheory.PreGaloisCategory.PreservesIsConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {D : Type v₁} [CategoryTheory.Category.{v₂, v₁} D] (F : CategoryTheory.Functor C D) : Prop

A functor is said to preserve connectedness if whenever X : C is connected, also F.obj X is connected.

• preserves : ∀ {X : C} [inst : CategoryTheory.PreGaloisCategory.IsConnected X], CategoryTheory.PreGaloisCategory.IsConnected (F.toPrefunctor.obj X)

  F.obj X is connected if X is connected.

instance CategoryTheory.PreGaloisCategory.instHasFiniteLimits {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasFiniteLimits C

Equations

• (_ : CategoryTheory.Limits.HasFiniteLimits C) = (_ : CategoryTheory.Limits.HasFiniteLimits C)

instance CategoryTheory.PreGaloisCategory.instHasBinaryProducts {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasBinaryProducts C

Equations

• (_ : CategoryTheory.Limits.HasBinaryProducts C) = (_ : CategoryTheory.Limits.HasBinaryProducts C)

instance CategoryTheory.PreGaloisCategory.instHasEqualizers {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasEqualizers C

Equations

• (_ : CategoryTheory.Limits.HasEqualizers C) = (_ : CategoryTheory.Limits.HasEqualizers C)

noncomputable instance CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatInstCategoryFintypeCatDiscretePEmptyDiscreteCategory {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.ReflectsLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatInstCategoryFintypeCatDiscretePEmptyDiscreteCategory {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCatInstCategoryFintypeCat {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.PreservesFiniteLimits F

Equations

• CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCatInstCategoryFintypeCat = CategoryTheory.Limits.preservesFiniteLimitsOfPreservesTerminalAndPullbacks F

instance CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCatInstCategoryFintypeCat {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Functor.ReflectsMonomorphisms F

Fiber functors reflect monomorphisms.

Equations

• (_ : CategoryTheory.Functor.ReflectsMonomorphisms F) = (_ : CategoryTheory.Functor.ReflectsMonomorphisms F)

instance CategoryTheory.PreGaloisCategory.FiberFunctor.instFaithfulFintypeCatInstCategoryFintypeCat {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Faithful F

Fiber functors are faithful.

Equations

• (_ : CategoryTheory.Faithful F) = (_ : CategoryTheory.Faithful F)

theorem CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) : Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↑(F.toPrefunctor.obj X)

An object is initial if and only if its fiber is empty.

theorem CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) : CategoryTheory.Limits.IsInitial X → False ↔ Nonempty ↑(F.toPrefunctor.obj X)

An object is not initial if and only if its fiber is nonempty.

theorem CategoryTheory.PreGaloisCategory.not_initial_of_inhabited {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} (x : ↑(F.toPrefunctor.obj X)) (h : CategoryTheory.Limits.IsInitial X) : False

An object whose fiber is inhabited is not initial.

instance CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : Nonempty ↑(F.toPrefunctor.obj X)

The fiber of a connected object is nonempty.

Equations

• (_ : Nonempty ↑(F.toPrefunctor.obj X)) = (_ : Nonempty ↑(F.toPrefunctor.obj X))

theorem CategoryTheory.PreGaloisCategory.evaluationInjective_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) (X : C) [CategoryTheory.PreGaloisCategory.IsConnected A] (a : ↑(F.toPrefunctor.obj A)) : Function.Injective fun (f : A ⟶ X) => F.toPrefunctor.map f a

The evaluation map is injective for connected objects.

theorem CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] (a : ↑(F.toPrefunctor.obj A)) : Function.Injective fun (f : CategoryTheory.Aut A) => F.toPrefunctor.map f.hom a

The evaluation map on automorphisms is injective for connected objects.

class CategoryTheory.GaloisCategory (C : Type u₁) [CategoryTheory.Category.{u₂, u₁} C] extends CategoryTheory.PreGaloisCategory : Prop

A PreGaloisCategory is a GaloisCategory if it admits a fiber functor.

• hasTerminal : CategoryTheory.Limits.HasTerminal C
• hasPullbacks : CategoryTheory.Limits.HasPullbacks C
• hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C
• hasQuotientsByFiniteGroups : ∀ (G : Type u₂) [inst : Group G] [inst_1 : Finite G], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
• monoInducesIsoOnDirectSummand : ∀ {X Y : C} (i : X ⟶ Y) [inst : CategoryTheory.Mono i], ∃ (Z : C) (u : Z ⟶ Y), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
• hasFiberFunctor : ∃ (F : CategoryTheory.Functor C FintypeCat), Nonempty (CategoryTheory.PreGaloisCategory.FiberFunctor F)

instance CategoryTheory.PreGaloisCategory.instFiniteHomToQuiverToCategoryStruct {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (A : C) (X : C) [CategoryTheory.PreGaloisCategory.IsConnected A] : Finite (A ⟶ X)

In a GaloisCategory the set of morphisms out of a connected object is finite.

Equations

• (_ : Finite (A ⟶ X)) = (_ : Finite (A ⟶ X))

instance CategoryTheory.PreGaloisCategory.instFiniteAut {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] : Finite (CategoryTheory.Aut A)

In a GaloisCategory the set of automorphism of a connected object is finite.

Equations

• (_ : Finite (CategoryTheory.Aut A)) = (_ : Finite (CategoryTheory.Aut A))