Documentation Verification Report

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	47 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`, `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.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	47 math math: `isConnected_compl_of_one_lt_codim`, `IsPathConnected.isConnected`, `isConnected_compl_singleton_of_one_lt_rank`, `isConnected_Ioc`, `Convex.isConnected`, `AffineSubspace.isConnected_setOf_wOppSide`, `isConnected_sphere`, `isConnected_connectedComponent`, `Complex.isConnected_of_lowerHalfPlane`, `isConnected_Iio`, `isConnected_singleton`, `isConnected_Ici`, `IsSelfAdjoint.isConnected_spectrum_compl`, `isConnected_Icc`, `isConnected_Ioo`, `isConnected_univ_pi`, `AffineSubspace.isConnected_setOf_wSameSide`, `isConnected_univ`, `isConnected_Ico`, `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_Iic`, `isConnected_connectedComponentIn_iff`, `Homeomorph.isConnected_image`, `Metric.isConnected_closedEBall`, `AffineSubspace.isConnected_setOf_sOppSide`, `Metric.isConnected_ball`, `isConnected_Ioi`, `isConnected_iff_sUnion_disjoint_open`, `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