C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
a : Pseudoelement P
⊢ pseudoApply 0 a = 0
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
a : Pseudoelement P
⊢ pseudoApply g (pseudoApply f a) = 0
rw [← comp_apply, h.w]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
a : Pseudoelement P
⊢ pseudoApply 0 a = 0
exact zero_apply _ _
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
have hb' : b.hom ≫ g = 0 := (pseudoZero_iff _).1 hb
case mk
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' (isLimitImage f g h) _ hb'
case mk
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pseudoApply f (Quot.mk (PseudoEqual P) (Over.mk pullback.fst)) = Quotient.mk (setoid Q) b
case mk
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
use (pullback.fst : pullback (Abelian.factorThruImage f) c ⟶ P)
case mk.a
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ (fun g => app f g) (Over.mk pullback.fst) ≈ b
case mk
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pseudoApply f (Quot.mk (PseudoEqual P) (Over.mk pullback.fst)) = Quotient.mk (setoid Q) b
apply Quotient.sound
case mk.a
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ 𝟙 (pullback (Abelian.factorThruImage f) c) ≫ ((fun g => app f g) (Over.mk pullback.fst)).hom = pullback.snd ≫ b.hom
case mk.a
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ (fun g => app f g) (Over.mk pullback.fst) ≈ b
refine'
  ⟨pullback (Abelian.factorThruImage f) c, 𝟙 _, pullback.snd, inferInstance, inferInstance, _⟩
no goals
case mk.a
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ 𝟙 (pullback (Abelian.factorThruImage f) c) ≫ ((fun g => app f g) (Over.mk pullback.fst)).hom = pullback.snd ≫ b.hom
calc
  𝟙 (pullback (Abelian.factorThruImage f) c) ≫ pullback.fst ≫ f = pullback.fst ≫ f :=
    Category.id_comp _
  _ = pullback.fst ≫ Abelian.factorThruImage f ≫ kernel.ι (cokernel.π f) := by
    rw [Abelian.image.fac]
  _ = (pullback.snd ≫ c) ≫ kernel.ι (cokernel.π f) := by
    rw [← Category.assoc, pullback.condition]
  _ = pullback.snd ≫ b.hom := by
    rw [Category.assoc]
    congr
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.fst ≫ f = pullback.fst ≫ Abelian.factorThruImage f ≫ kernel.ι (cokernel.π f)
rw [Abelian.image.fac]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.fst ≫ Abelian.factorThruImage f ≫ kernel.ι (cokernel.π f) = (pullback.snd ≫ c) ≫ kernel.ι (cokernel.π f)
rw [← Category.assoc, pullback.condition]
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.snd ≫ c ≫ kernel.ι (cokernel.π f) = pullback.snd ≫ b.hom
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ (pullback.snd ≫ c) ≫ kernel.ι (cokernel.π f) = pullback.snd ≫ b.hom
rw [Category.assoc]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.snd ≫ c ≫ kernel.ι (cokernel.π f) = pullback.snd ≫ b.hom
congr