Documentation

Mathlib.CategoryTheory.Galois.Basic

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

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

Instances

theorem CategoryTheory.PreGaloisCategory.hasTerminal {C : Type u₁} :

∀ {inst : 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₁} :

∀ {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C], CategoryTheory.Limits.HasPullbacks C

C has pullbacks (G1).

theorem CategoryTheory.PreGaloisCategory.hasFiniteCoproducts {C : Type u₁} :

∀ {inst : 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₁} :

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

C has quotients by finite groups (G2).

theorem CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C] {X Y : C} (i : X ⟶ Y) [inst_1 : 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).

Instances

theorem CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : 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₁} :

∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : 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) :

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.

Instances

theorem CategoryTheory.PreGaloisCategory.IsConnected.notInitial {C : Type u₁} :

∀ {inst : 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₁} :

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

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.

Instances

theorem CategoryTheory.PreGaloisCategory.PreservesIsConnected.preserves {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {D : Type v₁} {inst_1 : CategoryTheory.Category.{v₂, v₁} D} {F : CategoryTheory.Functor C D} [self : CategoryTheory.PreGaloisCategory.PreservesIsConnected F] {X : C} [inst_2 : 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

⋯ = ⋯

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

CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) 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

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

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F

Fiber functors preserve quotients by finite groups in arbitrary universes.

Equations

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

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

⋯ = ⋯

noncomputable def CategoryTheory.PreGaloisCategory.FiberFunctor.compRight {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (E : CategoryTheory.Functor FintypeCat FintypeCat) [E.IsEquivalence] :

CategoryTheory.PreGaloisCategory.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.

Equations

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

Instances For

instance CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatαFintypeObj {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) :

MulAction (CategoryTheory.Aut F) ↑(F.obj X)

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

Equations

CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatαFintypeObj F X = MulAction.mk ⋯ ⋯

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

σ • x = σ.hom.app X x

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

σ • F.map f x = F.map f (σ • x)

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.

theorem CategoryTheory.PreGaloisCategory.card_fiber_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.

theorem CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} (x : ↑(F.obj X)) (h : CategoryTheory.Limits.IsInitial X) :

An object whose fiber is inhabited is not initial.

instance CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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.

Instances For

@[simp]

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

F.map (CategoryTheory.Limits.equalizer.ι f g) ((CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x

noncomputable def CategoryTheory.PreGaloisCategory.fiberPullbackEquiv {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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.

Instances For

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {A : C} {B : C} {f : A ⟶ X} {g : B ⟶ X} (a : ↑(F.obj A)) (b : ↑(F.obj B)) (h : F.map f a = F.map g b) :

F.map (CategoryTheory.Limits.pullback.fst f g) ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {A : C} {B : C} {f : A ⟶ X} {g : B ⟶ X} (a : ↑(F.obj A)) (b : ↑(F.obj B)) (h : F.map f a = F.map g b) :

F.map (CategoryTheory.Limits.pullback.snd f g) ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b

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

↑(F.obj (X ⨯ Y)) ≃ ↑(F.obj X) × ↑(F.obj Y)

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

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {Y : C} (x : ↑(F.obj X)) (y : ↑(F.obj Y)) :

F.map CategoryTheory.Limits.prod.fst ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = x

@[simp]

theorem CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {Y : C} (x : ↑(F.obj X)) (y : ↑(F.obj Y)) :

F.map CategoryTheory.Limits.prod.snd ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = y

theorem CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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.epi_of_nonempty_of_isConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {A : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [h : Nonempty ↑(F.obj X)] (f : X ⟶ A) :

CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C} {A : C} [Nonempty ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.IsConnected A] (f : X ⟶ A) :

Function.Surjective (F.map f)

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

Nonempty ↑(F.obj (∏ᶜ X))

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

Equations

⋯ = ⋯

theorem CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eq_card_fiber {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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.lt_card_fiber_of_mono_of_notIso {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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.card_fiber_coprod_eq_sum {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [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.card_hom_le_card_fiber_of_connected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) (X : C) [CategoryTheory.PreGaloisCategory.IsConnected A] :

Nat.card (A ⟶ X) ≤ Nat.card ↑(F.obj X)

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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] :

Nat.card (CategoryTheory.Aut A) ≤ Nat.card ↑(F.obj A)

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

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)

Instances

theorem CategoryTheory.GaloisCategory.hasFiberFunctor {C : Type u₁} :

∀ {inst : 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 ⋯

Instances For

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

⋯ = ⋯