Commit 2024-05-19 09:37 d874bdff

feat: moving some adjunctions of over categories to CategoryTheory.Adjunction.Over (#12980) We move the functor CategoryTheory.Over.baseChange and the adjunction CategoryTheory.Over.mapAdjunction to CategoryTheory.Adjunction.Over. Note that we already have

def forgetAdjStar [HasBinaryProducts C] : Over.forget X ⊣ star X

in the file CategoryTheory.Adjunction.Over and it would make sense to have the facts about adjunction of Over categories in one place. This change also reduces the length of the file CategoryTheory.Limits.Shapes.Pullbacks which is almost 3k LOC.