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.
Equations
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeDep F X = { coe := X.obj }
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.
The category of pointed Galois objects.
Equations
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeHomHomObj F = { coe := fun (f : A.Hom B) => f.val }
The canonical functor from pointed Galois objects to C.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
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.
The limit of autGaloisSystem.
The canonical projection from AutGalois F to the C-automorphism group of each
pointed Galois object.
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.
Functorial isomorphism Aut A ≅ F.obj A for Galois objects A.
Equations
- One or more equations did not get rendered due to their size.
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.
The monoid isomorphism between endomorphisms of F and the (multiplicative opposite of the)
limit of automorphism groups of all Galois objects.
Equations
- CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F = { toEquiv := (CategoryTheory.PreGaloisCategory.endEquivAutGalois F).trans MulOpposite.opEquiv, map_mul' := ⋯ }
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.
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.