Horizontal maps in a pullback square have the same kernel #
Consider a commutative square:
t
X₁ --> X₂
l| |r
v v
X₃ --> X₄
b
- If this is a pullback square, then the induced map
kernel t ⟶ kernel bis an isomorphism. - If this is a pushout square, then the induced map
cokernel t ⟶ cokernel bis an isomorphism.
(Similar results for the (co)kernels of the vertical maps can be obtained by applying these results to the flipped square.)
theorem
CategoryTheory.Limits.isIso_kernel_map_of_isPullback
{C : Type u_1}
[Category.{v_1, u_1} C]
[HasZeroMorphisms C]
{X₁ X₂ X₃ X₄ : C}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
[HasKernel t]
[HasKernel b]
(sq : IsPullback t l r b)
:
IsIso (kernel.map t b l r ⋯)
theorem
CategoryTheory.Limits.isIso_cokernel_map_of_isPushout
{C : Type u_1}
[Category.{v_1, u_1} C]
[HasZeroMorphisms C]
{X₁ X₂ X₃ X₄ : C}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
[HasCokernel t]
[HasCokernel b]
(sq : IsPushout t l r b)
:
IsIso (cokernel.map t b l r ⋯)