Documentation

Mathlib.CategoryTheory.Galois.Decomposition

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 #

References #

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.

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

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

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

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]

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

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