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

• [lenstraGSchemes]: 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.

theorem CategoryTheory.PreGaloisCategory.has_decomp_connected_components {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (X : C) : ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : Limits.IsColimit (Limits.Cofan.mk X g)), (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

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

theorem CategoryTheory.PreGaloisCategory.has_decomp_connected_components' {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (X : C) : ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : ∐ f ≅ X), ∀ (i : ι), IsConnected (f i)

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

theorem CategoryTheory.PreGaloisCategory.fiber_in_connected_component {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (X : C) (x : (F.obj X).carrier) : ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).carrier), (ConcreteCategory.hom (F.map i)) y = x ∧ IsConnected Y ∧ Mono i

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

theorem CategoryTheory.PreGaloisCategory.connected_component_unique {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] {X A B : C} [IsConnected A] [IsConnected B] (a : (F.obj A).carrier) (b : (F.obj B).carrier) (i : A ⟶ X) (j : B ⟶ X) (h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b) [Mono i] [Mono j] : ∃ (f : A ≅ B), (ConcreteCategory.hom (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]

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

The fiber of any object in a Galois category is represented by a Galois object.

theorem CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (X : C) (x : (F.obj X).carrier) : ∃ (A : C) (f : A ⟶ X) (a : (F.obj A).carrier), IsGalois A ∧ (ConcreteCategory.hom (F.map f)) a = x

Any element in the fiber of an object X is the evaluation of a morphism from a Galois object.

theorem CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (X : C) (h : Nonempty (F.obj X).carrier) : ∃ (A : C) (x : A ⟶ X), IsGalois A

Any object with non-empty fiber admits a hom from a Galois object.

theorem CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_connected {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] (X : C) [IsConnected X] : ∃ (A : C) (x : A ⟶ X), IsGalois A

Any connected object admits a hom from a Galois object.

theorem CategoryTheory.PreGaloisCategory.natTrans_ext_of_isGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (F : Functor C FintypeCat) [FiberFunctor F] {G : Functor C FintypeCat} {t s : F ⟶ G} (h : ∀ (X : C) [IsGalois X], t.app X = s.app X) : t = s

To check equality of natural transformations F ⟶ G, it suffices to check it on Galois objects.