IsConnected

📁 Source: Mathlib/CategoryTheory/IsConnected.lean

Statistics

Metric	Count
Definitions `IsPreconnected`, `Zag`, `Zigzag`, `setoid`, `discreteIsConnectedEquivPUnit`, `instTransZagZigzag`, `instTransZagZigzag_1`, `instTransZigzag`, `instTransZigzagZag`, `isoConstant`	10
Theorems `is_nonempty`, `of_any_functor_const_on_obj`, `of_constant_of_preserves_morphisms`, `of_induct`, `prod`, `toIsPreconnected`, `iso_constant`, `of_any_functor_const_on_obj`, `of_constant_of_preserves_morphisms`, `prod`, `of_hom`, `of_inv`, `refl`, `of_hom`, `of_hom_hom`, `of_hom_inv`, `of_inv`, `of_inv_hom`, `of_inv_inv`, `of_zag`, `of_zag_trans`, `refl`, `trans`, `any_functor_const_on_obj`, `constant_of_preserves_morphisms`, `constant_of_preserves_morphisms'`, `eq_of_zag`, `eq_of_zigzag`, `equiv_relation`, `exists_zigzag'`, `induct_on_objects`, `instFullFunctorConstOfIsConnected`, `instIsConnectedULiftHomULift`, `isConnected_iff_of_equivalence`, `isConnected_of_equivalent`, `isConnected_of_isConnected_op`, `isConnected_of_nonempty_and_subsingleton`, `isConnected_of_zigzag`, `isConnected_op`, `isConnected_op_iff_isConnected`, `isPreconnected_iff_of_equivalence`, `isPreconnected_induction`, `isPreconnected_of_equivalent`, `isPreconnected_of_isPreconnected_op`, `isPreconnected_of_subsingleton`, `isPreconnected_of_zigzag`, `isPreconnected_op`, `isPreconnected_zigzag`, `nat_trans_from_is_connected`, `nonempty_hom_of_preconnected_groupoid`, `zag_of_zag_obj`, `zag_symmetric`, `zigzag_equivalence`, `zigzag_isConnected`, `zigzag_isPreconnected`, `zigzag_obj_of_zigzag`, `zigzag_prefunctor_obj_of_zigzag`, `zigzag_symmetric`	58
Total	68

CategoryTheory

Definitions

Name	Category	Theorems
`IsPreconnected` 📖	CompData	13 math math: `IsPreconnected.of_constant_of_preserves_morphisms`, `zigzag_isPreconnected`, `IsFilteredOrEmpty.isPreconnected`, `isPreconnected_of_subsingleton`, `isPreconnected_of_equivalent`, `isPreconnected_of_zigzag`, `IsConnected.toIsPreconnected`, `IsPreconnected.of_any_functor_const_on_obj`, `isPreconnected_of_isPreconnected_op`, `IsCofilteredOrEmpty.isPreconnected`, `isPreconnected_iff_of_equivalence`, `IsPreconnected.prod`, `isPreconnected_op`
`Zag` 📖	MathDef	5 math math: `exists_zigzag'`, `Zag.refl`, `zag_symmetric`, `Zag.of_hom`, `Zag.of_inv`
`Zigzag` 📖	MathDef	14 math math: `Zigzag.of_inv_inv`, `isPreconnected_zigzag`, `Zigzag.refl`, `Zigzag.of_hom_hom`, `Limits.Types.zigzag_of_eqvGen_colimitTypeRel`, `Zigzag.of_zag_trans`, `zigzag_symmetric`, `Zigzag.of_zag`, `Zigzag.of_inv_hom`, `Functor.Final.zigzag_of_eqvGen_colimitTypeRel`, `Zigzag.of_hom_inv`, `Zigzag.of_hom`, `Zigzag.of_inv`, `zigzag_equivalence`
`discreteIsConnectedEquivPUnit` 📖	CompOp	—
`instTransZagZigzag` 📖	CompOp	—
`instTransZagZigzag_1` 📖	CompOp	—
`instTransZigzag` 📖	CompOp	—
`instTransZigzagZag` 📖	CompOp	—
`isoConstant` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`any_functor_const_on_obj` 📖	mathematical	—	`Functor.obj` `Discrete` `discreteCategory`	—	`Discrete.ext`
`constant_of_preserves_morphisms` 📖	—	—	—	—	`Discrete.ext` `eqToHom_trans` `any_functor_const_on_obj`
`constant_of_preserves_morphisms'` 📖	—	—	—	—	`IsConnected.is_nonempty` `constant_of_preserves_morphisms` `IsConnected.toIsPreconnected`
`eq_of_zag` 📖	mathematical	`Zag` `Discrete` `discreteCategory`	`Discrete.as`	—	`Discrete.eq_of_hom`
`eq_of_zigzag` 📖	mathematical	`Zigzag` `Discrete` `discreteCategory`	`Discrete.as`	—	`eq_of_zag`
`equiv_relation` 📖	—	—	—	—	`induct_on_objects`
`exists_zigzag'` 📖	mathematical	—	`Zag`	—	`List.exists_isChain_cons_of_relationReflTransGen` `isPreconnected_zigzag` `IsConnected.toIsPreconnected`
`induct_on_objects` 📖	—	`Set` `Set.instMembership`	—	—	`constant_of_preserves_morphisms`
`instFullFunctorConstOfIsConnected` 📖	mathematical	—	`Functor.Full` `Functor` `Functor.category` `Functor.const`	—	`IsConnected.is_nonempty` `NatTrans.ext'` `nat_trans_from_is_connected` `IsConnected.toIsPreconnected`
`instIsConnectedULiftHomULift` 📖	mathematical	—	`IsConnected` `ULiftHom` `ULiftHom.category` `uliftCategory`	—	`IsConnected.of_induct` `IsConnected.is_nonempty` `induct_on_objects` `IsConnected.toIsPreconnected`
`isConnected_iff_of_equivalence` 📖	mathematical	—	`IsConnected`	—	`isConnected_of_equivalent`
`isConnected_of_equivalent` 📖	mathematical	—	`IsConnected`	—	`isPreconnected_of_equivalent` `IsConnected.toIsPreconnected` `Nonempty.map` `IsConnected.is_nonempty`
`isConnected_of_isConnected_op` 📖	mathematical	—	`IsConnected`	—	`isConnected_of_equivalent` `isConnected_op`
`isConnected_of_nonempty_and_subsingleton` 📖	mathematical	—	`IsConnected`	—	`isPreconnected_of_subsingleton`
`isConnected_of_zigzag` 📖	mathematical	`Zag`	`IsConnected`	—	`isPreconnected_of_zigzag`
`isConnected_op` 📖	mathematical	—	`IsConnected` `Opposite` `Category.opposite`	—	`isPreconnected_op` `IsConnected.toIsPreconnected` `IsConnected.is_nonempty`
`isConnected_op_iff_isConnected` 📖	mathematical	—	`IsConnected` `Opposite` `Category.opposite`	—	`isConnected_of_isConnected_op` `isConnected_op`
`isPreconnected_iff_of_equivalence` 📖	mathematical	—	`IsPreconnected`	—	`isPreconnected_of_equivalent`
`isPreconnected_induction` 📖	—	—	—	—	`induct_on_objects`
`isPreconnected_of_equivalent` 📖	mathematical	—	`IsPreconnected`	—	—
`isPreconnected_of_isPreconnected_op` 📖	mathematical	—	`IsPreconnected`	—	`isPreconnected_of_equivalent` `isPreconnected_op`
`isPreconnected_of_subsingleton` 📖	mathematical	—	`IsPreconnected`	—	`Category.comp_id` `Discrete.instSubsingletonDiscreteHom`
`isPreconnected_of_zigzag` 📖	mathematical	`Zag`	`IsPreconnected`	—	`zigzag_isPreconnected` `List.relationReflTransGen_of_exists_isChain_cons`
`isPreconnected_op` 📖	mathematical	—	`IsPreconnected` `Opposite` `Category.opposite`	—	`Discrete.ext` `Discrete.eq_of_hom` `IsPreconnected.iso_constant` `Category.comp_id` `Discrete.instSubsingletonDiscreteHom`
`isPreconnected_zigzag` 📖	mathematical	—	`Zigzag`	—	`equiv_relation` `zigzag_equivalence` `Relation.ReflTransGen.single`
`nat_trans_from_is_connected` 📖	mathematical	—	`NatTrans.app` `Functor.obj` `Functor` `Functor.category` `Functor.const`	—	`constant_of_preserves_morphisms` `Category.comp_id` `Category.id_comp` `NatTrans.naturality`
`nonempty_hom_of_preconnected_groupoid` 📖	mathematical	—	`Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Groupoid.toCategory`	—	`equiv_relation` `Nonempty.map` `IsGroupoid.all_isIso` `instIsGroupoid` `Nonempty.map2`
`zag_of_zag_obj` 📖	—	`Zag` `Functor.obj`	—	—	`Nonempty.map`
`zag_symmetric` 📖	mathematical	—	`Symmetric` `Zag`	—	—
`zigzag_equivalence` 📖	mathematical	—	`Zigzag`	—	`Relation.reflexive_reflTransGen` `zigzag_symmetric` `Relation.transitive_reflTransGen`
`zigzag_isConnected` 📖	mathematical	`Zigzag`	`IsConnected`	—	`zigzag_isPreconnected`
`zigzag_isPreconnected` 📖	mathematical	`Zigzag`	`IsPreconnected`	—	`IsPreconnected.of_constant_of_preserves_morphisms`
`zigzag_obj_of_zigzag` 📖	mathematical	`Zigzag`	`Functor.obj`	—	`zigzag_prefunctor_obj_of_zigzag`
`zigzag_prefunctor_obj_of_zigzag` 📖	mathematical	`Zigzag`	`Prefunctor.obj` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	`Relation.ReflTransGen.lift` `Nonempty.map`
`zigzag_symmetric` 📖	mathematical	—	`Symmetric` `Zigzag`	—	`Relation.ReflTransGen.symmetric` `zag_symmetric`

CategoryTheory.IsConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_nonempty` 📖	—	—	—	—	—
`of_any_functor_const_on_obj` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	`CategoryTheory.IsConnected`	—	`CategoryTheory.IsPreconnected.of_any_functor_const_on_obj`
`of_constant_of_preserves_morphisms` 📖	mathematical	—	`CategoryTheory.IsConnected`	—	`CategoryTheory.IsPreconnected.of_constant_of_preserves_morphisms`
`of_induct` 📖	mathematical	`Set` `Set.instMembership`	`CategoryTheory.IsConnected`	—	`of_constant_of_preserves_morphisms`
`prod` 📖	mathematical	—	`CategoryTheory.IsConnected` `CategoryTheory.prod'`	—	`CategoryTheory.IsPreconnected.prod` `toIsPreconnected` `is_nonempty`
`toIsPreconnected` 📖	mathematical	—	`CategoryTheory.IsPreconnected`	—	—

CategoryTheory.IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_constant` 📖	mathematical	—	`CategoryTheory.Iso` `CategoryTheory.Functor` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const`	—	—
`of_any_functor_const_on_obj` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	`CategoryTheory.IsPreconnected`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Discrete.instSubsingletonDiscreteHom`
`of_constant_of_preserves_morphisms` 📖	mathematical	—	`CategoryTheory.IsPreconnected`	—	`of_any_functor_const_on_obj` `CategoryTheory.Discrete.ext` `CategoryTheory.Discrete.eq_of_hom`
`prod` 📖	mathematical	—	`CategoryTheory.IsPreconnected` `CategoryTheory.prod'`	—	`of_any_functor_const_on_obj` `CategoryTheory.any_functor_const_on_obj`

CategoryTheory.Zag

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_hom` 📖	mathematical	—	`CategoryTheory.Zag`	—	—
`of_inv` 📖	mathematical	—	`CategoryTheory.Zag`	—	—
`refl` 📖	mathematical	—	`CategoryTheory.Zag`	—	—

CategoryTheory.Zigzag

Definitions

Name	Category	Theorems
`setoid` 📖	CompOp	1 math math: `CategoryTheory.Functor.mapConnectedComponents_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_hom` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`of_zag` `CategoryTheory.Zag.of_hom`
`of_hom_hom` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`trans` `of_hom`
`of_hom_inv` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`trans` `of_hom` `of_inv`
`of_inv` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`of_zag` `CategoryTheory.Zag.of_inv`
`of_inv_hom` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`trans` `of_inv` `of_hom`
`of_inv_inv` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`trans` `of_inv`
`of_zag` 📖	mathematical	`CategoryTheory.Zag`	`CategoryTheory.Zigzag`	—	`Relation.ReflTransGen.single`
`of_zag_trans` 📖	mathematical	`CategoryTheory.Zag`	`CategoryTheory.Zigzag`	—	`trans` `of_zag`
`refl` 📖	mathematical	—	`CategoryTheory.Zigzag`	—	`CategoryTheory.zigzag_equivalence`
`trans` 📖	—	`CategoryTheory.Zigzag`	—	—	`CategoryTheory.zigzag_equivalence`

---

← Back to Index