Commit 2024-05-19 09:37 d874bdff
View on Github →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.