Pro-Representability of fiber functors #
We show that any fiber functor is pro-representable, i.e. there exists a pro-object
X : I ⥤ C such that F is naturally isomorphic to the colimit of X ⋙ coyoneda.
From this we deduce the canonical isomorphism of Aut F with the limit over the automorphism
groups of all Galois objects.
Main definitions #
PointedGaloisObject: the category of pointed Galois objectsPointedGaloisObject.cocone: a cocone on(PointedGaloisObject.incl F).op ≫ coyonedawith pointF ⋙ FintypeCat.incl.autGaloisSystem: the system of automorphism groups indexed by the pointed Galois objects.
Main results #
PointedGaloisObject.isColimit: the coconePointedGaloisObject.coconeis a colimit cocone.autMulEquivAutGalois:Aut Fis canonically isomorphic to the limit over the automorphism groups of all Galois objects.FiberFunctor.isPretransitive_of_isConnected: TheAut Faction on the fiber of a connected object is transitive.
Implementation details #
The pro-representability statement and the isomorphism of Aut F with the limit over the
automorphism groups of all Galois objects naturally forces F to take values in FintypeCat.{u₂}
where u₂ is the Hom-universe of C. Since this is used to show that Aut F acts
transitively on F.obj X for connected X, we a priori only obtain this result for
the mentioned specialized universe setup. To obtain the result for F taking values in an arbitrary
FintypeCat.{w}, we postcompose with an equivalence FintypeCat.{w} ≌ FintypeCat.{u₂} and apply
the specialized result.
In the following the section Specialized is reserved for the setup where F takes values in
FintypeCat.{u₂} and the section General contains results holding for F taking values in
an arbitrary FintypeCat.{w}.
References #
- [lenstraGSchemes]: H. W. Lenstra. Galois theory for schemes.
A pointed Galois object is a Galois object with a fixed point of its fiber.
Instances For
The type of homomorphisms between two pointed Galois objects. This is a homomorphism
of the underlying objects of C that maps the distinguished points to each other.
The underlying homomorphism of
C.The distinguished point of
Ais mapped to the distinguished point ofB.
Instances For
The category of pointed Galois objects.
The canonical functor from pointed Galois objects to C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F ⋙ FintypeCat.incl as a cocone over (can F).op ⋙ coyoneda.
This is a colimit cocone (see PreGaloisCategory.isColimìt)
Equations
- One or more equations did not get rendered due to their size.
Instances For
The category of pointed Galois objects is cofiltered.
cocone F is a colimit cocone, i.e. F is pro-represented by incl F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diagram sending each pointed Galois object to its automorphism group
as an object of C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The limit of autGaloisSystem.
Equations
Instances For
The canonical projection from AutGalois F to the C-automorphism group of each
pointed Galois object.
Equations
Instances For
Equality of elements of AutGalois F can be checked on the projections on each pointed
Galois object.
autGalois.π is surjective for every pointed Galois object.
Isomorphism between Aut F and AutGalois F #
In this section we establish the isomorphism between the automorphism group of F and
the limit over the automorphism groups of all Galois objects.
We first establish the isomorphism between End F and AutGalois F, from which we deduce that
End F is a group, hence End F = Aut F. The isomorphism is built in multiple steps:
endEquivSectionsFibers : End F ≅ (incl F ⋙ F').sections: the endomorphisms ofFare isomorphic to the limit overF.obj Afor all Galois objectsA. This is obtained as the composition (slightly simplified):End F ≅ (colimit ((incl F).op ⋙ coyoneda) ⟶ F) ≅ (incl F ⋙ F).sectionsWhere the first isomorphism is induced from the pro-representability of
Fand the second one from the pro-coyoneda lemma.endEquivAutGalois : End F ≅ AutGalois F: this is the composition ofendEquivSectionsFiberswith:(incl F ⋙ F).sections ≅ (autGaloisSystem F ⋙ forget Grp).sectionswhich is induced from the level-wise equivalence
Aut A ≃ F.obj Afor a Galois objectA.
The endomorphisms of F are isomorphic to the limit over the fibers of F on all
Galois objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Functorial isomorphism Aut A ≅ F.obj A for Galois objects A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between endomorphisms of F and the limit over the automorphism groups
of all Galois objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The monoid isomorphism between endomorphisms of F and the (multiplicative opposite of the)
limit of automorphism groups of all Galois objects.
Equations
Instances For
Any endomorphism of a fiber functor is a unit.
Any endomorphism of a fiber functor is an isomorphism.
The automorphism group of F is multiplicatively isomorphic to
(the multiplicative opposite of) the limit over the automorphism groups of
the Galois objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Aut F action on the fiber of a Galois object is transitive. See
pretransitive_of_isConnected for the same result for connected objects.
The Aut F action on the fiber of a connected object is transitive.