A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ a = b
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h : π' f g w ≫ a = π' f g w ≫ b
⊢ a = b
dsimp [π'] at h
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) a = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) b

case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ Function.Injective fun e => (homologyIsoCokernelLift f g w).inv ≫ e
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ a = b
apply_fun fun e => (homologyIsoCokernelLift f g w).inv ≫ e
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ Function.Injective fun e => (homologyIsoCokernelLift f g w).inv ≫ e

A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) a = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) b
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) a = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) b

case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ Function.Injective fun e => (homologyIsoCokernelLift f g w).inv ≫ e
swap
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv ≫ a =
    cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv ≫ b
⊢ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) a = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) b
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) a = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) b
simp only [Category.assoc] at h
no goals
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv ≫ a =
    cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv ≫ b
⊢ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) a = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) b
exact coequalizer.hom_ext h
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
i j : homology f g w ⟶ W
hh : (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) i = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) j
⊢ i = j
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
⊢ Function.Injective fun e => (homologyIsoCokernelLift f g w).inv ≫ e
intro i j hh
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
i j : homology f g w ⟶ W
hh :
  (homologyIsoCokernelLift f g w).hom ≫ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) i =
    (homologyIsoCokernelLift f g w).hom ≫ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) j
⊢ i = j
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
i j : homology f g w ⟶ W
hh : (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) i = (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) j
⊢ i = j
apply_fun fun e => (homologyIsoCokernelLift f g w).hom ≫ e  at hh
no goals
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : homology f g w ⟶ W
h :
  (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ a =
    (cokernel.π (kernel.lift g f w) ≫ (homologyIsoCokernelLift f g w).inv) ≫ b
i j : homology f g w ⟶ W
hh :
  (homologyIsoCokernelLift f g w).hom ≫ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) i =
    (homologyIsoCokernelLift f g w).hom ≫ (fun e => (homologyIsoCokernelLift f g w).inv ≫ e) j
⊢ i = j
simpa using hh