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

• ⋯ = ⋯

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

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

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

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

Equations

• CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a = Equiv.ofBijective (fun (f : CategoryTheory.Aut A) => F.map f.hom a) ⋯

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.PreGaloisCategory.autMap f σ = Exists.choose ⋯

@[simp]

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

@[simp]

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

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

autMap is uniquely characterized by making the canonical diagram commute.

@[simp]

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

@[simp]

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

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

autMap is surjective, if the source is also Galois.

@[simp]

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

@[simp]

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

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

MonoidHom version of autMap.

Equations

• CategoryTheory.PreGaloisCategory.autMapHom f = MonoidHom.mk' (CategoryTheory.PreGaloisCategory.autMap f) ⋯