# Functoriality and proofs

Recently, I began to study $\mathcal{D}$-modules and one of the major problems I encountered is that many natural transformations on the (derived) category of $\mathcal{D}$-modules are defined as the composition of many different morphisms. By this I mean that for any object it is defined a morphism between the image of this object via the two functors, and often it is not checked that this construction is functorial. Moreover, in many proofs these natural transformations are splitted into several natural transformations, but it is not clear to me why this can be done.

Let me give an example so to make things clearer. (Everything I will write can be found in $\mathcal{D}$-modules, Perverse Sheaves, and Representation Theory)

Let us consider $X$ a smooth algebraic variety over $\mathbb{C}$ and denote $X^{an}$ the associated complex manifold. Let $f : X \rightarrow Y$ be a morphism of smooth algebraic varieties. We define the direct image of $M^{\cdot} \in D^{b}(\mathcal{D}_X)$ as $$\int_fM^{\cdot} = Rf_{*} \left( \mathcal{D}_{Y \leftarrow X} \otimes^{L}_{\mathcal{D}_X} M^{\cdot}\right) \in D^b(\mathcal{D}_Y)$$ and we define the analytization of a $\mathcal{D}_X$ module as $$(M^{\cdot})^{an} = \mathcal{D}_{X^{an}} \otimes_{i^{-1}\mathcal{D}_X} i^{-1}M^{\cdot}$$ where $i : (X^{an}, \mathcal{O}_{X^{an}}) \rightarrow (X, \mathcal{O}_X)$ is the canonical morphism. There exists a natural morphism $\left( \int_f M^{\cdot} \right)^{an} \rightarrow \int_{f^{an}} (M^{\cdot})^{an}$ which is constructed as the composition of many maps. Hence, it is quite difficult to deal concretly with this morphism and to verify that it is functorial in $M$. Moreover, from the construction of the morphism it is not clear to me why it should hold $$\left( \int_{f \circ g} M^{\cdot} \right)^{an} \rightarrow \int_{(f \circ g)^{an}} (M^{\cdot})^{an} = \left( \int_{f \circ g} M^{\cdot} \right)^{an} \rightarrow \int_{f^{an}} \left( \int_g M^{\cdot} \right)^{an} \rightarrow \int_{f^{an}} \circ \int_{g^{an}} (M^{\cdot})^{an}.$$ Hence, my question is: the functoriality of some trasformations has to be awlays checked by hand or can it be deduced by a clever way of defining the maps? Moreover, the fact that some trasformations can be splitted into several ones comes from the construction if this is done in a particular way?

Mostly what I would like to understand is that if there is a "correct" (and what does correct mean?) construction of a theory such that it brings easily facts as the ones stated above.

• To verify a natural transformation made of many steps is functorial in $M$ (I guess you mean it satisfies the naturality square) one just has to check this for each step separately, and usually some or all of the steps are "obvious". For more general commutative diagrams like the one you have with $f$ and $g$, doing it by hand might be quadratic in the number of steps, so I agree this is not such a good idea. – Will Sawin Jun 22 '18 at 10:58
• Yes, that's what I mean by functorial. Ok, so generally it must be done by hand. As you said, sometimes this can be difficult and very long. Is there a way to avoid such problems? – Federico Barbacovi Jun 22 '18 at 11:04