Diagonal

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

Statistics

Metric	Count
Definitions diagonalObjPullbackFstIso, diagonal, diagonalObj, pullbackDiagonalMapIdIso, pullbackDiagonalMapIso, hom, inv, pullbackFstFstIso	8
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, 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	60
Total	68

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
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	—	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 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 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.pullback

Definitions

Name	Category	Theorems
diagonal 📖	CompOp	52 math math: CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst, diagonal_snd_assoc, AlgebraicGeometry.diagonal_SpecMap, 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, 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.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, 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	68 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, diagonal_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst, 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.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.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.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

---

← Back to Index