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

Any fiber functor F induces an equivalence with the category of finite, discrete Aut F-types. This is proven in Mathlib/CategoryTheory/Galois/Equivalence.lean.

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₁) [Category.{u₂, u₁} C] : Prop

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

• hasTerminal : Limits.HasTerminal C

  C has a terminal object (G1).

• hasPullbacks : Limits.HasPullbacks C

  C has pullbacks (G1).

• hasFiniteCoproducts : Limits.HasFiniteCoproducts C

  C has finite coproducts (G2).

• hasQuotientsByFiniteGroups (G : Type u₂) [Group G] [Finite G] : Limits.HasColimitsOfShape (SingleObj G) C

  C has quotients by finite groups (G2).

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

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

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

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

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

  F preserves terminal objects (G4).

• preservesPullbacks : Limits.PreservesLimitsOfShape Limits.WalkingCospan F

  F preserves pullbacks (G4).

• preservesFiniteCoproducts : Limits.PreservesFiniteCoproducts F

  F preserves finite coproducts (G5).

• preservesEpis : F.PreservesEpimorphisms

  F preserves epimorphisms (G5).

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

  F preserves quotients by finite groups (G5).

• reflectsIsos : F.ReflectsIsomorphisms

  F reflects isomorphisms (G6).

class CategoryTheory.PreGaloisCategory.IsConnected {C : Type u₁} [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 : ∀ (a : Limits.IsInitial X), False

  X is not an initial object.

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

  X has no non-trivial subobjects.

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

  F.obj X is connected if X is connected.

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

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

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

instance CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite {C : Type u₁} [Category.{u₂, u₁} C] [PreGaloisCategory C] {G : Type u_1} [Group G] [Finite G] : Limits.HasColimitsOfShape (SingleObj G) C

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

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

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

instance CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [PreGaloisCategory C] [FiberFunctor F] {G : Type u_1} [Group G] [Finite G] : Limits.PreservesColimitsOfShape (SingleObj G) F

Fiber functors preserve quotients by finite groups in arbitrary universes.

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

Fiber functors reflect monomorphisms.

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

Fiber functors are faithful.

instance CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right {C : Type u₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [PreGaloisCategory C] [FiberFunctor F] (E : Functor FintypeCat FintypeCat) [E.IsEquivalence] : FiberFunctor (F.comp E)

If F is a fiber functor and E is an equivalence between categories of finite types, then F ⋙ E is again a fiber functor.

instance CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatCarrierObj {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : MulAction (Aut F) (F.obj X).carrier

The canonical action of Aut F on the fiber of each object.

Equations

• CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatCarrierObj F X = { smul := fun (σ : CategoryTheory.Aut F) (x : (F.obj X).carrier) => σ.hom.app X x, one_smul := ⋯, mul_smul := ⋯ }

theorem CategoryTheory.PreGaloisCategory.mulAction_def {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) {X : C} (σ : Aut F) (x : (F.obj X).carrier) : σ • x = σ.hom.app X x

theorem CategoryTheory.PreGaloisCategory.mulAction_naturality {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) {X Y : C} (σ : Aut F) (f : X ⟶ Y) (x : (F.obj X).carrier) : σ • F.map f x = F.map f (σ • x)

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

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

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

The cardinality of the fiber is preserved under isomorphisms.

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

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

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

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

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

An object whose fiber is inhabited is not initial.

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

The fiber of a connected object is nonempty.

noncomputable def CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X Y : C} (f g : X ⟶ Y) : (F.obj (Limits.equalizer f g)).carrier ≃ { x : (F.obj X).carrier // 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.

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X Y : C} {f g : X ⟶ Y} (x : (F.obj X).carrier) (h : F.map f x = F.map g x) : F.map (Limits.equalizer.ι f g) ((fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x

noncomputable def CategoryTheory.PreGaloisCategory.fiberPullbackEquiv {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X A B : C} (f : A ⟶ X) (g : B ⟶ X) : (F.obj (Limits.pullback f g)).carrier ≃ { p : (F.obj A).carrier × (F.obj B).carrier // 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.

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X A B : C} {f : A ⟶ X} {g : B ⟶ X} (a : (F.obj A).carrier) (b : (F.obj B).carrier) (h : F.map f a = F.map g b) : F.map (Limits.pullback.fst f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X A B : C} {f : A ⟶ X} {g : B ⟶ X} (a : (F.obj A).carrier) (b : (F.obj B).carrier) (h : F.map f a = F.map g b) : F.map (Limits.pullback.snd f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b

noncomputable def CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] (X Y : C) : (F.obj (X ⨯ Y)).carrier ≃ (F.obj X).carrier × (F.obj Y).carrier

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

Equations

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

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X Y : C} (x : (F.obj X).carrier) (y : (F.obj Y).carrier) : F.map Limits.prod.fst ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X Y : C} (x : (F.obj X).carrier) (y : (F.obj Y).carrier) : F.map Limits.prod.snd ((fiberBinaryProductEquiv F X Y).symm (x, y)) = y

theorem CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] (A X : C) [IsConnected A] (a : (F.obj A).carrier) : 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₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] (A : C) [IsConnected A] (a : (F.obj A).carrier) : Function.Injective fun (f : Aut A) => F.map f.hom a

The evaluation map on automorphisms is injective for connected objects.

theorem CategoryTheory.PreGaloisCategory.epi_of_nonempty_of_isConnected {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X A : C} [IsConnected A] [h : Nonempty (F.obj X).carrier] (f : X ⟶ A) : Epi f

A morphism from an object X with non-empty fiber to a connected object A is an epimorphism.

theorem CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X Y : C} (f : X ⟶ Y) [Epi f] : Function.Surjective (F.map f)

An epimorphism induces a surjective map on fibers.

theorem CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {X A : C} [Nonempty (F.obj X).carrier] [IsConnected A] (f : X ⟶ A) : Function.Surjective (F.map f)

instance CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] {ι : Type u_1} [Finite ι] (X : ι → C) [∀ (i : ι), Nonempty (F.obj (X i)).carrier] : Nonempty (F.obj (∏ᶜ X)).carrier

If X : ι → C is a finite family of objects with non-empty fiber, then also ∏ᶜ X has non-empty fiber.

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

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

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

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₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] (X : C) (h : ∀ (a : Limits.IsInitial X), False) : Nat.card (F.obj X).carrier ≠ 0

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

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

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

theorem CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] (A X : C) [IsConnected A] : Nat.card (A ⟶ X) ≤ Nat.card (F.obj X).carrier

The cardinality of morphisms A ⟶ X is smaller than the cardinality of the fiber of the target if the source is connected.

theorem CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [PreGaloisCategory C] [FiberFunctor F] (A : C) [IsConnected A] : Nat.card (Aut A) ≤ Nat.card (F.obj A).carrier

If A is connected, the cardinality of Aut A is smaller than the cardinality of the fiber of A.

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

Coproduct inclusions are monic in Galois categories.