mathlib3 documentation


Connected limits in the over category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Shows that the forgetful functor over B ⥤ C creates connected limits, in particular over B has any connected limit which C has.

(Impl) Given a diagram in the over category, produce a natural transformation from the diagram legs to the specific object.


(Impl) Given a cone in the base category, raise it to a cone in the over category. Note this is where the connected assumption is used.

@[protected, instance]

The over category has any connected limit which the original category has.