Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorEric
• CommentTimeMay 21st 2010

On the page hom-functor, it says

There is also a contravariant hom-functor

$hom(-,c) : C^{op} \to Set,$

where $C^{op}$ is the opposite category to $C$, which sends any object $x \in C^{op}$ to the hom-set $hom(x,c)$.

If you write it like this, should you really call it “contravariant”? When you write $C^{op}$, I thought you should call it just “functor” or “covariant”. By saying it is contravariant AND writing $C^{op}$, it seems like double counting.

I hope to add some illustrations to these pages. It is a shame there are not more illustrations on the nLab since nStuff is so amenable to nice pictures.

• CommentRowNumber2.
• CommentAuthorDavidRoberts
• CommentTimeMay 21st 2010

One could argue that the functor is just called the ”contravariant hom-functor, to distinguish it, as saying ’hom-functor’ could mean one of three things: $Hom(-,c),Hom(c,-)$ or $Hom(-,-)$. But I don’t really know the rationale.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeMay 21st 2010

Thanks for spotting this.

I completely rewrote the page, and expanded it.

Also created a stub for product category.

• CommentRowNumber4.
• CommentAuthorEric
• CommentTimeMay 21st 2010
• (edited May 21st 2010)

Nice. Thanks :)

Edit: For a second, I changed functor to profunctor, but realized it wasn’t quite right so changed it back. It would be interesting to relate hom-functor and profunctor somehow though (I just did it wrong).

Relation to profunctors

A hom-functor $C^{op}\times C\to Set$ is also a profunctor $C ⇸ C$.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeMay 21st 2010

That’s right Eric:

The hom-functor $C^{op} \times C \to Set$ is the identity profunctor $Id : C ⇸ C$ !

• CommentRowNumber6.
• CommentAuthorEric
• CommentTimeMay 21st 2010

Whoa :)

Ok. Changed it to

Relation to profunctors

A hom-functor $C^{op}\times C\to Set$ is also the identity profunctor $1_C: C ⇸ C$.

:)

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeMay 21st 2010

Whoa :)

Yeah, speaking of striking category theory. ;-)

I added to hom-functor some remarks on why this is the case. And also to the beginning of profunctor.

A good warm-up excercise if you want to play around with the Yoneda embedding.

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeMay 21st 2010

Eric, this statement (that $hom$ is a unit profunctor) is also essentially the key fact of Yoneda reduction (which I really need to get into better shape).

• CommentRowNumber9.
• CommentAuthorEric
• CommentTimeMay 21st 2010

Thanks. The reason I’m reading this page on hom-functor is that I’m working on Yoneda lemma from Vistoli’s paper. His explanation of Yoneda lemma is very nice. As usual, I will not understand until I’ve drawn some pictures so was hoping to add some illustrations to the nLab.

• CommentRowNumber10.
• CommentAuthorAndrew Stacey
• CommentTimeMay 21st 2010

(Just testing to see if I can post here)

• CommentRowNumber11.
• CommentAuthorEric
• CommentTimeMay 21st 2010

Test

1. adding text from HoTT wiki

Anonymous

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeJun 7th 2022

Wait, there is nothing specific to homotopy type theory in what you just added. You are essentially just re-stating the usual definition.

It’s great that you are copying material from the HoTT-wiki, but let’s do it a little less mechanically, more with an eye towards retaining logic and cosistency of existing entries.