[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ AddMonoidHom.range f = AddMonoidHom.ker g
[PROOFSTEP]
rw [Abelian.exact_iff' f g (kernelIsLimit _) (cokernelIsColimit _)]
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 0 ∧ Fork.ι (kernelCone g) ≫ Cofork.π (cokernelCocone f) = 0 ↔ AddMonoidHom.range f = AddMonoidHom.ker g
[PROOFSTEP]
exact
  ⟨fun h =>
    ((AddMonoidHom.range_le_ker_iff _ _).mpr h.left).antisymm ((QuotientAddGroup.ker_le_range_iff _ _).mpr h.right),
    fun h => ⟨(AddMonoidHom.range_le_ker_iff _ _).mp h.le, (QuotientAddGroup.ker_le_range_iff _ _).mp h.symm.le⟩⟩
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ PreservesFiniteLimits colim
[PROOFSTEP]
refine Functor.preservesFiniteLimitsOfMapExact _ fun F G H η γ h => (exact_iff _ _).mpr (le_antisymm ?_ ?_)
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.range (colim.map η) ≤ AddMonoidHom.ker (colim.map γ)
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.ker (colim.map γ) ≤ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
all_goals replace h : ∀ j : J, Exact (η.app j) (γ.app j) := fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.range (colim.map η) ≤ AddMonoidHom.ker (colim.map γ)
[PROOFSTEP]
replace h : ∀ j : J, Exact (η.app j) (γ.app j) := fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
[GOAL]
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : Exact η γ
⊢ AddMonoidHom.ker (colim.map γ) ≤ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
replace h : ∀ j : J, Exact (η.app j) (γ.app j) := fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
⊢ AddMonoidHom.range (colim.map η) ≤ AddMonoidHom.ker (colim.map γ)
[PROOFSTEP]
rw [AddMonoidHom.range_le_ker_iff, ← comp_def]
[GOAL]
case refine_1
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
⊢ colim.map η ≫ colim.map γ = 0
[PROOFSTEP]
exact colimit.hom_ext fun j => by simp [reassoc_of% (h j).w]
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
⊢ colimit.ι F j ≫ colim.map η ≫ colim.map γ = colimit.ι F j ≫ 0
[PROOFSTEP]
simp [reassoc_of% (h j).w]
[GOAL]
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
⊢ AddMonoidHom.ker (colim.map γ) ≤ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
intro x (hx : _ = _)
[GOAL]
case refine_2
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
x : ↑(colim.obj G)
hx : ↑(colim.map γ) x = 0
⊢ x ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rcases Concrete.colimit_exists_rep G x with ⟨j, y, rfl⟩
[GOAL]
case refine_2.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx : ↑(colim.map γ) (↑(colimit.ι G j) y) = 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
erw [← comp_apply, colimit.ι_map, comp_apply, ← map_zero (by exact colimit.ι H j : H.obj j →+ ↑(colimit H))] at hx 
[GOAL]
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
⊢ ↑(H.obj j) →+ ↑(colimit H)
[PROOFSTEP]
exact colimit.ι H j
[GOAL]
case refine_2.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rcases Concrete.colimit_exists_of_rep_eq H _ _ hx with ⟨k, e₁, e₂, hk : _ = H.map e₂ 0⟩
[GOAL]
case refine_2.intro.intro.intro.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(H.map e₁) (↑(NatTrans.app γ j) y) = ↑(H.map e₂) 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rw [map_zero, ← comp_apply, ← NatTrans.naturality, comp_apply] at hk 
[GOAL]
case refine_2.intro.intro.intro.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
rcases((exact_iff _ _).mp <| h k).ge hk with ⟨t, ht⟩
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
t : ↑(F.obj k)
ht : ↑(NatTrans.app η k) t = ↑(G.map e₁) y
⊢ ↑(colimit.ι G j) y ∈ AddMonoidHom.range (colim.map η)
[PROOFSTEP]
use colimit.ι F k t
[GOAL]
case h
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
t : ↑(F.obj k)
ht : ↑(NatTrans.app η k) t = ↑(G.map e₁) y
⊢ ↑(colim.map η) (↑(colimit.ι F k) t) = ↑(colimit.ι G j) y
[PROOFSTEP]
erw [← comp_apply, colimit.ι_map, comp_apply, ht]
[GOAL]
case h
X Y Z : AddCommGroupCat
f : X ⟶ Y
g : Y ⟶ Z
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F G H : J ⥤ AddCommGroupCat
η : F ⟶ G
γ : G ⟶ H
h : ∀ (j : J), Exact (NatTrans.app η j) (NatTrans.app γ j)
j : J
y : (forget AddCommGroupCat).obj (G.obj j)
hx✝ : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = 0
hx : ↑(colimit.ι H j) (↑(NatTrans.app γ j) y) = ↑(colimit.ι H j) 0
k : J
e₁ e₂ : j ⟶ k
hk : ↑(NatTrans.app γ k) (↑(G.map e₁) y) = 0
t : ↑(F.obj k)
ht : ↑(NatTrans.app η k) t = ↑(G.map e₁) y
⊢ ↑(colimit.ι G k) (↑(G.map e₁) y) = ↑(colimit.ι G j) y
[PROOFSTEP]
exact colimit.w_apply G e₁ y
