Topic: connected categories
Reid Barton (Sep 12 2018 at 16:57):
I took a stab at defining an "interface" for what it means for a category to be connected and used it to prove a standard fact about cofinal functors. @Mario Carneiro I'm curious to hear whether you would suggest any improvements.
Reid Barton (Sep 12 2018 at 16:59):
I didn't bother actually defining
connected as I figure it's easy once you have the interface right. So the interface is the three
components is not used directly, but the definition of
connected should make proving
connected_iff_components_trivial easy so it should probably be related to
components in some way.
Reid Barton (Sep 12 2018 at 17:05):
I guess I didn't include any way to prove that a category is connected, but I feel like that side of things should be easier
Reid Barton (Sep 12 2018 at 17:43):
Actually I need the inv_fun direction of
connected_iff_components_trivial elsewhere, so that can also be considered part of the interface
Last updated: May 06 2021 at 17:38 UTC