ChosenPullbacksAlong

📁 Source: Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean

Statistics

Metric	Count
Definitions ChosenPullbacks, ChosenPullbacksAlong, cartesianMonoidalCategoryFst, cartesianMonoidalCategorySnd, cartesianMonoidalCategoryToUnit, chosenPullbacksAlongFst, comp, fst, fst', id, isLimitPullbackCone, iso, isoInv, mapPullbackAdj, ofHasPullbacksAlong, pullback, pullbackComp, pullbackCone, pullbackId, pullbackIsoOverPullback, pullbackMap, pullbackObj, snd, snd'	24
Theorems cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app, cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, cartesianMonoidalCategoryFst_pullback_map, cartesianMonoidalCategoryFst_pullback_obj, cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app, cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, cartesianMonoidalCategorySnd_pullback_map, cartesianMonoidalCategorySnd_pullback_obj, cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, cartesianMonoidalCategoryToUnit_pullback_map, cartesianMonoidalCategoryToUnit_pullback_obj, condition, condition_assoc, fst'_left, hasPullbackAlong, hasPullbacks, hom_ext, hom_ext_iff, isPullback, isoInv_mapPullbackAdj_counit_app_left, isoInv_mapPullbackAdj_unit_app_left, isoInv_pullback_map_left, isoInv_pullback_obj_hom, isoInv_pullback_obj_left, isoInv_pullback_obj_right_as, iso_mapPullbackAdj_counit_app, iso_mapPullbackAdj_unit_app, iso_pullback_map, iso_pullback_obj, lift_fst, lift_fst_assoc, lift_snd, lift_snd_assoc, ofHasPullbacksAlong_mapPullbackAdj, ofHasPullbacksAlong_pullback, pullbackComp_hom_counit, pullbackComp_hom_counit_assoc, pullbackCone_fst, pullbackCone_snd, pullbackId_hom_counit, pullbackId_hom_counit_assoc, pullbackIsoOverPullback_hom_app_comp_fst, pullbackIsoOverPullback_hom_app_comp_fst_assoc, pullbackIsoOverPullback_hom_app_comp_snd, pullbackIsoOverPullback_hom_app_comp_snd_assoc, pullbackIsoOverPullback_inv_app_comp_fst, pullbackIsoOverPullback_inv_app_comp_fst_assoc, pullbackIsoOverPullback_inv_app_comp_snd, pullbackIsoOverPullback_inv_app_comp_snd_assoc, pullbackMap_comp, pullbackMap_comp_assoc, pullbackMap_fst, pullbackMap_fst_assoc, pullbackMap_id, pullbackMap_snd, pullbackMap_snd_assoc, snd'_left, unit_pullbackComp_hom, unit_pullbackComp_hom_assoc, unit_pullbackId_hom, unit_pullbackId_hom_app, unit_pullbackId_hom_app_assoc, unit_pullbackId_hom_assoc	64
Total	88

CategoryTheory

Definitions

Name	Category	Theorems
ChosenPullbacks 📖	CompOp	—
ChosenPullbacksAlong 📖	CompData	—

CategoryTheory.ChosenPullbacksAlong

Definitions

Name	Category	Theorems
cartesianMonoidalCategoryFst 📖	CompOp	4 math math: cartesianMonoidalCategoryFst_pullback_map, cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, cartesianMonoidalCategoryFst_pullback_obj, cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app
cartesianMonoidalCategorySnd 📖	CompOp	4 math math: cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, cartesianMonoidalCategorySnd_pullback_map, cartesianMonoidalCategorySnd_pullback_obj, cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app
cartesianMonoidalCategoryToUnit 📖	CompOp	6 math math: cartesianMonoidalCategoryToUnit_pullback_obj, cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, cartesianMonoidalCategoryToUnit_pullback_map, CategoryTheory.toOverUnitPullback_hom_app_left, CategoryTheory.toOverUnitPullback_inv_app_left
chosenPullbacksAlongFst 📖	CompOp	—
comp 📖	CompOp	4 math math: unit_pullbackComp_hom_assoc, pullbackComp_hom_counit, unit_pullbackComp_hom, pullbackComp_hom_counit_assoc
fst 📖	CompOp	34 math math: Over.whiskerLeft_left_fst, Over.associator_hom_left_snd_fst_assoc, Over.tensorHom_left_fst, hom_ext_iff, Over.tensorObj_ext_iff, Over.associator_hom_left_fst, isPullback, Over.associator_hom_left_snd_fst, condition_assoc, Over.leftUnitor_inv_left_fst_assoc, pullbackMap_fst_assoc, Over.leftUnitor_inv_left_fst, pullbackCone_fst, Over.whiskerRight_left_fst_assoc, lift_fst, pullbackMap_fst, pullbackIsoOverPullback_inv_app_comp_fst, Over.whiskerLeft_left_fst_assoc, Over.tensorHom_left_fst_assoc, Over.associator_inv_left_fst_snd_assoc, Over.associator_inv_left_fst_snd, Over.whiskerRight_left_fst, condition, Over.rightUnitor_hom_left, Over.associator_inv_left_fst_fst, fst'_left, pullbackIsoOverPullback_hom_app_comp_fst_assoc, pullbackIsoOverPullback_inv_app_comp_fst_assoc, pullbackIsoOverPullback_hom_app_comp_fst, Over.rightUnitor_inv_left_fst_assoc, Over.rightUnitor_inv_left_fst, lift_fst_assoc, Over.associator_hom_left_fst_assoc, Over.associator_inv_left_fst_fst_assoc
fst' 📖	CompOp	2 math math: fst'_left, Over.fst_eq_fst'
id 📖	CompOp	6 math math: unit_pullbackId_hom_app, pullbackId_hom_counit, pullbackId_hom_counit_assoc, unit_pullbackId_hom, unit_pullbackId_hom_app_assoc, unit_pullbackId_hom_assoc
isLimitPullbackCone 📖	CompOp	—
iso 📖	CompOp	4 math math: iso_mapPullbackAdj_unit_app, iso_pullback_obj, iso_mapPullbackAdj_counit_app, iso_pullback_map
isoInv 📖	CompOp	6 math math: isoInv_pullback_obj_left, isoInv_pullback_map_left, isoInv_mapPullbackAdj_unit_app_left, isoInv_mapPullbackAdj_counit_app_left, isoInv_pullback_obj_hom, isoInv_pullback_obj_right_as
mapPullbackAdj 📖	CompOp	25 math math: unit_pullbackComp_hom_assoc, iso_mapPullbackAdj_unit_app, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, isoInv_mapPullbackAdj_unit_app_left, unit_pullbackId_hom_app, cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, pullbackId_hom_counit, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, pullbackId_hom_counit_assoc, cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, pullbackComp_hom_counit, cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app, isoInv_mapPullbackAdj_counit_app_left, unit_pullbackId_hom, cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app, iso_mapPullbackAdj_counit_app, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, unit_pullbackComp_hom, pullbackComp_hom_counit_assoc, unit_pullbackId_hom_app_assoc, unit_pullbackId_hom_assoc, ofHasPullbacksAlong_mapPullbackAdj
ofHasPullbacksAlong 📖	CompOp	2 math math: ofHasPullbacksAlong_pullback, ofHasPullbacksAlong_mapPullbackAdj
pullback 📖	CompOp	59 math math: cartesianMonoidalCategoryFst_pullback_map, CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq, unit_pullbackComp_hom_assoc, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, pullbackIsoOverPullback_hom_app_comp_snd_assoc, snd'_left, isoInv_pullback_obj_left, isoInv_pullback_map_left, CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit_assoc, unit_pullbackId_hom_app, CategoryTheory.ExponentiableMorphism.ev_coev, iso_pullback_obj, pullbackId_hom_counit, CategoryTheory.ExponentiableMorphism.ev_def, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.ExponentiableMorphism.ev_coev_assoc, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit_assoc, CategoryTheory.ExponentiableMorphism.coev_def, pullbackIsoOverPullback_inv_app_comp_fst, cartesianMonoidalCategoryToUnit_pullback_obj, CategoryTheory.ExponentiableMorphism.ev_naturality_assoc, pullbackIsoOverPullback_inv_app_comp_snd, cartesianMonoidalCategorySnd_pullback_map, pullbackId_hom_counit_assoc, pullbackIsoOverPullback_hom_app_comp_snd, pullbackComp_hom_counit, CategoryTheory.ExponentiableMorphism.coev_ev_assoc, cartesianMonoidalCategoryFst_pullback_obj, cartesianMonoidalCategorySnd_pullback_obj, unit_pullbackId_hom, CategoryTheory.ExponentiableMorphism.coev_naturality_assoc, CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit, fst'_left, CategoryTheory.ExponentiableMorphism.coev_naturality, ofHasPullbacksAlong_pullback, CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom, isoInv_pullback_obj_hom, isoInv_pullback_obj_right_as, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, iso_pullback_map, CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom_assoc, pullbackIsoOverPullback_hom_app_comp_fst_assoc, CategoryTheory.ExponentiableMorphism.ev_naturality, unit_pullbackComp_hom, CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom, pullbackIsoOverPullback_inv_app_comp_fst_assoc, cartesianMonoidalCategoryToUnit_pullback_map, pullbackIsoOverPullback_hom_app_comp_fst, CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit, CategoryTheory.toOverUnitPullback_hom_app_left, CategoryTheory.ExponentiableMorphism.coev_ev, pullbackComp_hom_counit_assoc, unit_pullbackId_hom_app_assoc, CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq, CategoryTheory.toOverUnitPullback_inv_app_left, unit_pullbackId_hom_assoc, pullbackIsoOverPullback_inv_app_comp_snd_assoc, CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom_assoc
pullbackComp 📖	CompOp	4 math math: unit_pullbackComp_hom_assoc, pullbackComp_hom_counit, unit_pullbackComp_hom, pullbackComp_hom_counit_assoc
pullbackCone 📖	CompOp	2 math math: pullbackCone_snd, pullbackCone_fst
pullbackId 📖	CompOp	6 math math: unit_pullbackId_hom_app, pullbackId_hom_counit, pullbackId_hom_counit_assoc, unit_pullbackId_hom, unit_pullbackId_hom_app_assoc, unit_pullbackId_hom_assoc
pullbackIsoOverPullback 📖	CompOp	8 math math: pullbackIsoOverPullback_hom_app_comp_snd_assoc, pullbackIsoOverPullback_inv_app_comp_fst, pullbackIsoOverPullback_inv_app_comp_snd, pullbackIsoOverPullback_hom_app_comp_snd, pullbackIsoOverPullback_hom_app_comp_fst_assoc, pullbackIsoOverPullback_inv_app_comp_fst_assoc, pullbackIsoOverPullback_hom_app_comp_fst, pullbackIsoOverPullback_inv_app_comp_snd_assoc
pullbackMap 📖	CompOp	11 math math: pullbackMap_snd, Over.whiskerRight_left, pullbackMap_fst_assoc, pullbackMap_comp_assoc, pullbackMap_fst, pullbackMap_id, pullbackMap_snd_assoc, pullbackMap_comp, Over.whiskerLeft_left, CategoryTheory.Over.sections_map, Over.tensorHom_left
pullbackObj 📖	CompOp	37 math math: Over.associator_hom_left_snd_fst_assoc, Over.tensorHom_left_fst, hom_ext_iff, pullbackMap_snd, Over.tensorObj_hom, Over.tensorObj_left, lift_snd, Over.associator_hom_left_fst, isPullback, Over.associator_hom_left_snd_fst, condition_assoc, pullbackMap_fst_assoc, pullbackMap_comp_assoc, CategoryTheory.Over.toOverSectionsAdj_counit_app, CategoryTheory.Over.sections_obj, lift_fst, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, pullbackMap_fst, lift_snd_assoc, Over.associator_inv_left_fst_snd_assoc, Over.associator_inv_left_fst_snd, pullbackMap_id, pullbackMap_snd_assoc, Over.whiskerRight_left_fst, pullbackMap_comp, Over.associator_inv_left_snd_assoc, condition, Over.associator_inv_left_fst_fst, Over.associator_inv_left_snd, Over.whiskerLeft_left_snd, Over.associator_hom_left_snd_snd, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, lift_fst_assoc, Over.associator_hom_left_fst_assoc, Over.tensorHom_left_snd, Over.associator_inv_left_fst_fst_assoc, Over.associator_hom_left_snd_snd_assoc
snd 📖	CompOp	39 math math: Over.associator_hom_left_snd_fst_assoc, pullbackCone_snd, hom_ext_iff, pullbackIsoOverPullback_hom_app_comp_snd_assoc, pullbackMap_snd, snd'_left, Over.tensorObj_ext_iff, Over.tensorHom_left_snd_assoc, Over.rightUnitor_inv_left_snd, Over.tensorObj_hom, lift_snd, Over.associator_hom_left_fst, isPullback, Over.leftUnitor_inv_left_snd, Over.whiskerLeft_left_snd_assoc, Over.associator_hom_left_snd_fst, condition_assoc, Over.rightUnitor_inv_left_snd_assoc, Over.whiskerRight_left_snd, Over.whiskerRight_left_snd_assoc, pullbackIsoOverPullback_inv_app_comp_snd, lift_snd_assoc, pullbackIsoOverPullback_hom_app_comp_snd, Over.associator_inv_left_fst_snd_assoc, Over.associator_inv_left_fst_snd, pullbackMap_snd_assoc, Over.associator_inv_left_snd_assoc, condition, Over.leftUnitor_hom_left, Over.associator_inv_left_fst_fst, Over.associator_inv_left_snd, Over.whiskerLeft_left_snd, Over.associator_hom_left_snd_snd, Over.leftUnitor_inv_left_snd_assoc, pullbackIsoOverPullback_inv_app_comp_snd_assoc, Over.associator_hom_left_fst_assoc, Over.tensorHom_left_snd, Over.associator_inv_left_fst_fst_assoc, Over.associator_hom_left_snd_snd_assoc
snd' 📖	CompOp	2 math math: snd'_left, Over.snd_eq_snd'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Over.homMk CategoryTheory.CommaMorphism.left CategoryTheory.Over.map CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Adjunction.counit mapPullbackAdj cartesianMonoidalCategoryFst	—	—
cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.instCategoryOver CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Over.homMk CategoryTheory.CommaMorphism.left CategoryTheory.Adjunction.unit mapPullbackAdj cartesianMonoidalCategoryFst CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
cartesianMonoidalCategoryFst_pullback_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory pullback CategoryTheory.SemiCartesianMonoidalCategory.fst cartesianMonoidalCategoryFst CategoryTheory.Over.homMk CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left	—	—
cartesianMonoidalCategoryFst_pullback_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory pullback CategoryTheory.SemiCartesianMonoidalCategory.fst cartesianMonoidalCategoryFst CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Comma.hom CategoryTheory.Over.homMk CategoryTheory.CommaMorphism.left CategoryTheory.Over.map CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Adjunction.counit mapPullbackAdj cartesianMonoidalCategorySnd	—	—
cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.instCategoryOver CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Comma.hom CategoryTheory.Over.homMk CategoryTheory.CommaMorphism.left CategoryTheory.Adjunction.unit mapPullbackAdj cartesianMonoidalCategorySnd CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CategoryStruct.id	—	—
cartesianMonoidalCategorySnd_pullback_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory pullback CategoryTheory.SemiCartesianMonoidalCategory.snd cartesianMonoidalCategorySnd CategoryTheory.Over.homMk CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left	—	—
cartesianMonoidalCategorySnd_pullback_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory pullback CategoryTheory.SemiCartesianMonoidalCategory.snd cartesianMonoidalCategorySnd CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Comma.hom	—	—
cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Over.homMk CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.CommaMorphism.left CategoryTheory.Over.map CategoryTheory.Adjunction.counit mapPullbackAdj cartesianMonoidalCategoryToUnit CategoryTheory.Functor.obj CategoryTheory.SemiCartesianMonoidalCategory.fst	—	—
cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Over.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Over.homMk CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.CommaMorphism.left CategoryTheory.Adjunction.unit mapPullbackAdj cartesianMonoidalCategoryToUnit CategoryTheory.Functor.obj CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom	—	—
cartesianMonoidalCategoryToUnit_pullback_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.instCategoryOver pullback cartesianMonoidalCategoryToUnit CategoryTheory.Over.homMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.CommaMorphism.left	—	—
cartesianMonoidalCategoryToUnit_pullback_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.instCategoryOver pullback cartesianMonoidalCategoryToUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullbackObj fst snd	—	CategoryTheory.Over.w
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullbackObj fst snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
fst'_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.map pullback fst' fst	—	—
hasPullbackAlong 📖	mathematical	—	CategoryTheory.Limits.HasPullbacksAlong	—	CategoryTheory.IsPullback.hasPullback isPullback
hasPullbacks 📖	mathematical	—	CategoryTheory.Limits.HasPullbacks	—	CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan hasPullbackAlong
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullbackObj fst snd	—	—	Equiv.injective CategoryTheory.Functor.map_injective CategoryTheory.Over.forget_faithful
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullbackObj fst snd	—	hom_ext
isPullback 📖	mathematical	—	CategoryTheory.IsPullback pullbackObj fst snd	—	condition
isoInv_mapPullbackAdj_counit_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.Iso.symm CategoryTheory.Over.homMk CategoryTheory.Over.map CategoryTheory.Iso.hom CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit mapPullbackAdj isoInv CategoryTheory.CategoryStruct.id	—	—
isoInv_mapPullbackAdj_unit_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.Iso.hom CategoryTheory.Iso.symm CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.Over.homMk CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit mapPullbackAdj isoInv CategoryTheory.CategoryStruct.id	—	—
isoInv_pullback_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.Iso.symm CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver pullback isoInv	—	—
isoInv_pullback_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Iso.inv isoInv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Iso.hom	—	—
isoInv_pullback_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Iso.inv isoInv	—	—
isoInv_pullback_obj_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Iso.inv isoInv	—	—
iso_mapPullbackAdj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.Over.homMk CategoryTheory.CommaMorphism.left CategoryTheory.Over.map CategoryTheory.Iso.hom CategoryTheory.Adjunction.counit mapPullbackAdj iso CategoryTheory.CategoryStruct.id	—	—
iso_mapPullbackAdj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.Over.homMk CategoryTheory.CommaMorphism.left CategoryTheory.Adjunction.unit mapPullbackAdj iso CategoryTheory.CategoryStruct.id	—	—
iso_pullback_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Iso.hom iso CategoryTheory.Over.homMk CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.CommaMorphism.left	—	—
iso_pullback_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Iso.hom iso CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv	—	—
lift_fst 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj lift fst	—	Equiv.symm_apply_apply
lift_fst_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj lift fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fst
lift_snd 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj lift snd	—	CategoryTheory.Over.w
lift_snd_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj lift snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_snd
ofHasPullbacksAlong_mapPullbackAdj 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	mapPullbackAdj ofHasPullbacksAlong CategoryTheory.Over.mapPullbackAdj	—	—
ofHasPullbacksAlong_pullback 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	pullback ofHasPullbacksAlong CategoryTheory.Over.pullback	—	—
pullbackComp_hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.Over.map CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pullbackComp CategoryTheory.Adjunction.counit comp mapPullbackAdj	—	pullbackComp.eq_1 CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
pullbackComp_hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.Over.map CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pullbackComp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit comp mapPullbackAdj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackComp_hom_counit
pullbackCone_fst 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.fst pullbackCone fst	—	—
pullbackCone_snd 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.snd pullbackCone snd	—	—
pullbackId_hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.CategoryStruct.id CategoryTheory.Over.map CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pullbackId CategoryTheory.Adjunction.counit id mapPullbackAdj	—	CategoryTheory.Adjunction.rightAdjointUniq_hom_counit pullbackId.eq_1
pullbackId_hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.CategoryStruct.id CategoryTheory.Over.map CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pullbackId CategoryTheory.Adjunction.counit id mapPullbackAdj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackId_hom_counit
pullbackIsoOverPullback_hom_app_comp_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Over.pullback hasPullbackAlong CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom fst	—	hasPullbackAlong CategoryTheory.Category.id_comp CategoryTheory.Over.mapPullbackAdj_counit_app CategoryTheory.Functor.congr_map CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit
pullbackIsoOverPullback_hom_app_comp_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Over.pullback hasPullbackAlong CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom fst	—	hasPullbackAlong CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOverPullback_hom_app_comp_fst
pullbackIsoOverPullback_hom_app_comp_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Over.pullback hasPullbackAlong CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom snd	—	CategoryTheory.Over.w hasPullbackAlong
pullbackIsoOverPullback_hom_app_comp_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Over.pullback hasPullbackAlong CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom snd	—	hasPullbackAlong CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOverPullback_hom_app_comp_snd
pullbackIsoOverPullback_inv_app_comp_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback hasPullbackAlong pullback CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback fst CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right	—	hasPullbackAlong CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.id_comp
pullbackIsoOverPullback_inv_app_comp_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback hasPullbackAlong pullback CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback fst CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right	—	hasPullbackAlong CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOverPullback_inv_app_comp_fst
pullbackIsoOverPullback_inv_app_comp_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback hasPullbackAlong pullback CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback snd CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right	—	CategoryTheory.Over.w hasPullbackAlong
pullbackIsoOverPullback_inv_app_comp_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback hasPullbackAlong pullback CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullbackIsoOverPullback snd CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right	—	hasPullbackAlong CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOverPullback_inv_app_comp_snd
pullbackMap_comp 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj pullbackMap	—	hom_ext CategoryTheory.Category.assoc pullbackMap_fst pullbackMap_fst_assoc pullbackMap_snd pullbackMap_snd_assoc
pullbackMap_comp_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj pullbackMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackMap_comp
pullbackMap_fst 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj pullbackMap fst	—	lift_fst
pullbackMap_fst_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj pullbackMap fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackMap_fst
pullbackMap_id 📖	mathematical	—	pullbackMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct pullbackObj	—	hom_ext pullbackMap_fst CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp pullbackMap_snd
pullbackMap_snd 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj pullbackMap snd	—	lift_snd
pullbackMap_snd_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullbackObj pullbackMap snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackMap_snd
snd'_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.map pullback snd' snd	—	—
unit_pullbackComp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map pullback CategoryTheory.Adjunction.unit mapPullbackAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pullbackComp comp	—	pullbackComp.eq_1 CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
unit_pullbackComp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map pullback CategoryTheory.Adjunction.unit mapPullbackAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pullbackComp comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_pullbackComp_hom
unit_pullbackId_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.CategoryStruct.id pullback CategoryTheory.Adjunction.unit mapPullbackAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pullbackId id	—	pullbackId.eq_1 CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
unit_pullbackId_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.CategoryStruct.id pullback CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit mapPullbackAdj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackId id	—	pullbackId.eq_1 CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app
unit_pullbackId_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Over CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj pullback CategoryTheory.CategoryStruct.id CategoryTheory.Over.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit mapPullbackAdj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackId id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_pullbackId_hom_app
unit_pullbackId_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over.map CategoryTheory.CategoryStruct.id pullback CategoryTheory.Adjunction.unit mapPullbackAdj CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pullbackId id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_pullbackId_hom

---

← Back to Index