something about pullback

Stream: Is there code for X?

[Kenny Lau]

This is also a general question on how can I find stuff more efficiently, I feel like half of the time I'm finding the correct thing in the library:

image.png

so I want to use pullbacks but in terms of over categories. More concretely, I think X -> S above defines a functor Over S => Over X. What is this functor called?

[Bhavik Mehta]

docs#CategoryTheory.Over.pullback

[Kenny Lau]

aha, thanks!

[Kenny Lau]

@Bhavik Mehta and what is this itself as a functor?

[Calle Sönne]

docs#CategoryTheory.Over.map maybe?

[Bhavik Mehta]

I don't believe that exists right now, although the way it acts on identity and composition is in mathlib

[Calle Sönne]

no wait sorry! I was too quick

[Kenny Lau]

maybe it isn't in there because it involves 2-categories?

[Calle Sönne]

But to maybe answer your secret question: do you know about loogle since you came back (maybe you already do)?

[Kenny Lau]

yeah I've been using loogle

[Bhavik Mehta]

Kenny Lau said:

maybe it isn't in there because it involves 2-categories?

Yeah, Over.pullback was made before 2-categories were in mathlib

[Calle Sönne]

So maybe what you want is a natural transformation between two different pseudofunctors (the ones sending a scheme resp. S scheme to the over category)?

[Calle Sönne]

And these pseudofunctors don't seem to exist. The bicategory people are slacking!

[Kenny Lau]

image.png

[Kenny Lau]

I seem to need the bicategory stuff

[Kenny Lau]

basically I have a functor F, and I want Over X => Over F(X)

[Christian Merten]

This is just docs#Over.post

[Kenny Lau]

oh, interesting

[Kenny Lau]

thanks!

[Edward van de Meent]

(CategoryTheory.Over.post)

[Kenny Lau]

Could someone tell me all the idioms of Over, i find myself being confused by it a lot, and I can't really find it in the docstrings

[Kenny Lau]

image.png

[Kenny Lau]

so from these two I deduce that the idiom is left and hom

[Kenny Lau]

I think it would be better to put this information on the docstring of Over?

[Bhavik Mehta]

These are just the projections for the components of Over, inherited from those for Comma. But I have no objections to adding this to the Over docstring anyway