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

• [lenstraGSchemes]: 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).

theorem CategoryTheory.PreGaloisCategory.hasTerminal {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasTerminal C

C has a terminal object (G1).

theorem CategoryTheory.PreGaloisCategory.hasPullbacks {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasPullbacks C

C has pullbacks (G1).

theorem CategoryTheory.PreGaloisCategory.hasFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasFiniteCoproducts C

C has finite coproducts (G2).

theorem CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C] (G : Type u₂) [Group G] [Finite G] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C

C has quotients by finite groups (G2).

theorem CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C] {X : C} {Y : C} (i : X ⟶ Y) [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 : F.PreservesEpimorphisms

  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 : F.ReflectsIsomorphisms

  F reflects isomorphisms (G6).

theorem CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F] : F.PreservesEpimorphisms

F preserves epimorphisms (G5).

theorem CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F] : F.ReflectsIsomorphisms

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.

theorem CategoryTheory.PreGaloisCategory.IsConnected.notInitial {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {X : C} [self : CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.Limits.IsInitial X → False

X is not an initial object.

theorem CategoryTheory.PreGaloisCategory.IsConnected.noTrivialComponent {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {X : C} [self : CategoryTheory.PreGaloisCategory.IsConnected X] (Y : C) (i : Y ⟶ X) [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.obj X)

  F.obj X is connected if X is connected.

theorem CategoryTheory.PreGaloisCategory.PreservesIsConnected.preserves {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {D : Type v₁} [CategoryTheory.Category.{v₂, v₁} D] {F : CategoryTheory.Functor C D} [self : CategoryTheory.PreGaloisCategory.PreservesIsConnected F] {X : C} [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.PreGaloisCategory.IsConnected (F.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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty {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

• CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty = CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms

noncomputable instance CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty {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

• CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty = CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms

noncomputable instance CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCat {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.instPreservesFiniteLimitsFintypeCat = CategoryTheory.Limits.preservesFiniteLimitsOfPreservesTerminalAndPullbacks F

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

Fiber functors reflect monomorphisms.

Equations

• ⋯ = ⋯

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

Fiber functors are faithful.

Equations

• ⋯ = ⋯

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.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.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.obj X)) (h : CategoryTheory.Limits.IsInitial X) : False

An object whose fiber is inhabited is not initial.

theorem CategoryTheory.PreGaloisCategory.has_non_trivial_subobject_of_not_isConnected_of_not_initial {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (X : C) (hc : ¬CategoryTheory.PreGaloisCategory.IsConnected X) (hi : CategoryTheory.Limits.IsInitial X → False) : ∃ (Y : C) (v : Y ⟶ X), (CategoryTheory.Limits.IsInitial Y → False) ∧ CategoryTheory.Mono v ∧ ¬CategoryTheory.IsIso v

An object that is neither initial or connected has a non-trivial subobject.

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.obj X)

The fiber of a connected object is nonempty.

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : ↑(F.obj (CategoryTheory.Limits.equalizer f g)) ≃ { x : ↑(F.obj X) // F.map f x = F.map g x }

The fiber of the equalizer of f g : X ⟶ Y is equivalent to the set of agreement of f and g.

Equations

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

noncomputable def CategoryTheory.PreGaloisCategory.fiberPullbackEquiv {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {A : C} {B : C} (f : A ⟶ X) (g : B ⟶ X) : ↑(F.obj (CategoryTheory.Limits.pullback f g)) ≃ { p : ↑(F.obj A) × ↑(F.obj B) // F.map f p.1 = F.map g p.2 }

The fiber of the pullback is the fiber product of the fibers.

Equations

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

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.obj A)) : Function.Injective fun (f : A ⟶ X) => F.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.obj A)) : Function.Injective fun (f : CategoryTheory.Aut A) => F.map f.hom a

The evaluation map on automorphisms is injective for connected objects.

theorem CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eqCardFiber {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (h : Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)) : CategoryTheory.IsIso f

A mono between objects with equally sized fibers is an iso.

theorem CategoryTheory.PreGaloisCategory.ltCardFiber_of_mono_of_notIso {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (h : ¬CategoryTheory.IsIso f) : Nat.card ↑(F.obj X) < Nat.card ↑(F.obj Y)

Along a mono that is not an iso, the cardinality of the fiber strictly increases.

theorem CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) (h : CategoryTheory.Limits.IsInitial X → False) : Nat.card ↑(F.obj X) ≠ 0

The cardinality of the fiber of a not-initial object is non-zero.

theorem CategoryTheory.PreGaloisCategory.cardFiber_coprod_eq_sum {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) (Y : C) : Nat.card ↑(F.obj (X ⨿ Y)) = Nat.card ↑(F.obj X) + Nat.card ↑(F.obj Y)

The cardinality of the fiber of a coproduct is the sum of the cardinalities of the fibers.

theorem CategoryTheory.PreGaloisCategory.cardFiber_eq_of_iso {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X : C} {Y : C} (i : X ≅ Y) : Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)

The cardinality of the fiber is preserved under isomorphisms.

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)

theorem CategoryTheory.GaloisCategory.hasFiberFunctor {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.GaloisCategory C] : ∃ (F : CategoryTheory.Functor C FintypeCat), Nonempty (CategoryTheory.PreGaloisCategory.FiberFunctor F)

noncomputable def CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor (C : Type u₁) [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] : CategoryTheory.Functor C FintypeCat

Arbitrarily choose a fiber functor for a Galois category using choice.

Equations

• CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor C = Classical.choose ⋯

noncomputable instance CategoryTheory.PreGaloisCategory.instFiberFunctorGetFiberFunctor (C : Type u₁) [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] : CategoryTheory.PreGaloisCategory.FiberFunctor (CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor C)

The arbitrarily chosen fiber functor GaloisCategory.getFiberFunctor is a fiber functor.

Equations

• CategoryTheory.PreGaloisCategory.instFiberFunctorGetFiberFunctor C = Classical.choice ⋯

instance CategoryTheory.PreGaloisCategory.instFiniteHomOfIsConnected {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

• ⋯ = ⋯

instance CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected {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

• ⋯ = ⋯

instance CategoryTheory.PreGaloisCategory.instMonoCoprod {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] : CategoryTheory.Limits.MonoCoprod C

Coproduct inclusions are monic in Galois categories.

Equations

• ⋯ = ⋯