Decomposition of objects into connected components and applications #

We show that in a Galois category every object is the (finite) coproduct of connected subobjects. This has many useful corollaries, in particular that the fiber of every object is represented by a Galois object.

Main results #

has_decomp_connected_components: Every object is the sum of its (finitely many) connected components.
fiber_in_connected_component: An element of the fiber of X lies in the fiber of some connected component.
connected_component_unique: Up to isomorphism, for each element x in the fiber of X there is only one connected component whose fiber contains x.
exists_galois_representative: The fiber of X is represented by some Galois object A: Evaluation at some a in the fiber of A induces a bijection A ⟶ X to F.obj X.

References #

[Len]: H. W. Lenstra. Galois theory for schemes.

Decomposition in connected components #

To show that an object X of a Galois category admits a decomposition into connected objects, we proceed by induction on the cardinality of the fiber under an arbitrary fiber functor.

If X is connected, there is nothing to show. If not, we can write X as the sum of two non-trivial subobjects which have strictly smaller fiber and conclude by the induction hypothesis.

source

theorem CategoryTheory.PreGaloisCategory.has_decomp_connected_components {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C) :

∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X g)), (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι

In a Galois category, every object is the sum of connected objects.

source

theorem CategoryTheory.PreGaloisCategory.has_decomp_connected_components' {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C) :

∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : ∐ f ≅ X), ∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)

In a Galois category, every object is the sum of connected objects.

source

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

∃ (Y : C) (i : Y ⟶ X) (y : ↑(F.obj Y)), F.map i y = x ∧ CategoryTheory.PreGaloisCategory.IsConnected Y ∧ CategoryTheory.Mono i

Every element in the fiber of X lies in some connected component of X.

source

theorem CategoryTheory.PreGaloisCategory.connected_component_unique {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsConnected B] (a : ↑(F.obj A)) (b : ↑(F.obj B)) (i : A ⟶ X) (j : B ⟶ X) (h : F.map i a = F.map j b) [CategoryTheory.Mono i] [CategoryTheory.Mono j] :

∃ (f : A ≅ B), F.map f.hom a = b

Up to isomorphism an element of the fiber of X only lies in one connected component.

Galois representative of fiber #

If X is any object, then its fiber is represented by some Galois object: There exists a Galois object A and an element a in the fiber of A such that the evaluation at a from A ⟶ X to F.obj X is bijective.

To show this we consider the product ∏ᶜ (fun _ : F.obj X ↦ X) and let A be the connected component whose fiber contains the element a in the fiber of the self product that has at each index x : F.obj X the element x.

This A is Galois and evaluation at a is bijective.

Reference: [lenstraGSchemes, 3.14]

source