OverAdjunction

📁 Source: Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

Statistics

Metric	Count
Definitions map, mapComp, mapCongr, mapId, mapPullbackAdj, pullback, pullbackComp, pullbackCongr, pullbackMapHomPullback	9
Theorems mapComp_hom_app_left, mapComp_inv_app_left, mapCongr_hom_app_left, mapCongr_inv_app_left, mapId_hom_app_left, mapId_inv_app_left, mapPullbackAdj_counit_app, mapPullbackAdj_unit_app, map_comp, map_map_left, map_obj_hom, map_obj_left, pullbackComp_hom_app_left, pullbackComp_inv_app_left, pullbackComp_left_fst_fst, pullbackCongr_hom_app_left_fst, pullbackCongr_hom_app_left_fst_assoc, pullbackMapHomPullback_app, pullback_map_left, pullback_obj_hom, pullback_obj_left, instHasPullbackHomDiscretePUnitOfHasPullbacksAlong, instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong	24
Total	33

CategoryTheory.MorphismProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasPullbackHomDiscretePUnitOfHasPullbacksAlong 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	HasPullbacksAlong.hasPullback Comma.prop
instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.Comma.hom instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.pullback.snd	—	HasPullbacksAlong.hasPullback instHasPullbackHomDiscretePUnitOfHasPullbacksAlong IsStableUnderBaseChangeAlong.of_isPullback CategoryTheory.IsPullback.of_hasPullback Comma.prop
instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop Over.map	—	CategoryTheory.Adjunction.isLeftAdjoint IsMultiplicative.instTop instIsStableUnderBaseChangeTop instHasOfPostcompPropertyTop

CategoryTheory.MorphismProperty.Over

Definitions

Name	Category	Theorems
map 📖	CompOp	23 math math: map_obj_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, mapCongr_inv_app_left, pullbackMapHomPullback_app, map_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, mapPullbackAdj_counit_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, map_comp, mapPullbackAdj_unit_app, mapId_inv_app_left, mapCongr_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, mapComp_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, mapComp_inv_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, mapId_hom_app_left, map_obj_hom
mapComp 📖	CompOp	3 math math: mapComp_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, mapComp_inv_app_left
mapCongr 📖	CompOp	2 math math: mapCongr_inv_app_left, mapCongr_hom_app_left
mapId 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, mapId_inv_app_left, mapId_hom_app_left
mapPullbackAdj 📖	CompOp	2 math math: mapPullbackAdj_counit_app, mapPullbackAdj_unit_app
pullback 📖	CompOp	21 math math: pullbackComp_hom_app_left, pullbackMapHomPullback_app, pullback_obj_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, pullbackCongr_hom_app_left_fst, mapPullbackAdj_counit_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, instPreservesFiniteLimitsTopPullback, mapPullbackAdj_unit_app, pullbackComp_inv_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, pullback_map_left, pullback_obj_hom, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, pullbackComp_left_fst_fst, pullbackCongr_hom_app_left_fst_assoc
pullbackComp 📖	CompOp	3 math math: pullbackComp_hom_app_left, pullbackComp_inv_app_left, pullbackComp_left_fst_fst
pullbackCongr 📖	CompOp	2 math math: pullbackCongr_hom_app_left_fst, pullbackCongr_hom_app_left_fst_assoc
pullbackMapHomPullback 📖	CompOp	1 math math: pullbackMapHomPullback_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapComp_hom_app_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory map CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category mapComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mapComp_inv_app_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Functor.comp map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category mapComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mapCongr_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category mapCongr CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mapCongr_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category mapCongr CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mapId_hom_app_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category mapId CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mapId_inv_app_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category mapId CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mapPullbackAdj_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.comp pullback map CategoryTheory.Adjunction.counit CategoryTheory.MorphismProperty.IsMultiplicative.instTop mapPullbackAdj homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right CategoryTheory.Category.id_comp	—	homMk.congr_simp CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Category.id_comp
mapPullbackAdj_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.comp map pullback CategoryTheory.Adjunction.unit CategoryTheory.MorphismProperty.IsMultiplicative.instTop mapPullbackAdj homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.lift CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.CategoryStruct.id	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.comp_mem CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.IsMultiplicative.instTop	—	CategoryTheory.Functor.ext CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.Comma.Hom.prop_hom_left CategoryTheory.MorphismProperty.Comma.Hom.prop_hom_right CategoryTheory.Category.assoc Hom.ext CategoryTheory.MorphismProperty.Comma.eqToHom_left CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop map CategoryTheory.MorphismProperty.Comma.Hom.hom	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
map_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop map CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
map_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop map	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
pullbackComp_hom_app_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory pullback CategoryTheory.Functor.comp CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category pullbackComp CategoryTheory.Limits.pullback CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackLeftPullbackSndIso CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
pullbackComp_inv_app_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Functor.comp pullback CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.category pullbackComp CategoryTheory.Limits.pullback CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.pullback.snd CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackLeftPullbackSndIso CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id	—	CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.Limits.pullback.congrHom_inv
pullbackComp_left_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop pullback CategoryTheory.Functor.comp CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackComp CategoryTheory.Limits.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.MorphismProperty.instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong CategoryTheory.MorphismProperty.instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullback.map_id CategoryTheory.Category.id_comp CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst
pullbackCongr_hom_app_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop pullback CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackCongr CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.pullback.map_id CategoryTheory.Category.id_comp
pullbackCongr_hom_app_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop pullback CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackCongr CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackCongr_hom_app_left_fst
pullbackMapHomPullback_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp pullback CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks map pullbackMapHomPullback homMk CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.map CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks
pullback_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.Limits.pullback.snd CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop pullback CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.MorphismProperty.IsMultiplicative.instTop
pullback_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop pullback CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.left CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong	—	CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong CategoryTheory.MorphismProperty.IsMultiplicative.instTop
pullback_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop pullback CategoryTheory.Limits.pullback CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop

---

← Back to Index