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.

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

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

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

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

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

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

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

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.

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

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

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₁} [Category.{u₂, u₁} C] [GaloisCategory C] (X : C) [IsGalois X] : Limits.IsTerminal (Limits.colimit (SingleObj.functor (Aut.toEnd X)))

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

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

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

theorem CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (X : C) [IsGalois X] (x : (F.obj X).carrier) : (MulAction.stabilizer (Aut F) x).Normal

theorem CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (A : C) [IsGalois A] (a : (F.obj A).carrier) : Function.Surjective fun (f : Aut A) => F.map f.hom a

theorem CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (A : C) [IsGalois A] (a : (F.obj A).carrier) : Function.Bijective fun (f : Aut A) => F.map f.hom a

noncomputable def CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (A : C) [IsGalois A] (a : (F.obj A).carrier) : Aut A ≃ (F.obj A).carrier

For Galois A and a point a of the fiber of A, the evaluation at A as an equivalence.

@[simp]

theorem CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (A : C) [IsGalois A] (a : (F.obj A).carrier) (φ : Aut A) : (evaluationEquivOfIsGalois F A a) φ = F.map φ.hom a

@[simp]

theorem CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (A : C) [IsGalois A] (a b : (F.obj A).carrier) : F.map ((evaluationEquivOfIsGalois F A a).symm b).hom a = b

theorem CategoryTheory.PreGaloisCategory.exists_autMap {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} (f : A ⟶ B) [IsConnected A] [IsGalois B] (σ : Aut A) : ∃! τ : Aut B, CategoryStruct.comp f τ.hom = CategoryStruct.comp σ.hom f

For a morphism from a connected object A to a Galois object B and an automorphism of A, there exists a unique automorphism of B making the canonical diagram commute.

noncomputable def CategoryTheory.PreGaloisCategory.autMap {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) : Aut B

A morphism from a connected object to a Galois object induces a map on automorphism groups. This is a group homomorphism (see autMapHom).

@[simp]

theorem CategoryTheory.PreGaloisCategory.comp_autMap {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) : CategoryStruct.comp f (autMap f σ).hom = CategoryStruct.comp σ.hom f

@[simp]

theorem CategoryTheory.PreGaloisCategory.comp_autMap_apply {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) (a : (F.obj A).carrier) : F.map (autMap f σ).hom (F.map f a) = F.map f (F.map σ.hom a)

theorem CategoryTheory.PreGaloisCategory.autMap_unique {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) (τ : Aut B) (h : CategoryStruct.comp f τ.hom = CategoryStruct.comp σ.hom f) : autMap f σ = τ

autMap is uniquely characterized by making the canonical diagram commute.

@[simp]

theorem CategoryTheory.PreGaloisCategory.autMap_id {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A : C} [IsGalois A] : autMap (CategoryStruct.id A) = id

@[simp]

theorem CategoryTheory.PreGaloisCategory.autMap_comp {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {X Y Z : C} [IsConnected X] [IsGalois Y] [IsGalois Z] (f : X ⟶ Y) (g : Y ⟶ Z) : autMap (CategoryStruct.comp f g) = autMap g ∘ autMap f

theorem CategoryTheory.PreGaloisCategory.autMap_surjective_of_isGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsGalois A] [IsGalois B] (f : A ⟶ B) : Function.Surjective (autMap f)

autMap is surjective, if the source is also Galois.

@[simp]

theorem CategoryTheory.PreGaloisCategory.autMap_apply_mul {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ τ : Aut A) : autMap f (σ * τ) = autMap f σ * autMap f τ

noncomputable def CategoryTheory.PreGaloisCategory.autMapHom {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) : Aut A →* Aut B

MonoidHom version of autMap.

@[simp]

theorem CategoryTheory.PreGaloisCategory.autMapHom_apply {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) : (autMapHom f) σ = autMap f σ