Commit 2023-03-24 13:33 896bc69b

View on Github →

feat: port CategoryTheory.Limits.Shapes.Diagonal (#2881)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

added def CategoryTheory.Limits.diagonalObjPullbackFstIso

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst

added theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd

added theorem CategoryTheory.Limits.diagonal_pullback_fst

added def CategoryTheory.Limits.pullback.diagonal

added theorem CategoryTheory.Limits.pullback.diagonal_comp

added theorem CategoryTheory.Limits.pullback.diagonal_fst

added theorem CategoryTheory.Limits.pullback.diagonal_isKernelPair

added theorem CategoryTheory.Limits.pullback.diagonal_snd

added def CategoryTheory.Limits.pullbackDiagonalMapIdIso

added theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd

added theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd

added def CategoryTheory.Limits.pullbackDiagonalMapIso

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso_hom_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso_hom_snd

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso_inv_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_snd

added def CategoryTheory.Limits.pullbackFstFstIso

added theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst

added theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst

added theorem CategoryTheory.Limits.pullback_fst_map_snd_isPullback

added theorem CategoryTheory.Limits.pullback_lift_map_isPullback

added theorem CategoryTheory.Limits.pullback_map_diagonal_isPullback

added theorem CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean