no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
a : Pseudoelement P
⊢ pseudoApply (f ≫ g) a = 0
rw [comp_apply, h₁ a]
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
⊢ kernel.ι g ≫ cokernel.π f = 0
have : g (kernel.ι g) = 0 := apply_eq_zero_of_comp_eq_zero _ _ (kernel.condition _)
case intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
ha : pseudoApply f a' = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
⊢ kernel.ι g ≫ cokernel.π f = 0
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
obtain ⟨a', ha⟩ := h₂ _ this
case intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
ha : pseudoApply f a' = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
a : Over P
ha' : Quotient.mk (setoid P) a = a'
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
ha : pseudoApply f a' = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
⊢ kernel.ι g ≫ cokernel.π f = 0
obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
case intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
ha : pseudoApply f a' = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
a : Over P
ha' : Quotient.mk (setoid P) a = a'
⊢ kernel.ι g ≫ cokernel.π f = 0
rw [← ha'] at ha
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
⊢ kernel.ι g ≫ cokernel.π f = 0
obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ kernel.ι g ≫ cokernel.π f = 0
obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π f)) (kernel.ι g) _
  (r ≫ a.hom ≫ Abelian.factorThruImage f) q (by
    simp only [Category.assoc, Abelian.image.fac]
    exact comm)
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
⊢ kernel.ι g ≫ cokernel.π f = 0
let j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
⊢ kernel.ι g ≫ cokernel.π f = 0
haveI pe : Epi j := epi_of_epi_fac hz₂
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this✝ : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
this : IsIso j
⊢ kernel.ι g ≫ cokernel.π f = 0
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
⊢ kernel.ι g ≫ cokernel.π f = 0
haveI : IsIso j := isIso_of_mono_of_epi _
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this✝ : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst ≫ kernel.ι (cokernel.π f)) ≫ cokernel.π f = 0
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this✝ : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
this : IsIso j
⊢ kernel.ι g ≫ cokernel.π f = 0
rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
no goals
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this✝ : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst ≫ kernel.ι (cokernel.π f)) ≫ cokernel.π f = 0
simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ r ≫ a.hom ≫ f = q ≫ kernel.ι g
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ (r ≫ a.hom ≫ Abelian.factorThruImage f) ≫ kernel.ι (cokernel.π f) = q ≫ kernel.ι g
simp only [Category.assoc, Abelian.image.fac]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ r ≫ a.hom ≫ f = q ≫ kernel.ι g
exact comm