Pullback

📁 Source: Mathlib/CategoryTheory/Comma/Over/Pullback.lean

Statistics

Metric	Count
Definitions forgetAdjStar, forgetMapTerminal, mapPullbackAdj, postAdjunctionLeft, pullback, pullbackComp, pullbackId, starPullbackIsoStar, costar, costarAdjForget, forgetMapInitial, mapPushoutAdj, postAdjunctionRight, pushout, pushoutComp, pushoutId	16
Theorems faithful_pullback, forgetAdjStar_counit_app, forgetAdjStar_unit_app_left, forgetMapTerminal_hom_app, forgetMapTerminal_inv_app, instIsLeftAdjointForget, instIsRightAdjointStar, isLeftAdjoint_post, mapPullbackAdj_counit_app, mapPullbackAdj_unit_app, postAdjunctionLeft_counit_app_left, postAdjunctionLeft_unit_app_left, pullbackIsRightAdjoint, pullback_map_left, pullback_obj_hom, pullback_obj_left, starPullbackIsoStar_hom_app_left, starPullbackIsoStar_inv_app_left, star_map_left, star_obj_hom, star_obj_left, costar_map_left, costar_obj_hom, costar_obj_left, faithful_pushout, forgetMapInitial_hom_app, forgetMapInitial_inv_app, instIsLeftAdjointCostar, instIsRightAdjointForget, isRightAdjoint_post, mapPushoutAdj_counit_app, mapPushoutAdj_unit_app, postAdjunctionRight_counit_app_right, postAdjunctionRight_unit_app_right, pushoutIsLeftAdjoint, pushout_map, pushout_obj	37
Total	53

CategoryTheory.Over

Definitions

Name	Category	Theorems
forgetAdjStar 📖	CompOp	2 math math: forgetAdjStar_counit_app, forgetAdjStar_unit_app_left
forgetMapTerminal 📖	CompOp	2 math math: forgetMapTerminal_hom_app, forgetMapTerminal_inv_app
mapPullbackAdj 📖	CompOp	4 math math: mapPullbackAdj_counit_app, mapPullbackAdj_unit_app, CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_mapPullbackAdj, postAdjunctionLeft_counit_app_left
postAdjunctionLeft 📖	CompOp	2 math math: postAdjunctionLeft_unit_app_left, postAdjunctionLeft_counit_app_left
pullback 📖	CompOp	45 math math: μ_pullback_left_snd', faithful_pullback, pullback_obj_left, monObjMkPullbackSnd_mul, grpObjMkPullbackSnd_one, grpObjMkPullbackSnd_mul, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd_assoc, CategoryTheory.MorphismProperty.baseChange_map, postAdjunctionLeft_unit_app_left, preservesTerminalIso_pullback, mapPullbackAdj_counit_app, AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact, starPullbackIsoStar_hom_app_left, prodComparisonIso_pullback_inv_left_snd', μ_pullback_left_fst_snd', mapPullbackAdj_unit_app, pullbackIsRightAdjoint, pullback_map_left, prodComparisonIso_pullback_inv_left_fst_fst, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst, μ_pullback_left_fst_fst', μ_pullback_left_fst_snd, monObjMkPullbackSnd_one, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd, η_pullback_left, prodComparisonIso_pullback_Spec_inv_left_fst_fst', CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_pullback, μ_pullback_left_snd, μ_pullback_left_fst_fst, starPullbackIsoStar_inv_app_left, CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst_assoc, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst_assoc, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst, pullback_obj_hom, prodComparisonIso_pullback_inv_left_fst_snd', ε_pullback_left, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd_assoc, CategoryTheory.Limits.diagonal_pullback_fst, CategoryTheory.MorphismProperty.baseChange_obj, AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation, postAdjunctionLeft_counit_app_left
pullbackComp 📖	CompOp	—
pullbackId 📖	CompOp	—
starPullbackIsoStar 📖	CompOp	2 math math: starPullbackIsoStar_hom_app_left, starPullbackIsoStar_inv_app_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful_pullback 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong CategoryTheory.Epi CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	CategoryTheory.Functor.Faithful CategoryTheory.Over CategoryTheory.instCategoryOver pullback	—	CategoryTheory.Category.id_comp mapPullbackAdj_counit_app epi_homMk CategoryTheory.Adjunction.faithful_R_of_epi_counit_app
forgetAdjStar_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver star forget CategoryTheory.Functor.id CategoryTheory.Adjunction.counit forgetAdjStar CategoryTheory.Limits.prod.snd	—	CategoryTheory.Adjunction.comp_counit_app CategoryTheory.Category.id_comp CategoryTheory.Comonad.adj_counit
forgetAdjStar_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 forget star CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit forgetAdjStar CategoryTheory.Limits.prod.lift CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.pair CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Adjunction.comp_unit_app CategoryTheory.Comonad.adj_unit CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.id_comp
forgetMapTerminal_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver forget CategoryTheory.Functor.comp map CategoryTheory.Limits.IsTerminal.from CategoryTheory.Equivalence.functor equivalenceOfIsTerminal CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category forgetMapTerminal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
forgetMapTerminal_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp map CategoryTheory.Limits.IsTerminal.from CategoryTheory.Equivalence.functor equivalenceOfIsTerminal forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category forgetMapTerminal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
instIsLeftAdjointForget 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Over CategoryTheory.instCategoryOver forget	—	—
instIsRightAdjointStar 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Over CategoryTheory.instCategoryOver star	—	—
isLeftAdjoint_post 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj post	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
mapPullbackAdj_counit_app 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp pullback map CategoryTheory.Functor.id CategoryTheory.Adjunction.counit mapPullbackAdj homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right CategoryTheory.Category.id_comp	—	homMk.congr_simp CategoryTheory.Category.id_comp
mapPullbackAdj_unit_app 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.id CategoryTheory.Functor.comp map pullback CategoryTheory.Adjunction.unit mapPullbackAdj homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.lift CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
postAdjunctionLeft_counit_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver post CategoryTheory.Functor.comp pullback CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.Adjunction.counit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan postAdjunctionLeft map CategoryTheory.Limits.pullback CategoryTheory.Comma.left CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.snd DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv CategoryTheory.Adjunction.comp mapPullbackAdj postAdjunctionRight CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp
postAdjunctionLeft_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 post pullback CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan postAdjunctionLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Limits.pullback CategoryTheory.Comma.hom map CategoryTheory.Functor.map CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.id CategoryTheory.Adjunction.counit CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver homMk CategoryTheory.Comma.right DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.equivHomsetLeftOfNatIso CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatIso.ofComponents isoMk CategoryTheory.Iso.refl	—	CategoryTheory.Adjunction.comp_unit_app CategoryTheory.Category.assoc
pullbackIsRightAdjoint 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Over CategoryTheory.instCategoryOver pullback	—	—
pullback_map_left 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst	—	—
pullback_obj_hom 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.left	—	—
pullback_obj_left 📖	mathematical	CategoryTheory.Limits.HasPullbacksAlong	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Limits.pullback CategoryTheory.Comma.hom	—	—
starPullbackIsoStar_hom_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 star pullback CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan starPullbackIsoStar CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.prod CategoryTheory.Comma.hom CategoryTheory.Limits.prod.fst CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullbackProdFstIsoProd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
starPullbackIsoStar_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver star CategoryTheory.Functor.comp pullback CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan starPullbackIsoStar CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.pullback CategoryTheory.Limits.prod.fst CategoryTheory.Comma.hom CategoryTheory.Limits.pullbackProdFstIsoProd CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.pullback.congrHom_inv CategoryTheory.Category.assoc
star_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comonad.Coalgebra CategoryTheory.prodComonad CategoryTheory.Comonad.Coalgebra.eilenbergMoore CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.coalgebraToOver CategoryTheory.Comonad.cofree CategoryTheory.Functor.map star CategoryTheory.Limits.prod.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
star_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver star CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.limit.lift_π
star_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver star CategoryTheory.Limits.prod	—	—

CategoryTheory.Under

Definitions

Name	Category	Theorems
costar 📖	CompOp	4 math math: costar_obj_left, instIsLeftAdjointCostar, costar_map_left, costar_obj_hom
costarAdjForget 📖	CompOp	—
forgetMapInitial 📖	CompOp	2 math math: forgetMapInitial_inv_app, forgetMapInitial_hom_app
mapPushoutAdj 📖	CompOp	3 math math: postAdjunctionRight_unit_app_right, mapPushoutAdj_unit_app, mapPushoutAdj_counit_app
postAdjunctionRight 📖	CompOp	2 math math: postAdjunctionRight_unit_app_right, postAdjunctionRight_counit_app_right
pushout 📖	CompOp	16 math math: pushoutIsLeftAdjoint, pushout_map, CommRingCat.Under.preservesFiniteLimits_of_flat, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, postAdjunctionRight_unit_app_right, mapPushoutAdj_unit_app, CommRingCat.Under.instPreservesFiniteProductsUnderPushout, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, CommRingCat.tensorProdIsoPushout_app, pushout_obj, CategoryTheory.MorphismProperty.ind_underObj_pushout, mapPushoutAdj_counit_app, postAdjunctionRight_counit_app_right, faithful_pushout, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
pushoutComp 📖	CompOp	—
pushoutId 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
costar_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Monad.Algebra CategoryTheory.coprodMonad CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.algebraToUnder CategoryTheory.Monad.free CategoryTheory.Functor.map costar CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Limits.coprod CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.desc	—	—
costar_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder costar CategoryTheory.Limits.coprod.inl	—	CategoryTheory.Limits.colimit.ι_desc
costar_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder costar	—	—
faithful_pushout 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong CategoryTheory.Mono CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inl	CategoryTheory.Functor.Faithful CategoryTheory.Under CategoryTheory.instCategoryUnder pushout	—	CategoryTheory.Category.comp_id mapPushoutAdj_unit_app mono_homMk CategoryTheory.Adjunction.faithful_L_of_mono_unit_app
forgetMapInitial_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Under CategoryTheory.instCategoryUnder forget CategoryTheory.Functor.comp map CategoryTheory.Limits.IsInitial.to CategoryTheory.Equivalence.functor equivalenceOfIsInitial CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category forgetMapInitial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—
forgetMapInitial_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp map CategoryTheory.Limits.IsInitial.to CategoryTheory.Equivalence.functor equivalenceOfIsInitial forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category forgetMapInitial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—
instIsLeftAdjointCostar 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Under CategoryTheory.instCategoryUnder costar	—	—
instIsRightAdjointForget 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Under CategoryTheory.instCategoryUnder forget	—	—
isRightAdjoint_post 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Under CategoryTheory.Functor.obj CategoryTheory.instCategoryUnder post	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
mapPushoutAdj_counit_app 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong	CategoryTheory.NatTrans.app CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp map pushout CategoryTheory.Functor.id CategoryTheory.Adjunction.counit mapPushoutAdj homMk CategoryTheory.Limits.pushout CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.Functor.obj CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.desc CategoryTheory.CategoryStruct.id	—	—
mapPushoutAdj_unit_app 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong	CategoryTheory.NatTrans.app CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.id CategoryTheory.Functor.comp pushout map CategoryTheory.Adjunction.unit mapPushoutAdj homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pushout CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left CategoryTheory.Category.comp_id	—	homMk.congr_simp CategoryTheory.Category.comp_id
postAdjunctionRight_counit_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp post pushout CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span postAdjunctionRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Adjunction.unit CategoryTheory.Limits.pushout.desc map DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.equivHomsetRightOfNatIso CategoryTheory.NatIso.ofComponents isoMk CategoryTheory.Iso.refl CategoryTheory.CategoryStruct.id CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr homMk CategoryTheory.Comma.left	—	CategoryTheory.Adjunction.comp_counit_app
postAdjunctionRight_unit_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Under CategoryTheory.instCategoryUnder post CategoryTheory.Functor.comp pushout CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit CategoryTheory.Adjunction.unit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span postAdjunctionRight map CategoryTheory.Limits.pushout CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout.inr DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv CategoryTheory.Adjunction.comp postAdjunctionLeft mapPushoutAdj CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.comp_id
pushoutIsLeftAdjoint 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Under CategoryTheory.instCategoryUnder pushout	—	—
pushout_map 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong	CategoryTheory.Functor.map CategoryTheory.Under CategoryTheory.instCategoryUnder pushout homMk CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.desc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right CategoryTheory.Limits.pushout.inl	—	—
pushout_obj 📖	mathematical	CategoryTheory.Limits.HasPushoutsAlong	CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder pushout CategoryTheory.Limits.pushout CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pushout.inr	—	—

---

← Back to Index