Variant of Representable Functor

Stream: Is there code for X?

[Anthony Bordg]

Is there code for the following variant of a representable functor?

$$\text{Hom}_{\mathcal{D}}(F(-), d),$$

where $F$ is a functor from a category $\mathcal{C}$ to a category $\mathcal{D}$.

[Markus Himmel]

I think the usual spelling for that functor would be F.op ⋙ yoneda.obj d.

[Anthony Bordg]

Thank you, @Markus Himmel. It's really helpful :smile:
Given a morphism $f: d \rightarrow d'$ in $\mathcal{D}$, is there code for the following natural transformation?

$$Y(f^{\text{op}})_{F(-)}: \text{Hom}_{\mathcal{D}}(F(-),d) \rightarrow \text{Hom}_{\mathcal{D}}(F(-),d')$$

[Joël Riou]

Untested, but something like whiskerLeft F.op (yoneda.map f).

[Markus Himmel]

You also often see this as ((whiskeringLeft _ _ _).obj F.op).map (yoneda.map f). It's the same as what Joël wrote, but some useful theorems use this longer version. (Edit: this might actually be outdated information)

[Anthony Bordg]

Great! Thank you, Joël and Markus. Actually, the source and target of this transformation are sheaves, so it remains for me to understand how to convince Lean that your proposed transformation is not only a map between the underlying presheaves but a map between the corresponding sheaves. Is there a coercion to this effect?

[Dagur Asgeirsson]

If f : F.val ⟶ G.val is your morphism of underlying presheaves, then ⟨f⟩ or { val := f } gives you the corresponding morphism F ⟶ G of sheaves

[Dagur Asgeirsson]

See docs#CategoryTheory.Sheaf.Hom for how morphisms of sheaves are defined