search

b-mehta / topos

Topos theory in lean
56 stars 2 forks source link

Creating connected limits #27

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

Ref: Example sheet 2, question 5(ii) from PTJ.

A category J is said to be connected if it has just one connected component, i.e. (it is nonempty and) any two objects of J may be linked by a ‘zig-zag’ of morphisms. Let C be a category, and A an object of C. Show that the forgetful functor C/A → C creates connected limits.

I really only need this when J is cospan, i.e. C/A → C creates pullbacks, but the full result would be cool too.

b-mehta commented 4 years ago

This is done for J=cospan, but it's pretty unpleasant

b-mehta commented 4 years ago

Here's an idea of how it might be done. Define a connected category as one where every functor to a discrete category is constant (that is, given a functor F : J => discrete T, we produce an object j of J such that Fj = Fk for any j other k in J; and Ff = 1_{Fj} for any morphism f. It then suffices to show that prodinl X preserves limits of shape J (for any connected J), which when you unpack it amounts to showing that for any category C and objects A,B in C, there is a unique natural transformation between the functors G : J => C := const A and H : J => C := const B. But this is easy by using T as the homset A -> B of C in the definition of connected category

b-mehta commented 4 years ago

Done in https://github.com/b-mehta/topos/blob/connected/src/connected.lean