Reflexive

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean

Statistics

Metric	Count
Definitions IsCoreflexivePair, IsReflexivePair, HasCoreflexiveEqualizers, HasReflexiveCoequalizers, ReflexiveCofork, isColimitEquiv, mk, toCofork, π, inclusionWalkingReflexivePair, WalkingReflexivePair, comp, category, instDecidableEqHom, decEq, colimitOfIsReflexivePairIsoCoequalizer, inclusionWalkingReflexivePairOfIsReflexivePairIso, instDecidableEqWalkingReflexivePair, instInhabitedWalkingReflexivePair, default, ofIsReflexivePair, reflexiveCoequalizerIsoCoequalizer, reflexiveCoforkEquivCofork, reflexiveCoforkEquivCoforkObjIso, reflexivePair, compRightIso, diagramIsoReflexivePair, mkNatIso, mkNatTrans, commonRetraction, commonSection, Reflexive	32
Theorems common_retraction, common_retraction', mk', swap, isReflexivePair, common_section, common_section', mk', swap, has_eq, has_coeq, app_one_eq_π, condition, mk_pt, mk_π, inclusionWalkingReflexivePair_final, inclusionWalkingReflexivePair_map, inclusionWalkingReflexivePair_obj, instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, id_eq, leftCompReflexion_eq, map_reflexion_comp_map_left, map_reflexion_comp_map_left_assoc, map_reflexion_comp_map_right, map_reflexion_comp_map_right_assoc, reflexion_comp_left, reflexion_comp_left_assoc, reflexion_comp_right, reflexion_comp_right_assoc, rightCompReflexion_eq, hasCoequalizer_of_common_section, hasCoreflexiveEqualizers_of_hasEqualizers, hasEqualizer_of_common_retraction, hasReflexiveCoequalizer_iff_hasCoequalizer, hasReflexiveCoequalizers_iff, hasReflexiveCoequalizers_of_hasCoequalizers, ofIsReflexivePair_hasColimit_of_hasCoequalizer, ofIsReflexivePair_map_left, ofIsReflexivePair_map_right, reflexiveCoforkEquivCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_π, reflexiveCoforkEquivCofork_inverse_obj_pt, reflexiveCoforkEquivCofork_inverse_obj_π, compRightIso_hom_app, compRightIso_inv_app, diagramIsoReflexivePair_hom_app, diagramIsoReflexivePair_inv_app, mkNatIso_hom_app, mkNatIso_inv_app, mkNatTrans_app_one, mkNatTrans_app_zero, to_isReflexivePair, whiskerRightMkNatTrans, reflexivePair_hasColimit_of_hasCoequalizer, reflexivePair_map_left, reflexivePair_map_reflexion, reflexivePair_map_right, reflexivePair_obj_one, reflexivePair_obj_zero, ι_colimitOfIsReflexivePairIsoCoequalizer_hom, ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc, ι_reflexiveCoequalizerIsoCoequalizer_hom, ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc, π_colimitOfIsReflexivePairIsoCoequalizer_inv, π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, π_reflexiveCoequalizerIsoCoequalizer_inv, π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, instIsReflexivePairMapAppCounitObj, left_comp_retraction, left_comp_retraction_assoc, right_comp_retraction, right_comp_retraction_assoc, section_comp_left, section_comp_left_assoc, section_comp_right, section_comp_right_assoc	77
Total	109

CategoryTheory

Definitions

Name	Category	Theorems
IsCoreflexivePair 📖	CompData	5 math math: Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap, IsCoreflexivePair.mk', IsCoreflexivePair.swap, Comonad.ComonadicityInternal.main_pair_coreflexive, LiftRightAdjoint.instIsCoreflexivePairMapAppUnitOtherMap
IsReflexivePair 📖	CompData	8 math math: IsKernelPair.isReflexivePair, Limits.reflexivePair.to_isReflexivePair, IsReflexivePair.mk', IsReflexivePair.swap, LiftLeftAdjoint.instIsReflexivePairMapAppCounitOtherMap, Monad.MonadicityInternal.main_pair_reflexive, instIsReflexivePairMapAppCounitObj, Monad.instIsReflexivePairAlgebraTopMapBottomMap
commonRetraction 📖	CompOp	4 math math: right_comp_retraction, left_comp_retraction, right_comp_retraction_assoc, left_comp_retraction_assoc
commonSection 📖	CompOp	4 math math: section_comp_left_assoc, section_comp_right, section_comp_left, section_comp_right_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsReflexivePairMapAppCounitObj 📖	mathematical	—	IsReflexivePair Functor.obj Functor.comp Functor.id Functor.map NatTrans.app Adjunction.counit	—	IsReflexivePair.mk' Functor.map_comp Adjunction.right_triangle_components Functor.map_id Adjunction.left_triangle_components
left_comp_retraction 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonRetraction CategoryStruct.id	—	IsCoreflexivePair.common_retraction
left_comp_retraction_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonRetraction	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' left_comp_retraction
right_comp_retraction 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonRetraction CategoryStruct.id	—	IsCoreflexivePair.common_retraction
right_comp_retraction_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonRetraction	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' right_comp_retraction
section_comp_left 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonSection CategoryStruct.id	—	IsReflexivePair.common_section
section_comp_left_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonSection	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' section_comp_left
section_comp_right 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonSection CategoryStruct.id	—	IsReflexivePair.common_section
section_comp_right_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct commonSection	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' section_comp_right

CategoryTheory.IsCoreflexivePair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
common_retraction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	common_retraction'
common_retraction' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mk' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.IsCoreflexivePair	—	—
swap 📖	mathematical	—	CategoryTheory.IsCoreflexivePair	—	mk' CategoryTheory.right_comp_retraction CategoryTheory.left_comp_retraction

CategoryTheory.IsKernelPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isReflexivePair 📖	mathematical	CategoryTheory.IsKernelPair	CategoryTheory.IsReflexivePair	—	CategoryTheory.IsReflexivePair.mk'

CategoryTheory.IsReflexivePair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
common_section 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	common_section'
common_section' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mk' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.IsReflexivePair	—	—
swap 📖	mathematical	—	CategoryTheory.IsReflexivePair	—	mk' CategoryTheory.section_comp_right CategoryTheory.section_comp_left

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasCoreflexiveEqualizers 📖	CompData	1 math math: hasCoreflexiveEqualizers_of_hasEqualizers
HasReflexiveCoequalizers 📖	CompData	2 math math: hasReflexiveCoequalizers_iff, hasReflexiveCoequalizers_of_hasCoequalizers
ReflexiveCofork 📖	CompOp	4 math math: reflexiveCoforkEquivCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_π, reflexiveCoforkEquivCofork_inverse_obj_pt, reflexiveCoforkEquivCofork_inverse_obj_π
WalkingReflexivePair 📖	CompData	46 math math: reflexivePair.diagramIsoReflexivePair_hom_app, ReflexiveCofork.app_one_eq_π, reflexivePair.to_isReflexivePair, WalkingReflexivePair.reflexion_comp_left, reflexivePair_obj_one, WalkingReflexivePair.leftCompReflexion_eq, WalkingParallelPair.inclusionWalkingReflexivePair_map, π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, hasReflexiveCoequalizer_iff_hasCoequalizer, ofIsReflexivePair_hasColimit_of_hasCoequalizer, reflexivePair.compRightIso_hom_app, WalkingReflexivePair.map_reflexion_comp_map_left, WalkingParallelPair.inclusionWalkingReflexivePair_obj, WalkingReflexivePair.Hom.id_eq, ReflexiveCofork.condition, WalkingReflexivePair.reflexion_comp_right, WalkingReflexivePair.reflexion_comp_left_assoc, reflexiveCoforkEquivCofork_functor_obj_pt, reflexivePair_map_left, WalkingReflexivePair.reflexion_comp_right_assoc, reflexivePair_map_right, reflexiveCoforkEquivCofork_functor_obj_π, reflexiveCoforkEquivCofork_inverse_obj_pt, reflexivePair.diagramIsoReflexivePair_inv_app, ι_colimitOfIsReflexivePairIsoCoequalizer_hom, hasReflexiveCoequalizers_iff, WalkingReflexivePair.rightCompReflexion_eq, reflexivePair_obj_zero, π_colimitOfIsReflexivePairIsoCoequalizer_inv, π_reflexiveCoequalizerIsoCoequalizer_inv, ι_reflexiveCoequalizerIsoCoequalizer_hom, reflexiveCoforkEquivCofork_inverse_obj_π, WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, reflexivePair_map_reflexion, reflexivePair.compRightIso_inv_app, WalkingParallelPair.inclusionWalkingReflexivePair_final, ofIsReflexivePair_map_left, π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, WalkingReflexivePair.map_reflexion_comp_map_left_assoc, ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc, WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, ofIsReflexivePair_map_right, WalkingReflexivePair.map_reflexion_comp_map_right, reflexivePair_hasColimit_of_hasCoequalizer, ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc, WalkingReflexivePair.map_reflexion_comp_map_right_assoc
colimitOfIsReflexivePairIsoCoequalizer 📖	CompOp	4 math math: ι_colimitOfIsReflexivePairIsoCoequalizer_hom, π_colimitOfIsReflexivePairIsoCoequalizer_inv, π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc
inclusionWalkingReflexivePairOfIsReflexivePairIso 📖	CompOp	—
instDecidableEqWalkingReflexivePair 📖	CompOp	—
instInhabitedWalkingReflexivePair 📖	CompOp	—
ofIsReflexivePair 📖	CompOp	7 math math: ofIsReflexivePair_hasColimit_of_hasCoequalizer, ι_colimitOfIsReflexivePairIsoCoequalizer_hom, π_colimitOfIsReflexivePairIsoCoequalizer_inv, ofIsReflexivePair_map_left, π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, ofIsReflexivePair_map_right, ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc
reflexiveCoequalizerIsoCoequalizer 📖	CompOp	4 math math: π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, π_reflexiveCoequalizerIsoCoequalizer_inv, ι_reflexiveCoequalizerIsoCoequalizer_hom, ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc
reflexiveCoforkEquivCofork 📖	CompOp	4 math math: reflexiveCoforkEquivCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_π, reflexiveCoforkEquivCofork_inverse_obj_pt, reflexiveCoforkEquivCofork_inverse_obj_π
reflexiveCoforkEquivCoforkObjIso 📖	CompOp	—
reflexivePair 📖	CompOp	9 math math: reflexivePair.diagramIsoReflexivePair_hom_app, reflexivePair_obj_one, reflexivePair.compRightIso_hom_app, reflexivePair_map_left, reflexivePair_map_right, reflexivePair.diagramIsoReflexivePair_inv_app, reflexivePair_obj_zero, reflexivePair_map_reflexion, reflexivePair.compRightIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCoequalizer_of_common_section 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	HasCoequalizer	—	HasReflexiveCoequalizers.has_coeq CategoryTheory.IsReflexivePair.mk'
hasCoreflexiveEqualizers_of_hasEqualizers 📖	mathematical	—	HasCoreflexiveEqualizers	—	hasLimitOfHasLimitsOfShape
hasEqualizer_of_common_retraction 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	HasEqualizer	—	HasCoreflexiveEqualizers.has_eq CategoryTheory.IsCoreflexivePair.mk'
hasReflexiveCoequalizer_iff_hasCoequalizer 📖	mathematical	—	HasColimit WalkingReflexivePair WalkingReflexivePair.category HasCoequalizer CategoryTheory.Functor.obj WalkingReflexivePair.one WalkingReflexivePair.zero CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right	—	CategoryTheory.Equivalence.hasInitial_iff
hasReflexiveCoequalizers_iff 📖	mathematical	—	HasColimitsOfShape WalkingReflexivePair WalkingReflexivePair.category HasReflexiveCoequalizers	—	CategoryTheory.section_comp_left CategoryTheory.section_comp_right hasReflexiveCoequalizer_iff_hasCoequalizer hasColimitOfHasColimitsOfShape reflexivePair_hasColimit_of_hasCoequalizer HasReflexiveCoequalizers.has_coeq reflexivePair.to_isReflexivePair
hasReflexiveCoequalizers_of_hasCoequalizers 📖	mathematical	—	HasReflexiveCoequalizers	—	hasColimitOfHasColimitsOfShape
ofIsReflexivePair_hasColimit_of_hasCoequalizer 📖	mathematical	—	HasColimit WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair	—	hasReflexiveCoequalizer_iff_hasCoequalizer
ofIsReflexivePair_map_left 📖	mathematical	—	CategoryTheory.Functor.map WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair WalkingReflexivePair.one WalkingReflexivePair.zero WalkingReflexivePair.Hom.left	—	—
ofIsReflexivePair_map_right 📖	mathematical	—	CategoryTheory.Functor.map WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair WalkingReflexivePair.one WalkingReflexivePair.zero WalkingReflexivePair.Hom.right	—	—
reflexiveCoforkEquivCofork_functor_obj_pt 📖	mathematical	—	Cocone.pt WalkingParallelPair walkingParallelPairHomCategory parallelPair CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.one WalkingReflexivePair.zero CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right Cocone Cocone.category Cofork CategoryTheory.Equivalence.functor ReflexiveCofork reflexiveCoforkEquivCofork	—	—
reflexiveCoforkEquivCofork_functor_obj_π 📖	mathematical	—	Cofork.π CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.one WalkingReflexivePair.zero CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right ReflexiveCofork Cocone.category Cofork WalkingParallelPair walkingParallelPairHomCategory parallelPair CategoryTheory.Equivalence.functor reflexiveCoforkEquivCofork ReflexiveCofork.π	—	ReflexiveCofork.π.eq_1 Cofork.π.eq_1 CategoryTheory.Category.id_comp
reflexiveCoforkEquivCofork_inverse_obj_pt 📖	mathematical	—	Cocone.pt WalkingReflexivePair WalkingReflexivePair.category CategoryTheory.Functor.obj Cofork WalkingReflexivePair.one WalkingReflexivePair.zero CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right Cocone.category WalkingParallelPair walkingParallelPairHomCategory parallelPair Cocone CategoryTheory.Equivalence.inverse ReflexiveCofork reflexiveCoforkEquivCofork	—	—
reflexiveCoforkEquivCofork_inverse_obj_π 📖	mathematical	—	ReflexiveCofork.π CategoryTheory.Functor.obj Cofork WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.one WalkingReflexivePair.zero CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right Cocone.category WalkingParallelPair walkingParallelPairHomCategory parallelPair ReflexiveCofork CategoryTheory.Equivalence.inverse reflexiveCoforkEquivCofork Cofork.π	—	WalkingParallelPair.inclusionWalkingReflexivePair_final CategoryTheory.Functor.Final.extendCocone_obj_ι_app' CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
reflexivePair_hasColimit_of_hasCoequalizer 📖	mathematical	—	HasColimit WalkingReflexivePair WalkingReflexivePair.category	—	hasReflexiveCoequalizer_iff_hasCoequalizer
reflexivePair_map_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.Functor.map WalkingReflexivePair WalkingReflexivePair.category reflexivePair WalkingReflexivePair.one WalkingReflexivePair.zero WalkingReflexivePair.Hom.right	—	—
reflexivePair_map_reflexion 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.Functor.map WalkingReflexivePair WalkingReflexivePair.category reflexivePair WalkingReflexivePair.zero WalkingReflexivePair.one WalkingReflexivePair.Hom.reflexion	—	—
reflexivePair_map_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.Functor.map WalkingReflexivePair WalkingReflexivePair.category reflexivePair WalkingReflexivePair.one WalkingReflexivePair.zero WalkingReflexivePair.Hom.left	—	—
reflexivePair_obj_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category reflexivePair WalkingReflexivePair.one	—	—
reflexivePair_obj_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category reflexivePair WalkingReflexivePair.zero	—	—
ι_colimitOfIsReflexivePairIsoCoequalizer_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair WalkingReflexivePair.zero colimit ofIsReflexivePair_hasColimit_of_hasCoequalizer coequalizer colimit.ι CategoryTheory.Iso.hom colimitOfIsReflexivePairIsoCoequalizer coequalizer.π	—	ι_reflexiveCoequalizerIsoCoequalizer_hom
ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair WalkingReflexivePair.zero colimit ofIsReflexivePair_hasColimit_of_hasCoequalizer colimit.ι coequalizer CategoryTheory.Iso.hom colimitOfIsReflexivePairIsoCoequalizer coequalizer.π	—	ofIsReflexivePair_hasColimit_of_hasCoequalizer CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitOfIsReflexivePairIsoCoequalizer_hom
ι_reflexiveCoequalizerIsoCoequalizer_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.zero colimit reflexivePair_hasColimit_of_hasCoequalizer coequalizer WalkingReflexivePair.one CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right colimit.ι CategoryTheory.Iso.hom reflexiveCoequalizerIsoCoequalizer coequalizer.π	—	IsColimit.comp_coconePointUniqueUpToIso_hom reflexivePair_hasColimit_of_hasCoequalizer
ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.zero colimit reflexivePair_hasColimit_of_hasCoequalizer colimit.ι coequalizer WalkingReflexivePair.one CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right CategoryTheory.Iso.hom reflexiveCoequalizerIsoCoequalizer coequalizer.π	—	reflexivePair_hasColimit_of_hasCoequalizer CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_reflexiveCoequalizerIsoCoequalizer_hom
π_colimitOfIsReflexivePairIsoCoequalizer_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct coequalizer colimit WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair ofIsReflexivePair_hasColimit_of_hasCoequalizer coequalizer.π CategoryTheory.Iso.inv colimitOfIsReflexivePairIsoCoequalizer colimit.ι WalkingReflexivePair.zero	—	π_reflexiveCoequalizerIsoCoequalizer_inv
π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct coequalizer coequalizer.π colimit WalkingReflexivePair WalkingReflexivePair.category ofIsReflexivePair ofIsReflexivePair_hasColimit_of_hasCoequalizer CategoryTheory.Iso.inv colimitOfIsReflexivePairIsoCoequalizer colimit.ι WalkingReflexivePair.zero	—	ofIsReflexivePair_hasColimit_of_hasCoequalizer CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_colimitOfIsReflexivePairIsoCoequalizer_inv
π_reflexiveCoequalizerIsoCoequalizer_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.zero coequalizer WalkingReflexivePair.one CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right colimit reflexivePair_hasColimit_of_hasCoequalizer coequalizer.π CategoryTheory.Iso.inv reflexiveCoequalizerIsoCoequalizer colimit.ι	—	reflexivePair_hasColimit_of_hasCoequalizer reflexiveCoequalizerIsoCoequalizer.eq_1 colimit.comp_coconePointUniqueUpToIso_inv
π_reflexiveCoequalizerIsoCoequalizer_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj WalkingReflexivePair WalkingReflexivePair.category WalkingReflexivePair.zero coequalizer WalkingReflexivePair.one CategoryTheory.Functor.map WalkingReflexivePair.Hom.left WalkingReflexivePair.Hom.right coequalizer.π colimit reflexivePair_hasColimit_of_hasCoequalizer CategoryTheory.Iso.inv reflexiveCoequalizerIsoCoequalizer colimit.ι	—	reflexivePair_hasColimit_of_hasCoequalizer CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_reflexiveCoequalizerIsoCoequalizer_inv

CategoryTheory.Limits.HasCoreflexiveEqualizers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_eq 📖	mathematical	—	CategoryTheory.Limits.HasEqualizer	—	—

CategoryTheory.Limits.HasReflexiveCoequalizers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_coeq 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizer	—	—

CategoryTheory.Limits.ReflexiveCofork

Definitions

Name	Category	Theorems
isColimitEquiv 📖	CompOp	—
mk 📖	CompOp	—
toCofork 📖	CompOp	—
π 📖	CompOp	5 math math: app_one_eq_π, condition, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_π, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_π, mk_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_one_eq_π 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingReflexivePair.zero π	—	—
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left π CategoryTheory.Limits.WalkingReflexivePair.Hom.right	—	CategoryTheory.Limits.Cocone.w
mk_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right	CategoryTheory.Limits.Cocone.pt	—	—
mk_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right	π	—	—

CategoryTheory.Limits.WalkingParallelPair

Definitions

Name	Category	Theorems
inclusionWalkingReflexivePair 📖	CompOp	5 math math: inclusionWalkingReflexivePair_map, inclusionWalkingReflexivePair_obj, instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, inclusionWalkingReflexivePair_final, instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inclusionWalkingReflexivePair_final 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category inclusionWalkingReflexivePair	—	instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair
inclusionWalkingReflexivePair_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category inclusionWalkingReflexivePair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.CategoryStruct.id	—	—
inclusionWalkingReflexivePair_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category inclusionWalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one	—	—
instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.StructuredArrow CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category inclusionWalkingReflexivePair CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.IsConnected.of_induct
instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair 📖	mathematical	—	CategoryTheory.StructuredArrow CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category inclusionWalkingReflexivePair	—	—

CategoryTheory.Limits.WalkingReflexivePair

Definitions

Name	Category	Theorems
category 📖	CompOp	46 math math: CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair_hom_app, CategoryTheory.Limits.ReflexiveCofork.app_one_eq_π, CategoryTheory.Limits.reflexivePair.to_isReflexivePair, reflexion_comp_left, CategoryTheory.Limits.reflexivePair_obj_one, leftCompReflexion_eq, CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_map, CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, CategoryTheory.Limits.hasReflexiveCoequalizer_iff_hasCoequalizer, CategoryTheory.Limits.ofIsReflexivePair_hasColimit_of_hasCoequalizer, CategoryTheory.Limits.reflexivePair.compRightIso_hom_app, map_reflexion_comp_map_left, CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_obj, Hom.id_eq, CategoryTheory.Limits.ReflexiveCofork.condition, reflexion_comp_right, reflexion_comp_left_assoc, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_pt, CategoryTheory.Limits.reflexivePair_map_left, reflexion_comp_right_assoc, CategoryTheory.Limits.reflexivePair_map_right, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_π, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_pt, CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair_inv_app, CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom, CategoryTheory.Limits.hasReflexiveCoequalizers_iff, rightCompReflexion_eq, CategoryTheory.Limits.reflexivePair_obj_zero, CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv, CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv, CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_π, CategoryTheory.Limits.WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, CategoryTheory.Limits.reflexivePair_map_reflexion, CategoryTheory.Limits.reflexivePair.compRightIso_inv_app, CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_final, CategoryTheory.Limits.ofIsReflexivePair_map_left, CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, map_reflexion_comp_map_left_assoc, CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc, CategoryTheory.Limits.WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, CategoryTheory.Limits.ofIsReflexivePair_map_right, map_reflexion_comp_map_right, CategoryTheory.Limits.reflexivePair_hasColimit_of_hasCoequalizer, CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc, map_reflexion_comp_map_right_assoc
instDecidableEqHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftCompReflexion_eq 📖	mathematical	—	Hom.leftCompReflexion CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct category one zero Hom.left Hom.reflexion	—	—
map_reflexion_comp_map_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair category zero one CategoryTheory.Functor.map Hom.reflexion Hom.left CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp reflexion_comp_left CategoryTheory.Functor.map_id
map_reflexion_comp_map_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair category zero one CategoryTheory.Functor.map Hom.reflexion Hom.left	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_reflexion_comp_map_left
map_reflexion_comp_map_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair category zero one CategoryTheory.Functor.map Hom.reflexion Hom.right CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp reflexion_comp_right CategoryTheory.Functor.map_id
map_reflexion_comp_map_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair category zero one CategoryTheory.Functor.map Hom.reflexion Hom.right	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_reflexion_comp_map_right
reflexion_comp_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct category zero one Hom.reflexion Hom.left CategoryTheory.CategoryStruct.id	—	—
reflexion_comp_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct category zero one Hom.reflexion Hom.left	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' reflexion_comp_left
reflexion_comp_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct category zero one Hom.reflexion Hom.right CategoryTheory.CategoryStruct.id	—	—
reflexion_comp_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct category zero one Hom.reflexion Hom.right	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' reflexion_comp_right
rightCompReflexion_eq 📖	mathematical	—	Hom.rightCompReflexion CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct category one zero Hom.right Hom.reflexion	—	—

CategoryTheory.Limits.WalkingReflexivePair.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id_eq 📖	mathematical	—	id CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.WalkingReflexivePair.category	—	—

CategoryTheory.Limits.WalkingReflexivePair.instDecidableEqHom

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

CategoryTheory.Limits.instInhabitedWalkingReflexivePair

Definitions

Name	Category	Theorems
default 📖	CompOp	—

CategoryTheory.Limits.reflexivePair

Definitions

Name	Category	Theorems
compRightIso 📖	CompOp	2 math math: compRightIso_hom_app, compRightIso_inv_app
diagramIsoReflexivePair 📖	CompOp	2 math math: diagramIsoReflexivePair_hom_app, diagramIsoReflexivePair_inv_app
mkNatIso 📖	CompOp	2 math math: mkNatIso_hom_app, mkNatIso_inv_app
mkNatTrans 📖	CompOp	3 math math: mkNatTrans_app_zero, mkNatTrans_app_one, whiskerRightMkNatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compRightIso_hom_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Functor.comp CategoryTheory.Limits.reflexivePair CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category compRightIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
compRightIso_inv_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.reflexivePair CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category compRightIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
diagramIsoReflexivePair_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.reflexivePair CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category diagramIsoReflexivePair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
diagramIsoReflexivePair_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.reflexivePair CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category diagramIsoReflexivePair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mkNatIso_hom_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Iso.hom CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category mkNatIso	—	—
mkNatIso_inv_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Iso.hom CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion	CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mkNatIso	—	—
mkNatTrans_app_one 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion	CategoryTheory.NatTrans.app mkNatTrans	—	—
mkNatTrans_app_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion	CategoryTheory.NatTrans.app mkNatTrans	—	—
to_isReflexivePair 📖	mathematical	—	CategoryTheory.IsReflexivePair CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right	—	CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_left CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_right
whiskerRightMkNatTrans 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingReflexivePair CategoryTheory.Limits.WalkingReflexivePair.category CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Functor.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left CategoryTheory.Limits.WalkingReflexivePair.Hom.right CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion	CategoryTheory.Functor.whiskerRight mkNatTrans CategoryTheory.Functor.comp	—	CategoryTheory.NatTrans.ext'

(root)

Definitions

Name	Category	Theorems
Reflexive 📖	MathDef	14 math math: Equivalence.reflexive, Sym2.diagSet_subset_fromRel, Std.Refl.reflexive, IsRefl.reflexive, Sym2.reflexive_iff_diagSet_subset_fromRel, Relation.reflexive_reflTransGen, reflexive_iff_subrelation_eq, CategoryTheory.Abelian.pseudoEqual_refl, AddSemiconjBy.reflexive, SemiconjBy.reflexive, reflexive_manyOneReducible, Relation.reflexive_reflGen, reflexive_oneOneReducible, FirstOrder.Language.Relations.realize_reflexive

---

← Back to Index