Commit 2025-11-17 00:03 a2f7a8f9

feat(CategoryTheory): dense functors (#29565) A functor F : C ⥤ D is dense if 𝟭 D is a pointwise left Kan extension of F along itself, i.e. any Y : D is the colimit of all F.obj X for all morphisms F.obj X ⟶ Y (which is the condition F.DenseAt Y). When F is full, we show that this is equivalent to saying that the restricted Yoneda functor D ⥤ Cᵒᵖ ⥤ Type _ is fully faithful. We also show that the range of a dense functor is a strong generator.