IsConnected

📁 Source: Mathlib/CategoryTheory/Limits/IsConnected.lean

Statistics

Metric	Count
Definitions IsConnected, colimitConstPUnitIsoPUnit, constPUnitFunctor, isColimitPUnitCocone, pUnitCocone, IsConnected, IsConnected	7
Theorems isConnected_iff_of_final, isConnected_iff_of_initial, instHasColimitConstPUnitFunctor, instSubsingletonColimitPUnit, isConnected_iff_colimit_constPUnitFunctor_iso_pUnit, isConnected_iff_isColimit_pUnitCocone, pUnitCocone_pt, pUnitCocone_ι_app, zigzag_of_eqvGen_colimitTypeRel, isConnected_of_hasInitial, isConnected_of_hasTerminal, isConnected_of_isInitial, isConnected_of_isTerminal	13
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
IsConnected 📖	CompData	48 math math: TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, Functor.isConnected_iff_of_final, IsConnected.of_induct, isConnected_of_zigzag, isConnected_op_iff_isConnected, isConnected_op, IsConnected.of_constant_of_preserves_morphisms, Comma.isConnected_comma_of_initial, TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, isConnected_iff_of_equivalence, isConnected_of_hasTerminal, Functor.Final.out, isConnected_of_hasInitial, Functor.Initial.out, instIsConnectedWidePushoutShape, IsCofiltered.isConnected, Limits.Types.isConnected_iff_isColimit_pUnitCocone, HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, IsFiltered.isConnected, HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, instIsConnectedULiftHomULift, widePullbackShape_connected, TwoSquare.GuitartExact.isConnected_rightwards, LocalizerMorphism.isConnected_rightResolution_of_functorial_resolutions, isConnected_of_nonempty_and_subsingleton, Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit, isConnected_of_isInitial, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected, isConnected_iff_initial_of_unique, TwoSquare.isConnected_rightwards_iff_downwards, Comma.isConnected_comma_of_final, IsConnected.prod, Limits.WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, isConnected_iff_final_of_unique, instIsConnectedComponent, TwoSquare.guitartExact_iff_isConnected_rightwards, IsSifted.instIsConnected, widePushoutShape_connected, zigzag_isConnected, instIsConnectedWidePullbackShape, IsConnected.of_any_functor_const_on_obj, TwoSquare.guitartExact_iff_isConnected_downwards, ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty, parallel_pair_connected, isConnected_of_equivalent, isConnected_of_isTerminal, Functor.isConnected_iff_of_initial, isConnected_of_isConnected_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_of_hasInitial 📖	mathematical	—	IsConnected	—	isConnected_of_isInitial
isConnected_of_hasTerminal 📖	mathematical	—	IsConnected	—	isConnected_of_isTerminal
isConnected_of_isInitial 📖	mathematical	—	IsConnected	—	isConnected_of_zigzag Zag.symm Zag.of_hom
isConnected_of_isTerminal 📖	mathematical	—	IsConnected	—	isConnected_of_zigzag Zag.of_hom Zag.symm

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_iff_of_final 📖	mathematical	—	CategoryTheory.IsConnected	—	CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit Equiv.nonempty_congr
isConnected_iff_of_initial 📖	mathematical	—	CategoryTheory.IsConnected	—	CategoryTheory.isConnected_op_iff_isConnected isConnected_iff_of_final final_op_of_initial

CategoryTheory.Limits.Types

Definitions

Name	Category	Theorems
colimitConstPUnitIsoPUnit 📖	CompOp	—
constPUnitFunctor 📖	CompOp	6 math math: pUnitCocone_pt, pUnitCocone_ι_app, instHasColimitConstPUnitFunctor, isConnected_iff_isColimit_pUnitCocone, instSubsingletonColimitPUnit, isConnected_iff_colimit_constPUnitFunctor_iso_pUnit
isColimitPUnitCocone 📖	CompOp	—
pUnitCocone 📖	CompOp	3 math math: pUnitCocone_pt, pUnitCocone_ι_app, isConnected_iff_isColimit_pUnitCocone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimitConstPUnitFunctor 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.types constPUnitFunctor	—	—
instSubsingletonColimitPUnit 📖	mathematical	—	CategoryTheory.Limits.colimit CategoryTheory.types constPUnitFunctor	—	jointly_surjective' CategoryTheory.constant_of_preserves_morphisms colimit_sound
isConnected_iff_colimit_constPUnitFunctor_iso_pUnit 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.Iso CategoryTheory.types CategoryTheory.Limits.colimit constPUnitFunctor	—	nonempty_of_nonempty_colimit Nonempty.map CategoryTheory.zigzag_isConnected zigzag_of_eqvGen_colimitTypeRel colimit_eq Equiv.injective
isConnected_iff_isColimit_pUnitCocone 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.Limits.IsColimit CategoryTheory.types constPUnitFunctor pUnitCocone	—	isConnected_iff_colimit_constPUnitFunctor_iso_pUnit
pUnitCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.types constPUnitFunctor pUnitCocone	—	—
pUnitCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types constPUnitFunctor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι pUnitCocone	—	—
zigzag_of_eqvGen_colimitTypeRel 📖	mathematical	Relation.EqvGen CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.ColimitTypeRel	CategoryTheory.Zigzag CategoryTheory.Functor.obj CategoryTheory.types	—	CategoryTheory.Zigzag.of_hom CategoryTheory.Zigzag.refl CategoryTheory.zigzag_symmetric CategoryTheory.Zigzag.trans

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
IsConnected 📖	CompData	9 math math: PreservesIsConnected.preserves, exists_set_ker_evaluation_subset_of_isOpen, exists_lift_of_mono_of_isConnected, fiber_in_connected_component, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, IsGalois.toIsConnected, has_decomp_connected_components', has_decomp_connected_components, CategoryTheory.FintypeCat.Action.isConnected_of_transitive

(root)

Definitions

Name	Category	Theorems
IsConnected 📖	MathDef	59 math math: isConnected_compl_of_one_lt_codim, IsPathConnected.isConnected, isConnected_compl_singleton_of_one_lt_rank, isConnected_Ioc, IsConnected.image, IsConnected.iUnion_of_reflTransGen, Convex.isConnected, AffineSubspace.isConnected_setOf_wOppSide, isConnected_sphere, isConnected_connectedComponent, preimage_connectedComponent_connected, Complex.isConnected_of_lowerHalfPlane, IsConnected.biUnion_of_chain, isConnected_Iio, IsConnected.biUnion_of_reflTransGen, isConnected_singleton, isConnected_Ici, IsSelfAdjoint.isConnected_spectrum_compl, isConnected_Icc, isConnected_Ioo, isConnected_univ_pi, IsConnected.preimage_of_isClosedMap, AffineSubspace.isConnected_setOf_wSameSide, isConnected_univ, IsConnected.subset_closure, isConnected_Ico, IsConnected.closure, Set.Countable.isConnected_compl_of_one_lt_rank, Complex.isConnected_of_upperHalfPlane, isConnected_setOf_sameRay_and_ne_zero, Metric.isConnected_closedBall, Homeomorph.isConnected_preimage, isConnected_range, IsConnected.union, isConnected_Iic, isConnected_connectedComponentIn_iff, Homeomorph.isConnected_image, Metric.isConnected_closedEBall, AffineSubspace.isConnected_setOf_sOppSide, Metric.isConnected_ball, IsConnected.prod, isConnected_Ioi, isConnected_iff_sUnion_disjoint_open, IsConnected.iUnion_of_chain, IsConnected.preimage_of_isOpenMap, LocallyConnectedSpace.open_connected_basis, Sum.isConnected_iff, locallyConnectedSpace_iff_subsets_isOpen_isConnected, Metric.isConnected_eball, connectedSpace_iff_univ, isConnected_setOf_sameRay, Sigma.isConnected_iff, isConnected_uIoo, isConnected_uIoc, IsIrreducible.isConnected, locallyConnectedSpace_iff_hasBasis_isOpen_isConnected, IsOpen.isConnected_iff_isPathConnected, AffineSubspace.isConnected_setOf_sSameSide, isConnected_iff_connectedSpace

---

← Back to Index