Structures · Category theory
CategoryTheory.IsConnected
We define a connected category as a _nonempty_ category for which every functor to a discrete category is constant. NB. Some authors include the empty category as connected, we do not. We instead are interested in categories with exactly one 'connected component'. This allows us to show that the functor X ⨯ - preserves connected limits.
- Defined in
- Mathlib.CategoryTheory.IsConnected
- Shape
- One type argument · adds is_nonempty
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.IsConnected is also a
Concrete types that are instances13
- CategoryTheory.Comma
- CategoryTheory.CostructuredArrow
- CategoryTheory.StructuredArrow
- CategoryTheory.ULiftHom
- CategoryTheory.ActionCategory
- CategoryTheory.LocalizerMorphism.LeftResolution
- CategoryTheory.LocalizerMorphism.RightResolution
- CategoryTheory.Limits.WalkingParallelPair
- CategoryTheory.Limits.WidePullbackShape
- CategoryTheory.Limits.WidePushoutShape
- CategoryTheory.ConnectedComponents.Component
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by71
- CategoryTheory.isConnected_of_equivalent
- CategoryTheory.Limits.isColimitConstCocone
- CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone
- CategoryTheory.isConnected_of_isConnected_op
- CategoryTheory.constant_of_preserves_morphisms'
- CategoryTheory.Limits.isLimitConstCone
- CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
- CategoryTheory.Limits.IsColimit.isIso_colimMap_ι
- CategoryTheory.Limits.Types.isColimitPUnitCocone
- CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected
- CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape
- CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShape
- CategoryTheory.Limits.IsColimit.pullback_hom_ext
- CategoryTheory.Limits.Types.colimitConstPUnitIsoPUnit
- CategoryTheory.Limits.IsLimit.isIso_limMap_π
- CategoryTheory.Limits.IsColimit.pullback_zero_ext
- CategoryTheory.Limits.IsLimit.pushout_hom_ext
- CategoryTheory.Limits.Cone.isLimitOfIsIsoLimMapπ
- CategoryTheory.Comma.initial_snd_of_isConnected_costructuredArrow
- CategoryTheory.Limits.Cocone.isColimitOfIsIsoColimMapι
- CategoryTheory.Limits.Types.instHasColimitConstPUnitFunctor
- CategoryTheory.Over.hasLimitsOfShape_of_isConnected
- CategoryTheory.instIsConnectedULiftHomULift
- IsFreeGroupoid.generators_connected
- CategoryTheory.initial_snd
- CategoryTheory.CostructuredArrow.hasLimitsOfShape_of_isConnected
- CategoryTheory.Join.instFinalInclRightOfIsConnected
- CategoryTheory.Under.createsColimitsOfShapeForgetOfIsConnected
- CategoryTheory.Limits.hasLimit_const_of_isConnected
- CategoryTheory.Comma.isConnected_comma_of_final
- CategoryTheory.isConnected_op
- CategoryTheory.IsConnected.is_nonempty
- CategoryTheory.CostructuredArrow.instPreservesLimitsOfShapeProjOfIsConnected
- CategoryTheory.Under.hasColimitsOfShape_of_isConnected
- CategoryTheory.CostructuredArrow.CreatesConnected.isLimitRaiseCone
- CategoryTheory.StructuredArrow.instCreatesColimitsOfShapeProjOfIsConnected
- CategoryTheory.Under.preservesColimitsOfShape_forget_of_isConnected
- CategoryTheory.Comma.isConnected_comma_of_initial
- CategoryTheory.Limits.isColimitOfIsPushoutOfIsConnected
- CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected
- CategoryTheory.Limits.isLimitConstCone.congr_simp
- CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected
- CategoryTheory.instFinalDiscreteOfIsConnected
- IsFreeGroupoid.endIsFreeOfConnectedFree
- CategoryTheory.initial_fst
- CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_π_app
- CategoryTheory.Limits.IsLimit.pushout_zero_ext
- CategoryTheory.Limits.isColimitConstCocone.congr_simp
- CategoryTheory.CostructuredArrow.instCreatesLimitsOfShapeProjOfIsConnected
- CategoryTheory.StructuredArrow.instHasColimitsOfShapeOfIsConnected