Functors out of a Grothendieck construction

For F : C ⥤ Cat, a functor Grothendieck F ⥤ E amounts to a fiber functor over each object of C together with a transition transformation over each morphism of C, subject to identity and composition coherence; a natural transformation of two such functors amounts to a transformation of fiber functors coherent with the transitions. This module bundles each family of data as a structure, gives the data a category structure whose morphisms are the bundled transformations, and compares that category with the functor category. The contravariant construction is treated alongside the covariant one.

Main definitions

CategoryTheory.Grothendieck.FunctorFromData and Grothendieck.functorFromData

CategoryTheory.Grothendieck.NatTransFromData and Grothendieck.natTransFrom

CategoryTheory.Functor.leftOpEquiv

CategoryTheory.CoGrothendieck.FunctorFromData, with the constructor FunctorFromData.mk, its accessors, and the morphism interface natTransFromMk/natTransFromFibNat

Main statements

Grothendieck.natTransFromEquiv: the transformation data determines the transformation, bijectively

Grothendieck.functorFromDataEquivCat and CoGrothendieck.functorFromDataEquivCat: the category of data is equivalent to the functor category

Implementation notes

The correspondence is an equivalence rather than an isomorphism: extracting the fiber functors from functorFromData data restricts along Grothendieck.ι, which recovers data.fib c up to the canonical isomorphism ιCompFunctorFromData rather than on the nose.

functorFromData repeats the construction of mathlib's Grothendieck.functorFrom rather than calling it. The coherence arguments of mathlib's version carry eqToHom proof terms private to that module, and the module system does not export them, so a definition applying it fails in the kernel with an unknown private constant.

The contravariant data type is the covariant one for G ⋙ Cat.opFunctor, taken in the opposite category so that its transformations run in the direction of the codomain, with a constructor and accessors phrased in terms of morphisms of C. Functor.leftOpEquiv supplies the transport of the equivalence; the conversions between the two presentations of the coherence conditions are the image and preimage of the whole equation under NatTrans.op.

Cat is a semireducible def whose morphisms are a bundled Cat.Hom, so keyed simp/rw matching fails against generic lemmas on terms routed through F.obj/F.map even where the two sides are definitionally equal; see Geb/Mathlib/CategoryTheory/Grothendieck/Basic.lean § Implementation notes. The erw steps below isolate exactly those crossings.

References

The description of functors out of a Grothendieck construction by fiberwise data is standard; see [Vistoli2008] and [JohnsonYau2021].

Tags

Grothendieck construction, contravariant, functor category, universal property

Functors out of a covariant Grothendieck construction

The fiber-functor component of the data determining a functor out of Grothendieck F: a functor on the fiber over each object of C.

The transition component of the data determining a functor out of Grothendieck F: for each f : c ⟶ c', a transformation from the fiber functor over c to the fiber functor over c' precomposed with the pushforward.

The identity coherence condition on the transition component.

The composition coherence condition on the transition component.

The data determining a functor Grothendieck F ⥤ E: a fiber functor over each object of C, a transition transformation over each morphism of C, and the two coherence conditions.

The fiber functor over each object of C.

The transition transformation over each morphism of C.

Identity coherence.

Composition coherence.

The functor Grothendieck F ⥤ E determined by a FunctorFromData.

The FunctorFromData determined by a functor Grothendieck F ⥤ E: restrict along the fiber inclusions, with the transitions induced by ιNatTrans.