Galois objects in Galois categories

We define when a connected object of a Galois category C is Galois in a fiber functor independent way and show equivalent characterisations.

Main definitions

• IsGalois : Connected object X of C such that X / Aut X is terminal.

Main results

• galois_iff_pretransitive : A connected object X is Galois if and only if Aut X acts transitively on F.obj X for a fiber functor F.

noncomputable instance CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite {G : Type v} [Group G] [Finite G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat.incl

Equations

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

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

A connected object X of C is Galois if the quotient X / Aut X is terminal.

• notInitial : CategoryTheory.Limits.IsInitial X → False
• noTrivialComponent : ∀ (Y : C) (i : Y ⟶ X) [inst : CategoryTheory.Mono i], (CategoryTheory.Limits.IsInitial Y → False) → CategoryTheory.IsIso i
• quotientByAutTerminal : Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))

theorem CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {X : C} [self : CategoryTheory.PreGaloisCategory.IsGalois X] : Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))

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

The natural action of Aut X on F.obj X.

Equations

• CategoryTheory.PreGaloisCategory.autMulFiber F X = MulAction.mk ⋯ ⋯

noncomputable def CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))) ≃ Unique (MulAction.orbitRel.Quotient (CategoryTheory.Aut X) ↑(F.obj X))

For a connected object X of C, the quotient X / Aut X is terminal if and only if the quotient F.obj X / Aut X has exactly one element.

Equations

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

theorem CategoryTheory.PreGaloisCategory.isGalois_iff_aux {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.PreGaloisCategory.IsGalois X ↔ Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))

theorem CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.PreGaloisCategory.IsGalois X ↔ MulAction.IsPretransitive (CategoryTheory.Aut X) ↑(F.obj X)

Given a fiber functor F and a connected object X of C. Then X is Galois if and only if the natural action of Aut X on F.obj X is transitive.

noncomputable def CategoryTheory.PreGaloisCategory.isTerminalQuotientOfIsGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X)))

If X is Galois, the quotient X / Aut X is terminal.

Equations

• CategoryTheory.PreGaloisCategory.isTerminalQuotientOfIsGalois X = ⋯.some

instance CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : MulAction.IsPretransitive (CategoryTheory.Aut X) ↑(F.obj X)

If X is Galois, then the action of Aut X on F.obj X is transitive for every fiber functor F.

Equations

• ⋯ = ⋯