Basic

📁 Source: Mathlib/CategoryTheory/GuitartExact/Basic.lean

Statistics

Metric	Count
Definitions CostructuredArrowDownwards, mk, functor, inverse, GuitartExact, StructuredArrowRightwards, mk, costructuredArrowDownwardsPrecomp, costructuredArrowRightwards, equivalenceJ, structuredArrowDownwards	11
Theorems mk_surjective, functor_map, functor_obj, inverse_map, inverse_obj, isConnected_rightwards, mk_surjective, costructuredArrowDownwardsPrecomp_map, costructuredArrowDownwardsPrecomp_obj, costructuredArrowRightwards_map, costructuredArrowRightwards_obj, equivalenceJ_counitIso, equivalenceJ_functor, equivalenceJ_inverse, equivalenceJ_unitIso, guitartExact_id, guitartExact_iff_final, guitartExact_iff_initial, guitartExact_iff_isConnected_downwards, guitartExact_iff_isConnected_rightwards, guitartExact_of_isEquivalence_of_isIso, instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, isConnected_rightwards_iff_downwards, structuredArrowDownwards_map, structuredArrowDownwards_obj	28
Total	39

CategoryTheory.TwoSquare

Definitions

Name	Category	Theorems
CostructuredArrowDownwards 📖	CompOp	25 math math: structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, structuredArrowRightwardsOpEquivalence_inverse, EquivalenceJ.inverse_map, structuredArrowRightwardsOpEquivalence.functor_obj_right_as, structuredArrowRightwardsOpEquivalence.functor_obj_left_right, equivalenceJ_unitIso, structuredArrowRightwardsOpEquivalence_counitIso, equivalenceJ_counitIso, costructuredArrowDownwardsPrecomp_obj, equivalenceJ_inverse, structuredArrowRightwardsOpEquivalence.functor_map_left_right, structuredArrowRightwardsOpEquivalence_unitIso, costructuredArrowDownwardsPrecomp_map, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected, EquivalenceJ.functor_obj, isConnected_rightwards_iff_downwards, EquivalenceJ.functor_map, equivalenceJ_functor, EquivalenceJ.inverse_obj, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, guitartExact_iff_isConnected_downwards, structuredArrowRightwardsOpEquivalence_functor, structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as
GuitartExact 📖	CompData	25 math math: CategoryTheory.instGuitartExactOverObjOverPostOfHasBinaryProductOfPreservesLimitDiscreteWalkingPairPair, guitartExact_id', GuitartExact.vComp_iff_of_equivalences, guitartExact_iff_initial, guitartExact_id, GuitartExact.vComp'_iff_of_equivalences, GuitartExact.whiskerVertical_iff, guitartExact_op_iff, CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure', GuitartExact.instWhiskerVerticalOfIsIsoFunctor, guitartExact_of_isEquivalence_of_isIso, CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure, CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.guitartExact', instGuitartExactOppositeOp, CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure, CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure', guitartExact_iff_isConnected_rightwards, guitartExact_iff_final, GuitartExact.vComp, guitartExact_iff_isConnected_downwards, GuitartExact.vComp', CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff, CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact', GuitartExact.whiskerVertical
StructuredArrowRightwards 📖	CompOp	21 math math: structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, structuredArrowRightwardsOpEquivalence_inverse, EquivalenceJ.inverse_map, structuredArrowRightwardsOpEquivalence.functor_obj_right_as, structuredArrowRightwardsOpEquivalence.functor_obj_left_right, equivalenceJ_unitIso, structuredArrowRightwardsOpEquivalence_counitIso, equivalenceJ_counitIso, equivalenceJ_inverse, GuitartExact.isConnected_rightwards, structuredArrowRightwardsOpEquivalence.functor_map_left_right, structuredArrowRightwardsOpEquivalence_unitIso, EquivalenceJ.functor_obj, isConnected_rightwards_iff_downwards, guitartExact_iff_isConnected_rightwards, EquivalenceJ.functor_map, equivalenceJ_functor, EquivalenceJ.inverse_obj, structuredArrowRightwardsOpEquivalence_functor, structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as
costructuredArrowDownwardsPrecomp 📖	CompOp	2 math math: costructuredArrowDownwardsPrecomp_obj, costructuredArrowDownwardsPrecomp_map
costructuredArrowRightwards 📖	CompOp	26 math math: structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, structuredArrowRightwardsOpEquivalence_inverse, EquivalenceJ.inverse_map, structuredArrowRightwardsOpEquivalence.functor_obj_right_as, structuredArrowRightwardsOpEquivalence.functor_obj_left_right, equivalenceJ_unitIso, costructuredArrowRightwards_map, structuredArrowRightwardsOpEquivalence_counitIso, equivalenceJ_counitIso, instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, equivalenceJ_inverse, GuitartExact.isConnected_rightwards, structuredArrowRightwardsOpEquivalence.functor_map_left_right, structuredArrowRightwardsOpEquivalence_unitIso, EquivalenceJ.functor_obj, isConnected_rightwards_iff_downwards, guitartExact_iff_isConnected_rightwards, EquivalenceJ.functor_map, equivalenceJ_functor, guitartExact_iff_final, EquivalenceJ.inverse_obj, structuredArrowRightwardsOpEquivalence_functor, costructuredArrowRightwards_obj, structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as
equivalenceJ 📖	CompOp	4 math math: equivalenceJ_unitIso, equivalenceJ_counitIso, equivalenceJ_inverse, equivalenceJ_functor
structuredArrowDownwards 📖	CompOp	30 math math: structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, structuredArrowRightwardsOpEquivalence_inverse, EquivalenceJ.inverse_map, structuredArrowRightwardsOpEquivalence.functor_obj_right_as, instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, structuredArrowRightwardsOpEquivalence.functor_obj_left_right, equivalenceJ_unitIso, guitartExact_iff_initial, structuredArrowRightwardsOpEquivalence_counitIso, equivalenceJ_counitIso, costructuredArrowDownwardsPrecomp_obj, equivalenceJ_inverse, structuredArrowRightwardsOpEquivalence.functor_map_left_right, structuredArrowRightwardsOpEquivalence_unitIso, costructuredArrowDownwardsPrecomp_map, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected, EquivalenceJ.functor_obj, isConnected_rightwards_iff_downwards, structuredArrowDownwards_map, structuredArrowDownwards_obj, EquivalenceJ.functor_map, equivalenceJ_functor, EquivalenceJ.inverse_obj, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, guitartExact_iff_isConnected_downwards, structuredArrowRightwardsOpEquivalence_functor, structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
costructuredArrowDownwardsPrecomp_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CostructuredArrowDownwards CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow structuredArrowDownwards costructuredArrowDownwardsPrecomp CategoryTheory.CostructuredArrow.homMk CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.StructuredArrow.homMk CategoryTheory.CommaMorphism.left	—	—
costructuredArrowDownwardsPrecomp_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CostructuredArrowDownwards CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow structuredArrowDownwards costructuredArrowDownwardsPrecomp CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right	—	—
costructuredArrowRightwards_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CategoryTheory.Comma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.commaCategory CategoryTheory.CostructuredArrow.pre CategoryTheory.Comma.mapLeft CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CostructuredArrow.homMk CategoryTheory.CommaMorphism.left	—	—
costructuredArrowRightwards_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow costructuredArrowRightwards CategoryTheory.Comma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.commaCategory CategoryTheory.CostructuredArrow.pre CategoryTheory.Comma.mapLeft CategoryTheory.Comma.left CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
equivalenceJ_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso StructuredArrowRightwards CostructuredArrowDownwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards equivalenceJ CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp EquivalenceJ.inverse EquivalenceJ.functor	—	—
equivalenceJ_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor StructuredArrowRightwards CostructuredArrowDownwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards equivalenceJ EquivalenceJ.functor	—	—
equivalenceJ_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse StructuredArrowRightwards CostructuredArrowDownwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards equivalenceJ EquivalenceJ.inverse	—	—
equivalenceJ_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso StructuredArrowRightwards CostructuredArrowDownwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards equivalenceJ CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
guitartExact_id 📖	mathematical	—	GuitartExact CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	guitartExact_iff_isConnected_rightwards CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.CostructuredArrow.w CategoryTheory.zigzag_isConnected CategoryTheory.Zigzag.of_inv_hom
guitartExact_iff_final 📖	mathematical	—	GuitartExact CategoryTheory.Functor.Final CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards	—	instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact CategoryTheory.Functor.Final.out
guitartExact_iff_initial 📖	mathematical	—	GuitartExact CategoryTheory.Functor.Initial CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj structuredArrowDownwards	—	instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact guitartExact_iff_isConnected_downwards CategoryTheory.Functor.Initial.out
guitartExact_iff_isConnected_downwards 📖	mathematical	—	GuitartExact CategoryTheory.IsConnected CostructuredArrowDownwards CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj structuredArrowDownwards	—	—
guitartExact_iff_isConnected_rightwards 📖	mathematical	—	GuitartExact CategoryTheory.IsConnected StructuredArrowRightwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards	—	GuitartExact.isConnected_rightwards
guitartExact_of_isEquivalence_of_isIso 📖	mathematical	—	GuitartExact	—	guitartExact_iff_initial CategoryTheory.StructuredArrow.isEquivalence_post CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.StructuredArrow.isEquivalence_pre CategoryTheory.Functor.initial_comp CategoryTheory.Functor.initial_of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence
instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards	—	guitartExact_iff_final
instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact 📖	mathematical	—	CategoryTheory.Functor.Initial CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj structuredArrowDownwards	—	guitartExact_iff_initial
instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.CostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj structuredArrowDownwards CategoryTheory.instCategoryCostructuredArrow	—	guitartExact_iff_isConnected_downwards
instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.StructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CategoryTheory.instCategoryStructuredArrow	—	guitartExact_iff_isConnected_rightwards
isConnected_rightwards_iff_downwards 📖	mathematical	—	CategoryTheory.IsConnected StructuredArrowRightwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj costructuredArrowRightwards CostructuredArrowDownwards CategoryTheory.StructuredArrow structuredArrowDownwards	—	CategoryTheory.isConnected_iff_of_equivalence
structuredArrowDownwards_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj structuredArrowDownwards CategoryTheory.Comma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.commaCategory CategoryTheory.StructuredArrow.pre CategoryTheory.Comma.mapRight CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.StructuredArrow.homMk CategoryTheory.CommaMorphism.right	—	—
structuredArrowDownwards_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow structuredArrowDownwards CategoryTheory.Comma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.commaCategory CategoryTheory.StructuredArrow.pre CategoryTheory.Comma.mapRight CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—

CategoryTheory.TwoSquare.CostructuredArrowDownwards

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_surjective 📖	—	—	—	—	CategoryTheory.CostructuredArrow.mk_surjective CategoryTheory.StructuredArrow.mk_surjective CategoryTheory.StructuredArrow.homMk_surjective CategoryTheory.Category.assoc

CategoryTheory.TwoSquare.EquivalenceJ

Definitions

Name	Category	Theorems
functor 📖	CompOp	4 math math: CategoryTheory.TwoSquare.equivalenceJ_counitIso, functor_obj, functor_map, CategoryTheory.TwoSquare.equivalenceJ_functor
inverse 📖	CompOp	4 math math: inverse_map, CategoryTheory.TwoSquare.equivalenceJ_counitIso, CategoryTheory.TwoSquare.equivalenceJ_inverse, inverse_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.CostructuredArrowDownwards CategoryTheory.StructuredArrow CategoryTheory.TwoSquare.structuredArrowDownwards functor CategoryTheory.CostructuredArrow.homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Comma.mapLeft CategoryTheory.CostructuredArrow.post CategoryTheory.Comma.right CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom CategoryTheory.StructuredArrow.homMk CategoryTheory.CommaMorphism.right	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.CostructuredArrowDownwards CategoryTheory.StructuredArrow CategoryTheory.TwoSquare.structuredArrowDownwards functor CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Comma.mapLeft CategoryTheory.CostructuredArrow.post CategoryTheory.Comma.right CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom CategoryTheory.StructuredArrow.homMk	—	—
inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.TwoSquare.CostructuredArrowDownwards CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.structuredArrowDownwards CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.CostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards inverse CategoryTheory.StructuredArrow.homMk CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Comma.mapRight CategoryTheory.StructuredArrow.post CategoryTheory.Comma.left CategoryTheory.CommaMorphism.right CategoryTheory.Comma.hom CategoryTheory.CostructuredArrow.homMk CategoryTheory.CommaMorphism.left	—	—
inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.TwoSquare.CostructuredArrowDownwards CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.TwoSquare.structuredArrowDownwards CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.CostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards inverse CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Comma.mapRight CategoryTheory.StructuredArrow.post CategoryTheory.Comma.left CategoryTheory.CommaMorphism.right CategoryTheory.Comma.hom CategoryTheory.CostructuredArrow.homMk	—	—

CategoryTheory.TwoSquare.GuitartExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_rightwards 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.costructuredArrowRightwards	—	—

CategoryTheory.TwoSquare.StructuredArrowRightwards

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_surjective 📖	—	—	—	—	CategoryTheory.StructuredArrow.mk_surjective CategoryTheory.CostructuredArrow.mk_surjective CategoryTheory.CostructuredArrow.homMk_surjective

---

← Back to Index