PullbackObjObj

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackObjObj.lean

Statistics

Metric	Count
Definitions adj, PullbackObjObj, fst, mapArrowLeft, mapArrowRight, ofHasPullback, pt, snd, π, π_iso_of_iso_left, π_iso_of_iso_right, PushoutObjObj, flip, inl, inr, mapArrowLeft, mapArrowRight, ofHasPushout, pt, ι, ι_iso_of_iso_left, ι_iso_of_iso_right, leibnizAdjunction, leibnizPullback, leibnizPushout	25
Theorems adj_counit_app_left, adj_counit_app_right, adj_unit_app_left, adj_unit_app_right, hom_ext, hom_ext_iff, isPullback, mapArrowLeft_comp, mapArrowLeft_comp_assoc, mapArrowLeft_id, mapArrowLeft_left, mapArrowLeft_right, mapArrowRight_comp, mapArrowRight_comp_assoc, mapArrowRight_id, mapArrowRight_left, mapArrowRight_right, ofHasPullback_fst, ofHasPullback_pt, ofHasPullback_snd, ofHasPullback_π, π_fst, π_fst_assoc, π_iso_of_iso_left_hom, π_iso_of_iso_left_inv, π_iso_of_iso_right_hom, π_iso_of_iso_right_inv, π_snd, π_snd_assoc, flip_inl, flip_inr, flip_pt, hom_ext, hom_ext_iff, inl_ι, inl_ι_assoc, inr_ι, inr_ι_assoc, isPushout, mapArrowLeft_comp, mapArrowLeft_comp_assoc, mapArrowLeft_id, mapArrowLeft_left, mapArrowLeft_right, mapArrowRight_comp, mapArrowRight_comp_assoc, mapArrowRight_id, mapArrowRight_left, mapArrowRight_right, ofHasPushout_inl, ofHasPushout_inr, ofHasPushout_pt, ofHasPushout_ι, ι_flip, ι_iso_of_iso_left_hom, ι_iso_of_iso_left_inv, ι_iso_of_iso_right_hom, ι_iso_of_iso_right_inv, leibnizAdjunction_adj, leibnizPullback_map_app, leibnizPullback_obj_map, leibnizPullback_obj_obj, leibnizPushout_map_app, leibnizPushout_obj_map, leibnizPushout_obj_obj	65
Total	90

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PullbackObjObj 📖	CompData	—
PushoutObjObj 📖	CompData	—
leibnizAdjunction 📖	CompOp	1 math math: leibnizAdjunction_adj
leibnizPullback 📖	CompOp	8 math math: leibnizPullback_obj_map, LeibnizAdjunction.adj_unit_app_left, LeibnizAdjunction.adj_counit_app_left, leibnizAdjunction_adj, LeibnizAdjunction.adj_counit_app_right, LeibnizAdjunction.adj_unit_app_right, leibnizPullback_map_app, leibnizPullback_obj_obj
leibnizPushout 📖	CompOp	8 math math: LeibnizAdjunction.adj_unit_app_left, LeibnizAdjunction.adj_counit_app_left, leibnizAdjunction_adj, leibnizPushout_obj_map, LeibnizAdjunction.adj_counit_app_right, leibnizPushout_obj_obj, LeibnizAdjunction.adj_unit_app_right, leibnizPushout_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leibnizAdjunction_adj 📖	mathematical	—	CategoryTheory.ParametrizedAdjunction.adj CategoryTheory.Arrow CategoryTheory.instCategoryArrow leibnizPushout leibnizPullback leibnizAdjunction LeibnizAdjunction.adj	—	—
leibnizPullback_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category Opposite.op id CategoryTheory.Comma.right Opposite.unop CategoryTheory.Comma.left PullbackObjObj.pt CategoryTheory.Comma.hom PullbackObjObj.ofHasPullback PullbackObjObj.π PullbackObjObj.mapArrowRight map leibnizPullback PullbackObjObj.mapArrowLeft Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
leibnizPullback_obj_map 📖	mathematical	—	map CategoryTheory.Arrow CategoryTheory.instCategoryArrow obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category leibnizPullback PullbackObjObj.mapArrowRight Opposite.unop PullbackObjObj.ofHasPullback id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
leibnizPullback_obj_obj 📖	mathematical	—	obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category leibnizPullback Opposite.op id CategoryTheory.Comma.right Opposite.unop CategoryTheory.Comma.left PullbackObjObj.pt CategoryTheory.Comma.hom PullbackObjObj.ofHasPullback PullbackObjObj.π	—	—
leibnizPushout_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow PushoutObjObj.pt obj id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom PushoutObjObj.ofHasPushout CategoryTheory.Functor category PushoutObjObj.ι PushoutObjObj.mapArrowRight map leibnizPushout PushoutObjObj.mapArrowLeft	—	—
leibnizPushout_obj_map 📖	mathematical	—	map CategoryTheory.Arrow CategoryTheory.instCategoryArrow obj CategoryTheory.Functor category leibnizPushout PushoutObjObj.mapArrowRight PushoutObjObj.ofHasPushout id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
leibnizPushout_obj_obj 📖	mathematical	—	obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor category leibnizPushout PushoutObjObj.pt id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom PushoutObjObj.ofHasPushout PushoutObjObj.ι	—	—

CategoryTheory.Functor.LeibnizAdjunction

Definitions

Name	Category	Theorems
adj 📖	CompOp	5 math math: adj_unit_app_left, adj_counit_app_left, CategoryTheory.Functor.leibnizAdjunction_adj, adj_counit_app_right, adj_unit_app_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj_counit_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.leibnizPullback Opposite.op CategoryTheory.Functor.leibnizPushout CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit adj CategoryTheory.Limits.pushout.desc CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.ParametrizedAdjunction.homEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Limits.pullback.fst Opposite.unop Quiver.Hom.op	—	—
adj_counit_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.leibnizPullback Opposite.op CategoryTheory.Functor.leibnizPushout CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit adj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.ParametrizedAdjunction.homEquiv CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.left Opposite.unop CategoryTheory.Functor.map CategoryTheory.Comma.hom Quiver.Hom.op	—	—
adj_unit_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.leibnizPushout Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leibnizPullback Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit adj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right Opposite.unop CategoryTheory.Comma.left EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.ParametrizedAdjunction.homEquiv CategoryTheory.Limits.pushout.inl CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
adj_unit_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.leibnizPushout Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leibnizPullback Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit adj CategoryTheory.Limits.pullback.lift CategoryTheory.Comma.right CategoryTheory.Comma.left Opposite.unop CategoryTheory.Functor.map CategoryTheory.Comma.hom Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.ParametrizedAdjunction.homEquiv CategoryTheory.Limits.pushout.inr CategoryTheory.CategoryStruct.id	—	—

CategoryTheory.Functor.PullbackObjObj

Definitions

Name	Category	Theorems
fst 📖	CompOp	11 math math: mapArrowRight_right, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, π_fst, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, mapArrowLeft_right, π_fst_assoc, hom_ext_iff, ofHasPullback_fst, isPullback
mapArrowLeft 📖	CompOp	8 math math: mapArrowLeft_id, π_iso_of_iso_left_inv, mapArrowLeft_comp, mapArrowLeft_left, mapArrowLeft_comp_assoc, mapArrowLeft_right, CategoryTheory.Functor.leibnizPullback_map_app, π_iso_of_iso_left_hom
mapArrowRight 📖	CompOp	9 math math: CategoryTheory.Functor.leibnizPullback_obj_map, mapArrowRight_right, π_iso_of_iso_right_hom, mapArrowRight_comp_assoc, mapArrowRight_comp, π_iso_of_iso_right_inv, mapArrowRight_id, mapArrowRight_left, CategoryTheory.Functor.leibnizPullback_map_app
ofHasPullback 📖	CompOp	7 math math: CategoryTheory.Functor.leibnizPullback_obj_map, ofHasPullback_π, ofHasPullback_snd, ofHasPullback_pt, CategoryTheory.Functor.leibnizPullback_map_app, CategoryTheory.Functor.leibnizPullback_obj_obj, ofHasPullback_fst
pt 📖	CompOp	34 math math: mapArrowRight_right, mapArrowLeft_id, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left, π_fst, π_iso_of_iso_left_inv, mapArrowLeft_comp, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right, π_iso_of_iso_right_hom, mapArrowRight_comp_assoc, CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, mapArrowRight_comp, π_iso_of_iso_right_inv, mapArrowLeft_left, mapArrowLeft_comp_assoc, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc, mapArrowRight_id, π_snd_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, π_snd, mapArrowRight_left, mapArrowLeft_right, ofHasPullback_pt, π_fst_assoc, hom_ext_iff, CategoryTheory.Functor.leibnizPullback_map_app, π_iso_of_iso_left_hom, CategoryTheory.Functor.leibnizPullback_obj_obj, isPullback, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc
snd 📖	CompOp	10 math math: mapArrowRight_right, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right, ofHasPullback_snd, π_snd_assoc, π_snd, mapArrowLeft_right, hom_ext_iff, isPullback, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc
π 📖	CompOp	32 math math: mapArrowRight_right, mapArrowLeft_id, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left, π_fst, π_iso_of_iso_left_inv, mapArrowLeft_comp, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right, π_iso_of_iso_right_hom, mapArrowRight_comp_assoc, CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, ofHasPullback_π, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, mapArrowRight_comp, π_iso_of_iso_right_inv, mapArrowLeft_left, mapArrowLeft_comp_assoc, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc, mapArrowRight_id, π_snd_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, π_snd, mapArrowRight_left, mapArrowLeft_right, π_fst_assoc, CategoryTheory.Functor.leibnizPullback_map_app, π_iso_of_iso_left_hom, CategoryTheory.Functor.leibnizPullback_obj_obj, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc
π_iso_of_iso_left 📖	CompOp	2 math math: π_iso_of_iso_left_inv, π_iso_of_iso_left_hom
π_iso_of_iso_right 📖	CompOp	2 math math: π_iso_of_iso_right_hom, π_iso_of_iso_right_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pt CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op fst snd	—	—	CategoryTheory.IsPullback.hom_ext isPullback
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pt CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op fst snd	—	hom_ext
isPullback 📖	mathematical	—	CategoryTheory.IsPullback pt CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op fst snd CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
mapArrowLeft_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowLeft	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_comp CategoryTheory.IsPullback.lift.congr_simp hom_ext CategoryTheory.Category.assoc CategoryTheory.IsPullback.lift_fst CategoryTheory.IsPullback.lift_fst_assoc CategoryTheory.IsPullback.lift_snd CategoryTheory.IsPullback.lift_snd_assoc
mapArrowLeft_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapArrowLeft_comp
mapArrowLeft_id 📖	mathematical	—	mapArrowLeft CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.IsPullback.lift.congr_simp hom_ext CategoryTheory.IsPullback.lift_fst CategoryTheory.Category.id_comp CategoryTheory.IsPullback.lift_snd
mapArrowLeft_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right	—	—
mapArrowLeft_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowLeft CategoryTheory.IsPullback.lift fst snd CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.CommaMorphism.left	—	—
mapArrowRight_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowRight	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_comp CategoryTheory.IsPullback.lift.congr_simp hom_ext CategoryTheory.Category.assoc CategoryTheory.IsPullback.lift_fst CategoryTheory.IsPullback.lift_fst_assoc CategoryTheory.IsPullback.lift_snd CategoryTheory.IsPullback.lift_snd_assoc
mapArrowRight_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapArrowRight_comp
mapArrowRight_id 📖	mathematical	—	mapArrowRight CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.IsPullback.lift.congr_simp hom_ext CategoryTheory.IsPullback.lift_fst CategoryTheory.Category.id_comp CategoryTheory.IsPullback.lift_snd
mapArrowRight_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowRight CategoryTheory.Functor.map	—	—
mapArrowRight_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π mapArrowRight CategoryTheory.IsPullback.lift fst snd CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.CommaMorphism.left	—	—
ofHasPullback_fst 📖	mathematical	—	fst ofHasPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
ofHasPullback_pt 📖	mathematical	—	pt ofHasPullback CategoryTheory.Limits.pullback CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
ofHasPullback_snd 📖	mathematical	—	snd ofHasPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
ofHasPullback_π 📖	mathematical	—	π ofHasPullback CategoryTheory.Limits.pullback.lift CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	hom_ext CategoryTheory.IsPullback.lift_fst isPullback CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.lift_snd
π_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op pt π fst CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.IsPullback.lift_fst isPullback
π_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op pt π fst CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_fst
π_iso_of_iso_left_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π π_iso_of_iso_left mapArrowLeft CategoryTheory.Iso.inv	—	—
π_iso_of_iso_left_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π π_iso_of_iso_left mapArrowLeft CategoryTheory.Iso.hom	—	—
π_iso_of_iso_right_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π π_iso_of_iso_right mapArrowRight	—	—
π_iso_of_iso_right_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left pt CategoryTheory.Comma.hom π π_iso_of_iso_right mapArrowRight	—	—
π_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op pt π snd CategoryTheory.Functor.map	—	CategoryTheory.IsPullback.lift_snd isPullback
π_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op pt π snd CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_snd

CategoryTheory.Functor.PushoutObjObj

Definitions

Name	Category	Theorems
flip 📖	CompOp	4 math math: flip_pt, ι_flip, flip_inr, flip_inl
inl 📖	CompOp	12 math math: CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left, mapArrowRight_left, flip_inr, isPushout, flip_inl, inl_ι_assoc, ofHasPushout_inl, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc, mapArrowLeft_left, hom_ext_iff, inl_ι
inr 📖	CompOp	13 math math: inr_ι, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, mapArrowRight_left, flip_inr, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, isPushout, flip_inl, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, mapArrowLeft_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, ofHasPushout_inr, inr_ι_assoc, hom_ext_iff
mapArrowLeft 📖	CompOp	8 math math: mapArrowLeft_id, ι_iso_of_iso_left_inv, mapArrowLeft_left, mapArrowLeft_right, mapArrowLeft_comp_assoc, mapArrowLeft_comp, ι_iso_of_iso_left_hom, CategoryTheory.Functor.leibnizPushout_map_app
mapArrowRight 📖	CompOp	9 math math: mapArrowRight_id, mapArrowRight_left, mapArrowRight_comp_assoc, CategoryTheory.Functor.leibnizPushout_obj_map, ι_iso_of_iso_right_hom, ι_iso_of_iso_right_inv, mapArrowRight_comp, mapArrowRight_right, CategoryTheory.Functor.leibnizPushout_map_app
ofHasPushout 📖	CompOp	7 math math: ofHasPushout_pt, CategoryTheory.Functor.leibnizPushout_obj_map, CategoryTheory.Functor.leibnizPushout_obj_obj, ofHasPushout_inl, ofHasPushout_inr, CategoryTheory.Functor.leibnizPushout_map_app, ofHasPushout_ι
pt 📖	CompOp	35 math math: inr_ι, flip_pt, mapArrowRight_id, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right, mapArrowRight_left, mapArrowRight_comp_assoc, ofHasPushout_pt, CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff, mapArrowLeft_id, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, isPushout, ι_iso_of_iso_right_hom, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, ι_iso_of_iso_left_inv, inl_ι_assoc, CategoryTheory.Functor.leibnizPushout_obj_obj, ι_iso_of_iso_right_inv, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc, mapArrowLeft_left, mapArrowLeft_right, mapArrowLeft_comp_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, inr_ι_assoc, hom_ext_iff, mapArrowRight_comp, inl_ι, mapArrowRight_right, mapArrowLeft_comp, ι_iso_of_iso_left_hom, CategoryTheory.Functor.leibnizPushout_map_app, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc
ι 📖	CompOp	33 math math: inr_ι, mapArrowRight_id, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right, ι_flip, mapArrowRight_left, mapArrowRight_comp_assoc, CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff, mapArrowLeft_id, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, ι_iso_of_iso_right_hom, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, ι_iso_of_iso_left_inv, inl_ι_assoc, CategoryTheory.Functor.leibnizPushout_obj_obj, ι_iso_of_iso_right_inv, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc, mapArrowLeft_left, mapArrowLeft_right, mapArrowLeft_comp_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, inr_ι_assoc, mapArrowRight_comp, inl_ι, mapArrowRight_right, mapArrowLeft_comp, ι_iso_of_iso_left_hom, CategoryTheory.Functor.leibnizPushout_map_app, ofHasPushout_ι, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc
ι_iso_of_iso_left 📖	CompOp	2 math math: ι_iso_of_iso_left_inv, ι_iso_of_iso_left_hom
ι_iso_of_iso_right 📖	CompOp	2 math math: ι_iso_of_iso_right_hom, ι_iso_of_iso_right_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flip_inl 📖	mathematical	—	inl CategoryTheory.Functor.flip flip inr	—	—
flip_inr 📖	mathematical	—	inr CategoryTheory.Functor.flip flip inl	—	—
flip_pt 📖	mathematical	—	pt CategoryTheory.Functor.flip flip	—	—
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt inl inr	—	—	CategoryTheory.IsPushout.hom_ext isPushout
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt inl inr	—	hom_ext
inl_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt inl ι CategoryTheory.Functor.map	—	CategoryTheory.IsPushout.inl_desc isPushout
inl_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt inl ι CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_ι
inr_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt inr ι CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.IsPushout.inr_desc isPushout
inr_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt inr ι CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_ι
isPushout 📖	mathematical	—	CategoryTheory.IsPushout CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category pt CategoryTheory.NatTrans.app CategoryTheory.Functor.map inl inr	—	—
mapArrowLeft_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowLeft	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.IsPushout.desc.congr_simp hom_ext CategoryTheory.IsPushout.inl_desc_assoc CategoryTheory.IsPushout.inl_desc CategoryTheory.IsPushout.inr_desc_assoc CategoryTheory.IsPushout.inr_desc
mapArrowLeft_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow pt CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapArrowLeft_comp
mapArrowLeft_id 📖	mathematical	—	mapArrowLeft CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.IsPushout.desc.congr_simp hom_ext CategoryTheory.IsPushout.inl_desc CategoryTheory.Category.comp_id CategoryTheory.IsPushout.inr_desc
mapArrowLeft_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id pt CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowLeft CategoryTheory.IsPushout.desc CategoryTheory.NatTrans.app CategoryTheory.Functor.map inl inr CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right	—	—
mapArrowLeft_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id pt CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
mapArrowRight_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowRight	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.IsPushout.desc.congr_simp hom_ext CategoryTheory.IsPushout.inl_desc_assoc CategoryTheory.IsPushout.inl_desc CategoryTheory.IsPushout.inr_desc_assoc CategoryTheory.IsPushout.inr_desc
mapArrowRight_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow pt CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapArrowRight_comp
mapArrowRight_id 📖	mathematical	—	mapArrowRight CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι	—	CategoryTheory.Arrow.hom_ext CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.IsPushout.desc.congr_simp hom_ext CategoryTheory.IsPushout.inl_desc CategoryTheory.Category.comp_id CategoryTheory.IsPushout.inr_desc
mapArrowRight_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id pt CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowRight CategoryTheory.IsPushout.desc CategoryTheory.NatTrans.app CategoryTheory.Functor.map inl inr CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right	—	—
mapArrowRight_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id pt CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι mapArrowRight CategoryTheory.Functor.map	—	—
ofHasPushout_inl 📖	mathematical	—	inl ofHasPushout CategoryTheory.Limits.pushout.inl CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
ofHasPushout_inr 📖	mathematical	—	inr ofHasPushout CategoryTheory.Limits.pushout.inr CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
ofHasPushout_pt 📖	mathematical	—	pt ofHasPushout CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
ofHasPushout_ι 📖	mathematical	—	ι ofHasPushout CategoryTheory.Limits.pushout.desc CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	hom_ext CategoryTheory.IsPushout.inl_desc isPushout CategoryTheory.Limits.colimit.ι_desc CategoryTheory.IsPushout.inr_desc
ι_flip 📖	mathematical	—	ι CategoryTheory.Functor.flip flip	—	CategoryTheory.IsPushout.hom_ext isPushout inl_ι flip_inl inr_ι CategoryTheory.Functor.flip_obj_map flip_inr CategoryTheory.Functor.flip_map_app
ι_iso_of_iso_left_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι ι_iso_of_iso_left mapArrowLeft	—	—
ι_iso_of_iso_left_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι ι_iso_of_iso_left mapArrowLeft	—	—
ι_iso_of_iso_right_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι ι_iso_of_iso_right mapArrowRight	—	—
ι_iso_of_iso_right_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow pt CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category ι ι_iso_of_iso_right mapArrowRight	—	—

---

← Back to Index