Adjunction

📁 Source: Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

Statistics

Metric	Count
Definitions colimitIsoColimitGrothendieck, isPointwiseLeftKanExtensionLeftKanExtensionUnit, isPointwiseRightKanExtensionRanCounit, lan, lanAdjunction, lanCompColimIso, lanUnit, leftKanExtensionIsoFiberwiseColimit, leftKanExtensionObjIsoColimit, ran, ranAdjunction, ranCompLimIso, ranCounit, ranObjObjIsoLimit	14
Theorems coreflective, coreflective', hasColimit_map_comp_ι_comp_grothendieckProj, instHasColimitGrothendieckFunctorCompGrothendieckProj, instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension, instIsIsoAppLanUnit, instIsIsoAppLanUnit_1, instIsIsoAppRanCounit, instIsIsoAppRanCounit_1, instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension, instIsLeftKanExtensionObjLanAppLanUnit, instIsRightKanExtensionObjRanAppRanCounit, isIso_lanAdjunction_counit_app_iff, isIso_lanAdjunction_homEquiv_symm_iff, isIso_ranAdjunction_homEquiv_iff, isIso_ranAdjunction_unit_app_iff, lanAdjunction_counit_app, lanAdjunction_unit, lanCompColimIso_hom_app, lanCompColimIso_inv_app, lanUnit_app_app_lanAdjunction_counit_app_app, lanUnit_app_app_lanAdjunction_counit_app_app_assoc, lanUnit_app_whiskerLeft_lanAdjunction_counit_app, lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, leftKanExtensionIsoFiberwiseColimit_hom_app, leftKanExtensionIsoFiberwiseColimit_inv_app, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, ranAdjunction_counit, ranAdjunction_unit_app, ranCompLimIso_hom_app, ranCompLimIso_inv_app, ranCounit_app_app_ranAdjunction_unit_app_app, ranCounit_app_app_ranAdjunction_unit_app_app_assoc, ranCounit_app_whiskerLeft_ranAdjunction_unit_app, ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, ranObjObjIsoLimit_hom_π, ranObjObjIsoLimit_hom_π_assoc, ranObjObjIsoLimit_inv_π, ranObjObjIsoLimit_inv_π_assoc, reflective, reflective', ι_colimitIsoColimitGrothendieck_hom, ι_colimitIsoColimitGrothendieck_hom_assoc, ι_colimitIsoColimitGrothendieck_inv, ι_colimitIsoColimitGrothendieck_inv_assoc, ι_leftKanExtensionObjIsoColimit_hom, ι_leftKanExtensionObjIsoColimit_hom_assoc, ι_leftKanExtensionObjIsoColimit_inv, ι_leftKanExtensionObjIsoColimit_inv_assoc	51
Total	65

CategoryTheory.Functor

Definitions

Name	Category	Theorems
colimitIsoColimitGrothendieck 📖	CompOp	4 math math: ι_colimitIsoColimitGrothendieck_inv_assoc, ι_colimitIsoColimitGrothendieck_hom, ι_colimitIsoColimitGrothendieck_hom_assoc, ι_colimitIsoColimitGrothendieck_inv
isPointwiseLeftKanExtensionLeftKanExtensionUnit 📖	CompOp	—
isPointwiseRightKanExtensionRanCounit 📖	CompOp	—
lan 📖	CompOp	30 math math: CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits, CategoryTheory.lan_preservesFiniteLimits_of_flat, instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension, CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans_app_uliftYoneda_obj, instIsLeftKanExtensionObjLanAppLanUnit, lanUnit_app_app_lanAdjunction_counit_app_app, lanUnit_app_whiskerLeft_lanAdjunction_counit_app, instIsIsoAppLanUnit, CategoryTheory.TwoSquare.isIso_lanBaseChange_app, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, lanCompColimIso_inv_app, CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits, CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff, CategoryTheory.TwoSquare.instIsIsoFunctorLanBaseChangeOfGuitartExact, lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, isIso_lanAdjunction_homEquiv_symm_iff, lanAdjunction_unit, lanCompIsoOfPreserves_inv_app, CategoryTheory.flat_iff_lan_flat, CategoryTheory.lan_flat_of_flat, lanCompIsoOfPreserves_hom_app, instIsIsoAppLanUnit_1, coreflective', CategoryTheory.TwoSquare.lanBaseChange_app, lanAdjunction_counit_app, isIso_lanAdjunction_counit_app_iff, coreflective, lanUnit_app_app_lanAdjunction_counit_app_app_assoc, lanCompColimIso_hom_app
lanAdjunction 📖	CompOp	11 math math: instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension, lanUnit_app_app_lanAdjunction_counit_app_app, lanUnit_app_whiskerLeft_lanAdjunction_counit_app, lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, isIso_lanAdjunction_homEquiv_symm_iff, lanAdjunction_unit, coreflective', CategoryTheory.TwoSquare.lanBaseChange_app, lanAdjunction_counit_app, isIso_lanAdjunction_counit_app_iff, lanUnit_app_app_lanAdjunction_counit_app_app_assoc
lanCompColimIso 📖	CompOp	2 math math: lanCompColimIso_inv_app, lanCompColimIso_hom_app
lanUnit 📖	CompOp	15 math math: instIsLeftKanExtensionObjLanAppLanUnit, lanUnit_app_app_lanAdjunction_counit_app_app, lanUnit_app_whiskerLeft_lanAdjunction_counit_app, instIsIsoAppLanUnit, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, lanCompColimIso_inv_app, CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff, lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, lanAdjunction_unit, instIsIsoAppLanUnit_1, CategoryTheory.TwoSquare.lanBaseChange_app, lanAdjunction_counit_app, coreflective, lanUnit_app_app_lanAdjunction_counit_app_app_assoc, lanCompColimIso_hom_app
leftKanExtensionIsoFiberwiseColimit 📖	CompOp	2 math math: leftKanExtensionIsoFiberwiseColimit_hom_app, leftKanExtensionIsoFiberwiseColimit_inv_app
leftKanExtensionObjIsoColimit 📖	CompOp	9 math math: leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, ι_leftKanExtensionObjIsoColimit_inv, ι_leftKanExtensionObjIsoColimit_inv_assoc, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, leftKanExtensionIsoFiberwiseColimit_hom_app, ι_leftKanExtensionObjIsoColimit_hom, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, ι_leftKanExtensionObjIsoColimit_hom_assoc, leftKanExtensionIsoFiberwiseColimit_inv_app
ran 📖	CompOp	29 math math: instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension, CategoryTheory.ran_isSheaf_of_isCocontinuous, instIsIsoAppRanCounit, reflective', ranCompLimIso_inv_app, sheafAdjunctionCocontinuous_counit_app_val, ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, ranCompIsoOfPreserves_inv_app, ranCompIsoOfPreserves_hom_app, isIso_ranAdjunction_unit_app_iff, ranObjObjIsoLimit_inv_π_assoc, isIso_ranAdjunction_homEquiv_iff, ranCounit_app_app_ranAdjunction_unit_app_app_assoc, sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, ranObjObjIsoLimit_hom_π_assoc, instIsRightKanExtensionObjRanAppRanCounit, sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, ranCounit_app_app_ranAdjunction_unit_app_app, reflective, ranObjObjIsoLimit_hom_π, ranObjObjIsoLimit_inv_π, ranAdjunction_counit, ranCounit_app_whiskerLeft_ranAdjunction_unit_app, IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, ranCompLimIso_hom_app, sheafAdjunctionCocontinuous_homEquiv_apply_val, ranAdjunction_unit_app, sheafAdjunctionCocontinuous_unit_app_val, instIsIsoAppRanCounit_1
ranAdjunction 📖	CompOp	13 math math: instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension, reflective', sheafAdjunctionCocontinuous_counit_app_val, ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, isIso_ranAdjunction_unit_app_iff, isIso_ranAdjunction_homEquiv_iff, ranCounit_app_app_ranAdjunction_unit_app_app_assoc, ranCounit_app_app_ranAdjunction_unit_app_app, ranAdjunction_counit, ranCounit_app_whiskerLeft_ranAdjunction_unit_app, sheafAdjunctionCocontinuous_homEquiv_apply_val, ranAdjunction_unit_app, sheafAdjunctionCocontinuous_unit_app_val
ranCompLimIso 📖	CompOp	2 math math: ranCompLimIso_inv_app, ranCompLimIso_hom_app
ranCounit 📖	CompOp	17 math math: instIsIsoAppRanCounit, ranCompLimIso_inv_app, ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, ranObjObjIsoLimit_inv_π_assoc, ranCounit_app_app_ranAdjunction_unit_app_app_assoc, ranObjObjIsoLimit_hom_π_assoc, instIsRightKanExtensionObjRanAppRanCounit, ranCounit_app_app_ranAdjunction_unit_app_app, reflective, ranObjObjIsoLimit_hom_π, ranObjObjIsoLimit_inv_π, ranAdjunction_counit, ranCounit_app_whiskerLeft_ranAdjunction_unit_app, IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, ranCompLimIso_hom_app, ranAdjunction_unit_app, instIsIsoAppRanCounit_1
ranObjObjIsoLimit 📖	CompOp	4 math math: ranObjObjIsoLimit_inv_π_assoc, ranObjObjIsoLimit_hom_π_assoc, ranObjObjIsoLimit_hom_π, ranObjObjIsoLimit_inv_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreflective 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category id comp lan instHasLeftKanExtension obj whiskeringLeft lanUnit	—	CategoryTheory.NatIso.isIso_of_isIso_app instHasLeftKanExtension instIsIsoAppLanUnit_1
coreflective' 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category id comp lan instHasLeftKanExtension obj whiskeringLeft CategoryTheory.Adjunction.unit lanAdjunction	—	CategoryTheory.NatIso.isIso_of_isIso_app instHasLeftKanExtension instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension
hasColimit_map_comp_ι_comp_grothendieckProj 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.Limits.HasColimit CategoryTheory.Bundled.α CategoryTheory.Category obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.CostructuredArrow.functor CategoryTheory.Cat.str comp CategoryTheory.Cat.Hom.toFunctor map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.CostructuredArrow.grothendieckProj	—	CategoryTheory.Limits.hasColimit_of_iso
instHasColimitGrothendieckFunctorCompGrothendieckProj 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.Limits.HasColimit CategoryTheory.Grothendieck CategoryTheory.CostructuredArrow.functor CategoryTheory.Grothendieck.instCategory comp CategoryTheory.CostructuredArrow.grothendieckProj	—	CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit hasColimit_map_comp_ι_comp_grothendieckProj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension 📖	mathematical	HasPointwiseRightKanExtension HasRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj comp ran whiskeringLeft id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit ranAdjunction	—	ranAdjunction_counit instIsIsoAppRanCounit_1
instIsIsoAppLanUnit 📖	mathematical	HasPointwiseLeftKanExtension HasLeftKanExtension	CategoryTheory.IsIso obj CategoryTheory.Functor category id comp lan whiskeringLeft CategoryTheory.NatTrans.app lanUnit	—	LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app instHasLeftKanExtension
instIsIsoAppLanUnit_1 📖	mathematical	HasPointwiseLeftKanExtension HasLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj id comp lan whiskeringLeft CategoryTheory.NatTrans.app lanUnit	—	CategoryTheory.NatIso.isIso_of_isIso_app instIsIsoAppLanUnit
instIsIsoAppRanCounit 📖	mathematical	HasPointwiseRightKanExtension HasRightKanExtension	CategoryTheory.IsIso obj CategoryTheory.Functor category comp ran whiskeringLeft id CategoryTheory.NatTrans.app ranCounit	—	RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app
instIsIsoAppRanCounit_1 📖	mathematical	HasPointwiseRightKanExtension HasRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj comp ran whiskeringLeft id CategoryTheory.NatTrans.app ranCounit	—	CategoryTheory.NatIso.isIso_of_isIso_app instIsIsoAppRanCounit
instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension 📖	mathematical	HasPointwiseLeftKanExtension HasLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj id comp lan whiskeringLeft CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit lanAdjunction	—	lanAdjunction_unit instIsIsoAppLanUnit_1
instIsLeftKanExtensionObjLanAppLanUnit 📖	mathematical	HasLeftKanExtension	IsLeftKanExtension obj CategoryTheory.Functor category lan id CategoryTheory.NatTrans.app comp whiskeringLeft lanUnit	—	instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit
instIsRightKanExtensionObjRanAppRanCounit 📖	mathematical	HasRightKanExtension	IsRightKanExtension obj CategoryTheory.Functor category ran id CategoryTheory.NatTrans.app comp whiskeringLeft ranCounit	—	instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit
isIso_lanAdjunction_counit_app_iff 📖	mathematical	HasLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj comp whiskeringLeft lan id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit lanAdjunction IsLeftKanExtension CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isLeftKanExtension_iff_isIso lanUnit_app_whiskerLeft_lanAdjunction_counit_app instIsLeftKanExtensionObjLanAppLanUnit
isIso_lanAdjunction_homEquiv_symm_iff 📖	mathematical	HasLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj lan DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct whiskeringLeft EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv lanAdjunction IsLeftKanExtension	—	isLeftKanExtension_iff_isIso instIsLeftKanExtensionObjLanAppLanUnit CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv descOfIsLeftKanExtension_fac
isIso_ranAdjunction_homEquiv_iff 📖	mathematical	HasRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj ran DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct whiskeringLeft EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv ranAdjunction IsRightKanExtension	—	isRightKanExtension_iff_isIso instIsRightKanExtensionObjRanAppRanCounit CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv liftOfIsRightKanExtension_fac
isIso_ranAdjunction_unit_app_iff 📖	mathematical	HasRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category obj id comp whiskeringLeft ran CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit ranAdjunction IsRightKanExtension CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isRightKanExtension_iff_isIso ranCounit_app_whiskerLeft_ranAdjunction_unit_app instIsRightKanExtensionObjRanAppRanCounit
lanAdjunction_counit_app 📖	mathematical	HasLeftKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp obj whiskeringLeft lan id CategoryTheory.Adjunction.counit lanAdjunction descOfIsLeftKanExtension lanUnit instIsLeftKanExtensionObjLanAppLanUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
lanAdjunction_unit 📖	mathematical	HasLeftKanExtension	CategoryTheory.Adjunction.unit CategoryTheory.Functor category lan obj whiskeringLeft lanAdjunction lanUnit	—	CategoryTheory.NatTrans.ext' CategoryTheory.Category.comp_id
lanCompColimIso_hom_app 📖	mathematical	HasLeftKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp lan CategoryTheory.Limits.colim CategoryTheory.Iso.hom lanCompColimIso CategoryTheory.Limits.colimit obj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape colimitIsoOfIsLeftKanExtension id whiskeringLeft lanUnit instIsLeftKanExtensionObjLanAppLanUnit	—	—
lanCompColimIso_inv_app 📖	mathematical	HasLeftKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category CategoryTheory.Limits.colim comp lan CategoryTheory.Iso.inv lanCompColimIso CategoryTheory.Limits.colimit obj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape colimitIsoOfIsLeftKanExtension id whiskeringLeft lanUnit instIsLeftKanExtensionObjLanAppLanUnit	—	—
lanUnit_app_app_lanAdjunction_counit_app_app 📖	mathematical	HasLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor category id comp lan whiskeringLeft CategoryTheory.NatTrans.app lanUnit CategoryTheory.Adjunction.counit lanAdjunction CategoryTheory.CategoryStruct.id	—	CategoryTheory.congr_app lanUnit_app_whiskerLeft_lanAdjunction_counit_app
lanUnit_app_app_lanAdjunction_counit_app_app_assoc 📖	mathematical	HasLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor category whiskeringLeft lan comp CategoryTheory.NatTrans.app id lanUnit CategoryTheory.Adjunction.counit lanAdjunction	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' lanUnit_app_app_lanAdjunction_counit_app_app
lanUnit_app_whiskerLeft_lanAdjunction_counit_app 📖	mathematical	HasLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category obj id comp lan whiskeringLeft CategoryTheory.NatTrans.app lanUnit whiskerLeft CategoryTheory.Adjunction.counit lanAdjunction CategoryTheory.CategoryStruct.id	—	descOfIsLeftKanExtension_fac instIsLeftKanExtensionObjLanAppLanUnit
lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc 📖	mathematical	HasLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp obj whiskeringLeft lan CategoryTheory.NatTrans.app id lanUnit whiskerLeft CategoryTheory.Adjunction.counit lanAdjunction	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' lanUnit_app_whiskerLeft_lanAdjunction_counit_app
leftKanExtensionIsoFiberwiseColimit_hom_app 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.NatTrans.app leftKanExtension CategoryTheory.Limits.fiberwiseColimit CategoryTheory.CostructuredArrow.functor comp CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.CostructuredArrow.grothendieckProj hasColimit_map_comp_ι_comp_grothendieckProj CategoryTheory.Iso.hom CategoryTheory.Functor category leftKanExtensionIsoFiberwiseColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Grothendieck.ι CategoryTheory.Limits.hasColimit_ι_comp leftKanExtensionObjIsoColimit CategoryTheory.Iso.inv CategoryTheory.Limits.HasColimit.isoOfNatIso isoWhiskerRight CategoryTheory.CostructuredArrow.ιCompGrothendieckProj	—	hasColimit_map_comp_ι_comp_grothendieckProj
leftKanExtensionIsoFiberwiseColimit_inv_app 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Limits.fiberwiseColimit CategoryTheory.CostructuredArrow.functor comp CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.CostructuredArrow.grothendieckProj hasColimit_map_comp_ι_comp_grothendieckProj leftKanExtension CategoryTheory.Iso.inv CategoryTheory.Functor category leftKanExtensionIsoFiberwiseColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Grothendieck.ι CategoryTheory.Limits.hasColimit_ι_comp CategoryTheory.CostructuredArrow.proj obj CategoryTheory.Iso.hom CategoryTheory.Limits.HasColimit.isoOfNatIso isoWhiskerRight CategoryTheory.CostructuredArrow.ιCompGrothendieckProj leftKanExtensionObjIsoColimit	—	hasColimit_map_comp_ι_comp_grothendieckProj
leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp leftKanExtension instHasLeftKanExtension CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.NatTrans.app leftKanExtensionUnit CategoryTheory.Iso.hom leftKanExtensionObjIsoColimit CategoryTheory.Limits.colimit.ι CategoryTheory.CategoryStruct.id	—	instHasLeftKanExtension map_id CategoryTheory.Category.id_comp leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom
leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftKanExtension instHasLeftKanExtension CategoryTheory.NatTrans.app comp leftKanExtensionUnit CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.hom leftKanExtensionObjIsoColimit CategoryTheory.Limits.colimit.ι CategoryTheory.CategoryStruct.id	—	instHasLeftKanExtension CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom
leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit comp leftKanExtension instHasLeftKanExtension CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.NatTrans.app leftKanExtensionUnit CategoryTheory.Comma.right map CategoryTheory.Comma.hom CategoryTheory.Iso.hom leftKanExtensionObjIsoColimit CategoryTheory.Limits.colimit.ι	—	LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom instHasLeftKanExtension
ranAdjunction_counit 📖	mathematical	HasRightKanExtension	CategoryTheory.Adjunction.counit CategoryTheory.Functor category obj whiskeringLeft ran ranAdjunction ranCounit	—	CategoryTheory.NatTrans.ext' CategoryTheory.Category.id_comp
ranAdjunction_unit_app 📖	mathematical	HasRightKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category id comp obj whiskeringLeft ran CategoryTheory.Adjunction.unit ranAdjunction liftOfIsRightKanExtension ranCounit instIsRightKanExtensionObjRanAppRanCounit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ranCompLimIso_hom_app 📖	mathematical	HasRightKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category comp ran CategoryTheory.Limits.lim CategoryTheory.Iso.hom ranCompLimIso CategoryTheory.Limits.limit obj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape limitIsoOfIsRightKanExtension whiskeringLeft id ranCounit instIsRightKanExtensionObjRanAppRanCounit	—	—
ranCompLimIso_inv_app 📖	mathematical	HasRightKanExtension	CategoryTheory.NatTrans.app CategoryTheory.Functor category CategoryTheory.Limits.lim comp ran CategoryTheory.Iso.inv ranCompLimIso CategoryTheory.Limits.limit obj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape limitIsoOfIsRightKanExtension whiskeringLeft id ranCounit instIsRightKanExtensionObjRanAppRanCounit	—	—
ranCounit_app_app_ranAdjunction_unit_app_app 📖	mathematical	HasRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor category id comp whiskeringLeft ran CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit ranAdjunction ranCounit CategoryTheory.CategoryStruct.id	—	CategoryTheory.congr_app ranCounit_app_whiskerLeft_ranAdjunction_unit_app
ranCounit_app_app_ranAdjunction_unit_app_app_assoc 📖	mathematical	HasRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor category ran whiskeringLeft CategoryTheory.NatTrans.app id comp CategoryTheory.Adjunction.unit ranAdjunction ranCounit	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ranCounit_app_app_ranAdjunction_unit_app_app
ranCounit_app_whiskerLeft_ranAdjunction_unit_app 📖	mathematical	HasRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp obj id whiskeringLeft ran whiskerLeft CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit ranAdjunction ranCounit CategoryTheory.CategoryStruct.id	—	liftOfIsRightKanExtension_fac instIsRightKanExtensionObjRanAppRanCounit
ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc 📖	mathematical	HasRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp obj ran whiskeringLeft whiskerLeft CategoryTheory.NatTrans.app id CategoryTheory.Adjunction.unit ranAdjunction ranCounit	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ranCounit_app_whiskerLeft_ranAdjunction_unit_app
ranObjObjIsoLimit_hom_π 📖	mathematical	HasRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor category ran CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj CategoryTheory.Iso.hom ranObjObjIsoLimit CategoryTheory.Limits.limit.π CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right id map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app whiskeringLeft ranCounit	—	RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π
ranObjObjIsoLimit_hom_π_assoc 📖	mathematical	HasRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor category ran CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj CategoryTheory.Iso.hom ranObjObjIsoLimit CategoryTheory.Limits.limit.π CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit map CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.NatTrans.app whiskeringLeft id ranCounit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ranObjObjIsoLimit_hom_π
ranObjObjIsoLimit_inv_π 📖	mathematical	HasRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj obj CategoryTheory.Functor category ran id CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit CategoryTheory.Iso.inv ranObjObjIsoLimit map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app whiskeringLeft ranCounit CategoryTheory.Limits.limit.π	—	RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π
ranObjObjIsoLimit_inv_π_assoc 📖	mathematical	HasRightKanExtension HasPointwiseRightKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow comp CategoryTheory.StructuredArrow.proj obj CategoryTheory.Functor category ran CategoryTheory.Iso.inv ranObjObjIsoLimit CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app whiskeringLeft id ranCounit CategoryTheory.Limits.limit.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ranObjObjIsoLimit_inv_π
reflective 📖	mathematical	HasPointwiseRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category comp ran instHasRightKanExtension obj whiskeringLeft id ranCounit	—	CategoryTheory.NatIso.isIso_of_isIso_app instHasRightKanExtension instIsIsoAppRanCounit_1
reflective' 📖	mathematical	HasPointwiseRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor category comp ran instHasRightKanExtension obj whiskeringLeft id CategoryTheory.Adjunction.counit ranAdjunction	—	CategoryTheory.NatIso.isIso_of_isIso_app instHasRightKanExtension instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension
ι_colimitIsoColimitGrothendieck_hom 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Grothendieck CategoryTheory.CostructuredArrow.functor CategoryTheory.Grothendieck.instCategory comp CategoryTheory.CostructuredArrow.grothendieckProj instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.hom colimitIsoColimitGrothendieck CategoryTheory.CategoryStruct.id	—	instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Iso.eq_comp_inv ι_colimitIsoColimitGrothendieck_inv
ι_colimitIsoColimitGrothendieck_hom_assoc 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι CategoryTheory.Grothendieck CategoryTheory.CostructuredArrow.functor CategoryTheory.Grothendieck.instCategory comp CategoryTheory.CostructuredArrow.grothendieckProj instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Iso.hom colimitIsoColimitGrothendieck CategoryTheory.CategoryStruct.id	—	instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitIsoColimitGrothendieck_hom
ι_colimitIsoColimitGrothendieck_inv 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Grothendieck CategoryTheory.CostructuredArrow.functor CategoryTheory.Grothendieck.instCategory comp CategoryTheory.CostructuredArrow.grothendieckProj CategoryTheory.Limits.colimit instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv colimitIsoColimitGrothendieck CategoryTheory.CostructuredArrow CategoryTheory.Grothendieck.base CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Grothendieck.fiber	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Limits.hasColimit_ι_comp hasColimit_map_comp_ι_comp_grothendieckProj instHasLeftKanExtension CategoryTheory.Iso.trans_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv_assoc CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc map_id ι_leftKanExtensionObjIsoColimit_inv_assoc CategoryTheory.Limits.colimit.w_assoc ι_colimitIsoOfIsLeftKanExtension_hom CategoryTheory.Category.id_comp
ι_colimitIsoColimitGrothendieck_inv_assoc 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Grothendieck CategoryTheory.CostructuredArrow.functor CategoryTheory.Grothendieck.instCategory CategoryTheory.CostructuredArrow.grothendieckProj CategoryTheory.Limits.colimit comp instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Limits.colimit.ι CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Iso.inv colimitIsoColimitGrothendieck CategoryTheory.CostructuredArrow CategoryTheory.Grothendieck.base CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Grothendieck.fiber	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitGrothendieckFunctorCompGrothendieckProj CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitIsoColimitGrothendieck_inv
ι_leftKanExtensionObjIsoColimit_hom 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit comp leftKanExtension instHasLeftKanExtension CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.NatTrans.app leftKanExtensionUnit CategoryTheory.Comma.right map CategoryTheory.Comma.hom CategoryTheory.Iso.hom leftKanExtensionObjIsoColimit CategoryTheory.Limits.colimit.ι	—	LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom instHasLeftKanExtension
ι_leftKanExtensionObjIsoColimit_hom_assoc 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit leftKanExtension instHasLeftKanExtension CategoryTheory.NatTrans.app comp leftKanExtensionUnit CategoryTheory.Comma.right map CategoryTheory.Comma.hom CategoryTheory.Limits.colimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.hom leftKanExtensionObjIsoColimit CategoryTheory.Limits.colimit.ι	—	instHasLeftKanExtension CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_leftKanExtensionObjIsoColimit_hom
ι_leftKanExtensionObjIsoColimit_inv 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.colimit leftKanExtension CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv leftKanExtensionObjIsoColimit CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit CategoryTheory.Comma.right CategoryTheory.NatTrans.app leftKanExtensionUnit map CategoryTheory.Comma.hom	—	instHasLeftKanExtension LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv
ι_leftKanExtensionObjIsoColimit_inv_assoc 📖	mathematical	HasPointwiseLeftKanExtension	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.colimit comp CategoryTheory.Limits.colimit.ι leftKanExtension CategoryTheory.Iso.inv leftKanExtensionObjIsoColimit CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory fromPUnit CategoryTheory.NatTrans.app leftKanExtensionUnit map CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_leftKanExtensionObjIsoColimit_inv

---

← Back to Index