Today @sinhp and I discovered that there are two definitions of the pullback functor between over categories:

(i) one called Over.pullback that appears in Limits.Over.

(ii) one called Over.baseChange that appears in Adjunction.Over and

Over.pullback is proven to be a right adjoint in Over.mapPullbackAdj, while Over.baseChange was proven to be a right adjoint in Over.mapAdjunction --- my first mathlib PR!

The comments to the Limits.Over file mention a TODO: If C has binary products, then forget X : Over X ⥤ C has a right adjoint. This appears as Over.forgetAdjStar in the Over.Adjunction file.

@sinhp has discussed this with @jcommelin and @joelriou who confirm that the correct place for this material is in the adjunction folder. But I have no clue which names, constructions, etc are best.