Diagonal

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

Statistics

Metric	Count
Definitions Diagonal, diagonalObjPullbackFstIso, diagonal, diagonalObj, pullbackDiagonalMapIdIso, pullbackDiagonalMapIso, hom, inv, pullbackFstFstIso, codiagonal, codiagonalObj	11
Theorems diagonalObjPullbackFstIso_hom_fst_fst, diagonalObjPullbackFstIso_hom_fst_fst_assoc, diagonalObjPullbackFstIso_hom_fst_snd, diagonalObjPullbackFstIso_hom_fst_snd_assoc, diagonalObjPullbackFstIso_hom_snd, diagonalObjPullbackFstIso_hom_snd_assoc, diagonalObjPullbackFstIso_inv_fst_fst, diagonalObjPullbackFstIso_inv_fst_fst_assoc, diagonalObjPullbackFstIso_inv_fst_snd, diagonalObjPullbackFstIso_inv_fst_snd_assoc, diagonalObjPullbackFstIso_inv_snd_fst, diagonalObjPullbackFstIso_inv_snd_fst_assoc, diagonalObjPullbackFstIso_inv_snd_snd, diagonalObjPullbackFstIso_inv_snd_snd_assoc, diagonal_pullback_fst, isPullback_map_snd_snd, isPushout_map_codiagonal, comp_diagonal, comp_diagonal_assoc, diagonal_comp, diagonal_fst, diagonal_fst_assoc, diagonal_isKernelPair, diagonal_snd, diagonal_snd_assoc, instIsIsoDiagonalOfMono, instIsSplitEpiFst, instIsSplitEpiSnd, instIsSplitMonoDiagonal, isIso_diagonal_iff, pullbackDiagonalMapIdIso_hom_fst, pullbackDiagonalMapIdIso_hom_fst_assoc, pullbackDiagonalMapIdIso_hom_snd, pullbackDiagonalMapIdIso_hom_snd_assoc, pullbackDiagonalMapIdIso_inv_fst, pullbackDiagonalMapIdIso_inv_fst_assoc, pullbackDiagonalMapIdIso_inv_snd_fst, pullbackDiagonalMapIdIso_inv_snd_fst_assoc, pullbackDiagonalMapIdIso_inv_snd_snd, pullbackDiagonalMapIdIso_inv_snd_snd_assoc, hom_fst, hom_fst_assoc, hom_snd, hom_snd_assoc, inv_fst, inv_fst_assoc, inv_snd_fst, inv_snd_fst_assoc, inv_snd_snd, inv_snd_snd_assoc, pullbackFstFstIso_hom, pullbackFstFstIso_inv, pullback_diagonal_map_snd_fst_fst, pullback_diagonal_map_snd_fst_fst_assoc, pullback_diagonal_map_snd_snd_fst, pullback_diagonal_map_snd_snd_fst_assoc, pullback_fst_map_snd_isPullback, pullback_lift_diagonal_isPullback, pullback_lift_map_isPullback, pullback_map_diagonal_isPullback, pullback_map_eq_pullbackFstFstIso_inv, inl_codiagonal, inl_codiagonal_assoc, inr_codiagonal, inr_codiagonal_assoc, instIsIsoCodiagonalOfEpi, instIsSplitEpiCodiagonal, instIsSplitMonoInl, instIsSplitMonoInr, isIso_codiagonal_iff, op_codiagonal	71
Total	82

CategoryTheory.Limits

Definitions

Name	Category	Theorems
diagonalObjPullbackFstIso 📖	CompOp	15 math math: diagonalObjPullbackFstIso_inv_snd_snd_assoc, diagonalObjPullbackFstIso_inv_fst_snd_assoc, diagonalObjPullbackFstIso_inv_fst_fst, diagonalObjPullbackFstIso_hom_snd, diagonalObjPullbackFstIso_inv_snd_fst, diagonalObjPullbackFstIso_hom_fst_fst_assoc, diagonalObjPullbackFstIso_inv_snd_snd, diagonalObjPullbackFstIso_inv_snd_fst_assoc, diagonalObjPullbackFstIso_hom_fst_snd, diagonalObjPullbackFstIso_inv_fst_fst_assoc, diagonalObjPullbackFstIso_hom_fst_snd_assoc, diagonalObjPullbackFstIso_hom_snd_assoc, diagonalObjPullbackFstIso_hom_fst_fst, diagonalObjPullbackFstIso_inv_fst_snd, diagonal_pullback_fst
pullbackDiagonalMapIdIso 📖	CompOp	11 math math: pullbackDiagonalMapIdIso_inv_snd_fst_assoc, pullbackDiagonalMapIdIso_inv_snd_fst, pullbackDiagonalMapIdIso_inv_snd_snd_assoc, pullbackDiagonalMapIdIso_inv_fst, pullbackDiagonalMapIdIso_inv_fst_assoc, pullbackDiagonalMapIdIso_hom_fst_assoc, pullback.diagonal_comp, pullbackDiagonalMapIdIso_inv_snd_snd, pullbackDiagonalMapIdIso_hom_snd_assoc, pullbackDiagonalMapIdIso_hom_snd, pullbackDiagonalMapIdIso_hom_fst
pullbackDiagonalMapIso 📖	CompOp	10 math math: pullbackDiagonalMapIso.hom_fst, pullbackDiagonalMapIso.inv_fst_assoc, pullbackDiagonalMapIso.hom_snd_assoc, pullbackDiagonalMapIso.hom_snd, pullbackDiagonalMapIso.inv_snd_fst, pullbackDiagonalMapIso.inv_fst, pullbackDiagonalMapIso.inv_snd_fst_assoc, pullbackDiagonalMapIso.inv_snd_snd_assoc, pullbackDiagonalMapIso.hom_fst_assoc, pullbackDiagonalMapIso.inv_snd_snd
pullbackFstFstIso 📖	CompOp	3 math math: pullbackFstFstIso_hom, pullback_map_eq_pullbackFstFstIso_inv, pullbackFstFstIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonalObjPullbackFstIso_hom_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.snd hasPullbackHorizPaste CategoryTheory.Iso.hom diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackHorizPaste CategoryTheory.Category.assoc limit.lift_π_assoc CategoryTheory.Category.comp_id pullbackSymmetry_hom_comp_fst_assoc pullbackAssoc_hom_snd_fst pullbackRightPullbackFstIso_hom_fst_assoc
diagonalObjPullbackFstIso_hom_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.snd hasPullbackHorizPaste CategoryTheory.Iso.hom diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackHorizPaste CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_hom_fst_fst
diagonalObjPullbackFstIso_hom_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.snd hasPullbackHorizPaste CategoryTheory.Iso.hom diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackHorizPaste CategoryTheory.Category.assoc limit.lift_π_assoc CategoryTheory.Category.comp_id pullbackSymmetry_hom_comp_fst_assoc pullbackAssoc_hom_snd_snd limit.lift_π pullbackRightPullbackFstIso_hom_snd
diagonalObjPullbackFstIso_hom_fst_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.snd hasPullbackHorizPaste CategoryTheory.Iso.hom diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackHorizPaste CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_hom_fst_snd
diagonalObjPullbackFstIso_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.snd hasPullbackHorizPaste CategoryTheory.Iso.hom diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackHorizPaste CategoryTheory.Category.assoc limit.lift_π CategoryTheory.Category.comp_id pullbackSymmetry_hom_comp_snd pullbackAssoc_hom_fst limit.lift_π_assoc pullbackRightPullbackFstIso_hom_fst_assoc
diagonalObjPullbackFstIso_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.snd hasPullbackHorizPaste CategoryTheory.Iso.hom diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackHorizPaste CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_hom_snd
diagonalObjPullbackFstIso_inv_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.congrHom_inv CategoryTheory.Category.assoc hasPullback_symmetry pullbackRightPullbackFstIso_inv_fst_assoc limit.lift_π_assoc CategoryTheory.Category.comp_id pullbackAssoc_inv_fst_fst pullbackSymmetry_inv_comp_fst limit.lift_π
diagonalObjPullbackFstIso_inv_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_inv_fst_fst
diagonalObjPullbackFstIso_inv_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.congrHom_inv CategoryTheory.Category.assoc hasPullback_symmetry pullbackRightPullbackFstIso_inv_fst_assoc limit.lift_π_assoc CategoryTheory.Category.comp_id pullbackAssoc_inv_fst_snd pullbackSymmetry_inv_comp_snd_assoc
diagonalObjPullbackFstIso_inv_fst_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_inv_fst_snd
diagonalObjPullbackFstIso_inv_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.congrHom_inv CategoryTheory.Category.assoc hasPullback_symmetry pullbackRightPullbackFstIso_inv_snd_fst limit.lift_π_assoc CategoryTheory.Category.comp_id pullbackAssoc_inv_fst_fst pullbackSymmetry_inv_comp_fst limit.lift_π
diagonalObjPullbackFstIso_inv_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_inv_snd_fst
diagonalObjPullbackFstIso_inv_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.congrHom_inv CategoryTheory.Category.assoc hasPullback_symmetry pullbackRightPullbackFstIso_inv_snd_snd limit.lift_π CategoryTheory.Category.comp_id pullbackAssoc_inv_snd pullbackSymmetry_inv_comp_snd_assoc limit.lift_π_assoc
diagonalObjPullbackFstIso_inv_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.fst CategoryTheory.Iso.inv diagonalObjPullbackFstIso	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagonalObjPullbackFstIso_inv_snd_snd
diagonal_pullback_fst 📖	mathematical	—	pullback.diagonal pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom hasPullback_symmetry pullback.diagonalObj CategoryTheory.Iso.hom pullbackSymmetry CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback pullback.snd CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map CategoryTheory.Over.homMk CategoryTheory.Iso.inv hasPullbackHorizPaste diagonalObjPullbackFstIso	—	pullback.hom_ext hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullback_symmetry hasPullbackHorizPaste pullback.diagonal_fst CategoryTheory.Category.id_comp CategoryTheory.Category.assoc diagonalObjPullbackFstIso_inv_fst_fst limit.lift_π pullbackSymmetry_hom_comp_snd diagonalObjPullbackFstIso_inv_fst_snd limit.lift_π_assoc CategoryTheory.Category.comp_id pullbackSymmetry_hom_comp_fst pullback.diagonal_snd diagonalObjPullbackFstIso_inv_snd_fst diagonalObjPullbackFstIso_inv_snd_snd
isPullback_map_snd_snd 📖	mathematical	—	CategoryTheory.IsPullback pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst CategoryTheory.IsPullback.instHasPullbackFst pullback.map pullback.snd pullback.condition	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst pullback.condition limit.lift_π CategoryTheory.CommSq.w CategoryTheory.Category.assoc PullbackCone.condition_assoc pullback.hom_ext limit.lift_π_assoc PullbackCone.condition pullback.lift.congr_simp
isPushout_map_codiagonal 📖	mathematical	—	CategoryTheory.IsPushout pushout hasColimitOfHasColimitsOfShape WalkingSpan WidePushoutShape.category WalkingPair span CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasPushoutVertPaste instHasPushoutComp pushout.inr pushout.inl pushout.map CategoryTheory.CategoryStruct.id pushout.codiagonal	—	hasColimitOfHasColimitsOfShape hasPushoutVertPaste instHasPushoutComp CategoryTheory.IsPullback.op_iff instHasPushoutUnopOfHasPullbackOpposite instHasPullbackOppositeOpOfHasPushout op_pushoutMap pushout.op_codiagonal CategoryTheory.IsPullback.of_iso hasPullbackHorizPaste hasPullbackVertPaste hasLimitOfHasLimitsOfShape hasPullbacks_opposite CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id pullback_map_diagonal_isPullback pullbackIsoOpPushout_inv_fst_assoc CategoryTheory.Iso.hom_inv_id_assoc
pullbackDiagonalMapIdIso_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom pullbackDiagonalMapIdIso pullback.fst pullback.snd	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc hasLimitOfHasLimitsOfShape hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst limit.lift_π pullbackDiagonalMapIso.hom_fst limit.lift_π_assoc
pullbackDiagonalMapIdIso_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom pullbackDiagonalMapIdIso pullback.fst pullback.snd	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackDiagonalMapIdIso_hom_fst
pullbackDiagonalMapIdIso_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom pullbackDiagonalMapIdIso pullback.snd	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc hasLimitOfHasLimitsOfShape hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst limit.lift_π pullbackDiagonalMapIso.hom_snd limit.lift_π_assoc
pullbackDiagonalMapIdIso_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom pullbackDiagonalMapIdIso pullback.snd	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackDiagonalMapIdIso_hom_snd
pullbackDiagonalMapIdIso_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv pullbackDiagonalMapIdIso pullback.fst	—	CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_comp_eq pullback.diagonal_fst pullback.condition_assoc limit.lift_π pullbackDiagonalMapIdIso_hom_fst_assoc
pullbackDiagonalMapIdIso_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv pullbackDiagonalMapIdIso pullback.fst	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackDiagonalMapIdIso_inv_fst
pullbackDiagonalMapIdIso_inv_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv pullbackDiagonalMapIdIso pullback.snd pullback.fst	—	CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_comp_eq pullbackDiagonalMapIdIso_hom_fst
pullbackDiagonalMapIdIso_inv_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv pullbackDiagonalMapIdIso pullback.snd pullback.fst	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackDiagonalMapIdIso_inv_snd_fst
pullbackDiagonalMapIdIso_inv_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv pullbackDiagonalMapIdIso pullback.snd	—	CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_comp_eq pullbackDiagonalMapIdIso_hom_snd
pullbackDiagonalMapIdIso_inv_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.diagonalObj pullback.diagonal pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv pullbackDiagonalMapIdIso pullback.snd	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackDiagonalMapIdIso_inv_snd_snd
pullbackFstFstIso_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.hom pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst pullback.snd CategoryTheory.IsPullback.instHasPullbackFst pullbackFstFstIso pullback.lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst
pullbackFstFstIso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.inv pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst pullback.snd CategoryTheory.IsPullback.instHasPullbackFst pullbackFstFstIso pullback.lift pullback.map	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst
pullback_diagonal_map_snd_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.diagonalObj pullback.diagonal pullback.map pullback.fst	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id pullback.diagonal_fst pullback.condition_assoc pullback.lift_fst
pullback_diagonal_map_snd_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.diagonalObj pullback.diagonal pullback.map pullback.fst	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullback_diagonal_map_snd_fst_fst
pullback_diagonal_map_snd_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.diagonalObj pullback.diagonal pullback.map pullback.fst	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id pullback.diagonal_snd pullback.condition_assoc pullback.lift_snd
pullback_diagonal_map_snd_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.snd hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.diagonalObj pullback.diagonal pullback.map pullback.fst	—	hasLimitOfHasLimitsOfShape hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullback_diagonal_map_snd_snd_fst
pullback_fst_map_snd_isPullback 📖	mathematical	—	CategoryTheory.IsPullback pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.snd hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst pullback.diagonalObj pullback.fst pullback.map CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.id_comp pullback.diagonal	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.of_iso_pullback hasPullbackHorizPaste hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.id_comp pullback.hom_ext pullback.condition_assoc CategoryTheory.Category.assoc pullback.diagonal_fst CategoryTheory.Category.comp_id limit.lift_π limit.lift_π_assoc pullback.diagonal_snd pullbackDiagonalMapIso.inv_fst pullbackDiagonalMapIso.inv_snd_fst pullbackDiagonalMapIso.inv_snd_snd
pullback_lift_diagonal_isPullback 📖	mathematical	—	CategoryTheory.IsPullback pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasPullbackHorizPaste hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan CategoryTheory.IsPullback.instHasPullbackFst pullback.diagonalObj pullback.lift CategoryTheory.CategoryStruct.id pullback.diagonal pullback.map	—	hasPullbackHorizPaste hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst hasPullbackVertPaste CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id pullback.hom_ext limit.lift_π pullback.congrHom_inv CategoryTheory.Category.assoc limit.lift_π_assoc pullback.map_isIso CategoryTheory.IsIso.id CategoryTheory.Iso.isIso_inv CategoryTheory.IsPullback.of_iso_pullback pullback.diagonal_fst pullback.diagonal_snd pullback_fst_iso_of_right_iso CategoryTheory.Iso.trans_assoc pullbackDiagonalMapIdIso_inv_fst CategoryTheory.IsIso.inv_hom_id_assoc pullback.map.congr_simp CategoryTheory.asIso.congr_simp pullbackDiagonalMapIdIso_inv_snd_fst CategoryTheory.IsIso.inv_hom_id pullbackDiagonalMapIdIso_inv_snd_snd pullback_inv_fst_snd_of_right_isIso CategoryTheory.IsIso.inv_id
pullback_lift_map_isPullback 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsPullback pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.fst pullback.snd pullback.lift pullback.map pullback.lift_fst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.lift_snd	—	CategoryTheory.IsPullback.of_iso_pullback hasLimitOfHasLimitsOfShape pullback.lift_fst pullback.lift_snd CategoryTheory.IsPullback.instHasPullbackFst limit.lift_π
pullback_map_diagonal_isPullback 📖	mathematical	—	CategoryTheory.IsPullback pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback.diagonalObj pullback.fst pullback.map CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.id_comp pullback.diagonal CategoryTheory.Category.comp_id	—	CategoryTheory.Category.comp_id CategoryTheory.IsPullback.of_iso_pullback CategoryTheory.Category.id_comp pullback.hom_ext pullback.condition CategoryTheory.Category.assoc pullback.diagonal_fst limit.lift_π limit.lift_π_assoc pullback.diagonal_snd pullbackDiagonalMapIdIso_inv_fst pullbackDiagonalMapIdIso_inv_snd_fst pullbackDiagonalMapIdIso_inv_snd_snd
pullback_map_eq_pullbackFstFstIso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pullback.map hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback pullback.fst pullback.snd CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Iso.inv pullbackFstFstIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst pullback.lift_snd_assoc pullback.lift_fst

CategoryTheory.Limits.ChosenPullback

Definitions

Name	Category	Theorems
Diagonal 📖	CompOp	1 math math: instNonemptyDiagonal

CategoryTheory.Limits.pullback

Definitions

Name	Category	Theorems
diagonal 📖	CompOp	57 math math: CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst, AlgebraicGeometry.weaklyEtale_iff, diagonal_snd_assoc, AlgebraicGeometry.diagonal_SpecMap, AlgebraicGeometry.isAffineHom_diagonal_iff, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc, AlgebraicGeometry.UniversallyInjective.iff_diagonal, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc, diagonal_snd, instIsIsoDiagonalOfMono, AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion, comp_diagonal_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, AlgebraicGeometry.WeaklyEtale.flat_diagonal, CategoryTheory.Limits.pullback_lift_diagonal_isPullback, AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact, AlgebraicGeometry.IsImmersion.instDiagonalScheme, AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal, diagonal_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc, AlgebraicGeometry.isSeparated_iff, CategoryTheory.Limits.pullback_map_diagonal_isPullback, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst, comp_diagonal, isIso_diagonal_iff, diagonal_fst_assoc, AlgebraicGeometry.quasiSeparated_iff, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc, diagonal_comp, CategoryTheory.Limits.pushout.op_codiagonal, CategoryTheory.MorphismProperty.diagonal_iff, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc, AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc, AlgebraicGeometry.diagonal_Spec_map, AlgebraicGeometry.WeaklyEtale.instDiagonalScheme, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd, CategoryTheory.Limits.pullback_fst_map_snd_isPullback, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd, CategoryTheory.Limits.diagonal_pullback_fst, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, instIsSplitMonoDiagonal
diagonalObj 📖	CompOp	73 math math: CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc, AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst, AlgebraicGeometry.weaklyEtale_iff, diagonal_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst, AlgebraicGeometry.isAffineHom_diagonal_iff, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc, AlgebraicGeometry.UniversallyInjective.iff_diagonal, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst, diagonal_snd, instIsIsoDiagonalOfMono, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc, AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion, comp_diagonal_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd, AlgebraicGeometry.WeaklyEtale.flat_diagonal, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, CategoryTheory.Limits.pullback_lift_diagonal_isPullback, AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact, AlgebraicGeometry.IsImmersion.instDiagonalScheme, AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal, diagonal_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc, AlgebraicGeometry.isSeparated_iff, CategoryTheory.Limits.pullback_map_diagonal_isPullback, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst, comp_diagonal, isIso_diagonal_iff, diagonal_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd, AlgebraicGeometry.quasiSeparated_iff, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc, diagonal_comp, CategoryTheory.Limits.pushout.op_codiagonal, CategoryTheory.MorphismProperty.diagonal_iff, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc, AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc, AlgebraicGeometry.WeaklyEtale.instDiagonalScheme, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd, CategoryTheory.Limits.pullback_fst_map_snd_isPullback, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd, CategoryTheory.Limits.diagonal_pullback_fst, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, instIsSplitMonoDiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_diagonal 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct diagonalObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan diagonal CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullback snd CategoryTheory.IsPullback.instHasPullbackFst map CategoryTheory.CategoryStruct.id	—	hom_ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc diagonal_fst CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.lift_π diagonal_fst_assoc diagonal_snd diagonal_snd_assoc
comp_diagonal_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct diagonalObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan diagonal CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullback snd CategoryTheory.IsPullback.instHasPullbackFst map CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_diagonal
diagonal_comp 📖	mathematical	—	diagonal CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback snd CategoryTheory.IsPullback.instHasPullbackFst diagonalObj map CategoryTheory.CategoryStruct.id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIdIso	—	hom_ext CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id diagonal_fst CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst diagonal_snd CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd
diagonal_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct diagonalObj diagonal fst CategoryTheory.CategoryStruct.id	—	lift_fst
diagonal_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct diagonalObj diagonal fst	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' diagonal_fst
diagonal_isKernelPair 📖	mathematical	—	CategoryTheory.IsKernelPair CategoryTheory.Limits.pullback fst snd	—	CategoryTheory.IsPullback.of_hasPullback
diagonal_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct diagonalObj diagonal snd CategoryTheory.CategoryStruct.id	—	lift_snd
diagonal_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct diagonalObj diagonal snd	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' diagonal_snd
instIsIsoDiagonalOfMono 📖	mathematical	—	CategoryTheory.IsIso diagonalObj diagonal	—	CategoryTheory.Limits.isIso_fst_of_mono CategoryTheory.IsIso.inv_eq_of_inv_hom_id diagonal_fst CategoryTheory.IsIso.inv_isIso
instIsSplitEpiFst 📖	mathematical	—	CategoryTheory.IsSplitEpi CategoryTheory.Limits.pullback fst	—	diagonal_fst
instIsSplitEpiSnd 📖	mathematical	—	CategoryTheory.IsSplitEpi CategoryTheory.Limits.pullback snd	—	diagonal_snd
instIsSplitMonoDiagonal 📖	mathematical	—	CategoryTheory.IsSplitMono diagonalObj diagonal	—	diagonal_fst
isIso_diagonal_iff 📖	mathematical	—	CategoryTheory.IsIso diagonalObj diagonal CategoryTheory.Mono	—	lift_fst CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso diagonal_fst diagonal_snd lift_snd instIsIsoDiagonalOfMono

CategoryTheory.Limits.pullbackDiagonalMapIso

Definitions

Name	Category	Theorems
hom 📖	CompOp	—
inv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.limit.lift_π
hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_fst
hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.limit.lift_π
hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_snd
inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.limit.lift_π
inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_fst
inv_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id
inv_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_snd_fst
inv_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id
inv_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv CategoryTheory.Limits.pullbackDiagonalMapIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_snd_snd

CategoryTheory.Limits.pushout

Definitions

Name	Category	Theorems
codiagonal 📖	CompOp	9 math math: instIsIsoCodiagonalOfEpi, inr_codiagonal, instIsSplitEpiCodiagonal, isIso_codiagonal_iff, CategoryTheory.Limits.isPushout_map_codiagonal, inl_codiagonal, op_codiagonal, inr_codiagonal_assoc, inl_codiagonal_assoc
codiagonalObj 📖	CompOp	4 math math: instIsIsoCodiagonalOfEpi, instIsSplitEpiCodiagonal, isIso_codiagonal_iff, op_codiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl_codiagonal 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inl codiagonal CategoryTheory.CategoryStruct.id	—	inl_desc
inl_codiagonal_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inl codiagonal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inl_codiagonal
inr_codiagonal 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inr codiagonal CategoryTheory.CategoryStruct.id	—	inr_desc
inr_codiagonal_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inr codiagonal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inr_codiagonal
instIsIsoCodiagonalOfEpi 📖	mathematical	—	CategoryTheory.IsIso codiagonalObj codiagonal	—	CategoryTheory.Limits.isIso_inl_of_epi CategoryTheory.IsIso.inv_eq_of_hom_inv_id inl_codiagonal CategoryTheory.IsIso.inv_isIso
instIsSplitEpiCodiagonal 📖	mathematical	—	CategoryTheory.IsSplitEpi codiagonalObj codiagonal	—	inl_codiagonal
instIsSplitMonoInl 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.Limits.pushout inl	—	inl_codiagonal
instIsSplitMonoInr 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.Limits.pushout inr	—	inr_codiagonal
isIso_codiagonal_iff 📖	mathematical	—	CategoryTheory.IsIso codiagonalObj codiagonal CategoryTheory.Epi	—	inl_desc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso inl_codiagonal inr_codiagonal inr_desc instIsIsoCodiagonalOfEpi
op_codiagonal 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct codiagonalObj codiagonal CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Category.opposite CategoryTheory.Limits.instHasPullbackOppositeOpOfHasPushout CategoryTheory.Limits.pushout Opposite.unop Quiver.Hom.unop CategoryTheory.Limits.instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Limits.pullback.diagonal CategoryTheory.Iso.hom CategoryTheory.Limits.pullback CategoryTheory.Limits.pullbackIsoOpPushout	—	CategoryTheory.Limits.instHasPullbackOppositeOpOfHasPushout CategoryTheory.Limits.instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Iso.comp_inv_eq CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst inl_codiagonal CategoryTheory.Limits.pullback.diagonal_fst CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd inr_codiagonal CategoryTheory.Limits.pullback.diagonal_snd

---

← Back to Index