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 functorFiberFunctor: a fiber functor from aPreGaloisCategorytoFintypeCatGaloisCategory: aPreGaloisCategorythat admits aFiberFunctorIsConnected: 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 #
- [Len]: 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.
Definition of a (Pre)Galois category. Lenstra, Def 3.1, (G1)-(G3)
- hasTerminal : Limits.HasTerminal C
Chas a terminal object (G1). - hasPullbacks : Limits.HasPullbacks C
Chas pullbacks (G1). - hasFiniteCoproducts : Limits.HasFiniteCoproducts C
Chas finite coproducts (G2). - hasQuotientsByFiniteGroups (G : Type u₂) [Group G] [Finite G] : Limits.HasColimitsOfShape (SingleObj G) C
Chas 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
Cinduces an isomorphism on a direct summand (G3).
Instances
Definition of a fiber functor from a Galois category. Lenstra, Def 3.1, (G4)-(G6)
- preservesTerminalObjects : Limits.PreservesLimitsOfShape (Discrete PEmpty.{1}) F
Fpreserves terminal objects (G4). - preservesPullbacks : Limits.PreservesLimitsOfShape Limits.WalkingCospan F
Fpreserves pullbacks (G4). - preservesFiniteCoproducts : Limits.PreservesFiniteCoproducts F
Fpreserves finite coproducts (G5). - preservesEpis : F.PreservesEpimorphisms
Fpreserves epimorphisms (G5). - preservesQuotientsByFiniteGroups (G : Type u₂) [Group G] [Finite G] : Limits.PreservesColimitsOfShape (SingleObj G) F
Fpreserves quotients by finite groups (G5). - reflectsIsos : F.ReflectsIsomorphisms
Freflects isomorphisms (G6).
Instances
An object of a category C is connected if it is not initial
and has no non-trivial subobjects. Lenstra, 3.12.
- notInitial : Limits.IsInitial X → False
Xis not an initial object. Xhas no non-trivial subobjects.
Instances
A functor is said to preserve connectedness if whenever X : C is connected,
also F.obj X is connected.
F.obj Xis connected ifXis connected.
Instances
Fiber functors preserve quotients by finite groups in arbitrary universes.
Fiber functors reflect monomorphisms.
Fiber functors are faithful.
If F is a fiber functor and E is an equivalence between categories of finite types,
then F ⋙ E is again a fiber functor.
The canonical action of Aut F on the fiber of each object.
An object that is neither initial or connected has a non-trivial subobject.
The cardinality of the fiber is preserved under isomorphisms.
An object is initial if and only if its fiber is empty.
An object is not initial if and only if its fiber is nonempty.
An object whose fiber is inhabited is not initial.
The fiber of a connected object is nonempty.
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.
Instances For
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.
Instances For
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.
Instances For
The evaluation map is injective for connected objects.
The evaluation map on automorphisms is injective for connected objects.
A morphism from an object X with non-empty fiber to a connected object A is an
epimorphism.
An epimorphism induces a surjective map on fibers.
If X : ι → C is a finite family of objects with non-empty fiber, then
also ∏ᶜ X has non-empty fiber.
A mono between objects with equally sized fibers is an iso.
Along a mono that is not an iso, the cardinality of the fiber strictly increases.
The cardinality of the fiber of a not-initial object is non-zero.
The cardinality of the fiber of a coproduct is the sum of the cardinalities of the fibers.
The cardinality of morphisms A ⟶ X is smaller than the cardinality of
the fiber of the target if the source is connected.
If A is connected, the cardinality of Aut A is smaller than the cardinality of the
fiber of A.
A PreGaloisCategory is a GaloisCategory if it admits a fiber functor.
- 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)
Instances
Arbitrarily choose a fiber functor for a Galois category using choice.
Instances For
The arbitrarily chosen fiber functor GaloisCategory.getFiberFunctor is a fiber functor.
In a GaloisCategory the set of morphisms out of a connected object is finite.
In a GaloisCategory the set of automorphism of a connected object is finite.
Coproduct inclusions are monic in Galois categories.