[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Epi (imageToKernel f g hfg)
[PROOFSTEP]
set ψ : (kernelSubobject g : 𝒜) ⟶ imageSubobject f := Subobject.arrow _ ≫ φ ≫ factorThruImageSubobject f
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Epi (imageToKernel f g hfg)
[PROOFSTEP]
suffices : ψ ≫ imageToKernel f g hfg = 𝟙 _
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
this : ψ ≫ imageToKernel f g hfg = 𝟙 (Subobject.underlying.obj (kernelSubobject g))
⊢ Epi (imageToKernel f g hfg)
[PROOFSTEP]
exact epi_of_epi_fac this
[GOAL]
case this
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ ψ ≫ imageToKernel f g hfg = 𝟙 (Subobject.underlying.obj (kernelSubobject g))
[PROOFSTEP]
rw [← cancel_mono (Subobject.arrow _)]
[GOAL]
case this
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ (ψ ≫ imageToKernel f g hfg) ≫ Subobject.arrow (kernelSubobject g) =
    𝟙 (Subobject.underlying.obj (kernelSubobject g)) ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp only [imageToKernel_arrow, imageSubobject_arrow_comp, Category.id_comp, Category.assoc]
[GOAL]
case this
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Subobject.arrow (kernelSubobject g) ≫ φ ≫ f = Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
calc
  (kernelSubobject g).arrow ≫ φ ≫ f = (kernelSubobject g).arrow ≫ 𝟙 B :=
    by
    rw [← H, Preadditive.comp_add]
    simp only [add_zero, zero_comp, kernelSubobject_arrow_comp_assoc]
  _ = (kernelSubobject g).arrow := Category.comp_id _
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Subobject.arrow (kernelSubobject g) ≫ φ ≫ f = Subobject.arrow (kernelSubobject g) ≫ 𝟙 B
[PROOFSTEP]
rw [← H, Preadditive.comp_add]
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Subobject.arrow (kernelSubobject g) ≫ φ ≫ f =
    Subobject.arrow (kernelSubobject g) ≫ φ ≫ f + Subobject.arrow (kernelSubobject g) ≫ g ≫ χ
[PROOFSTEP]
simp only [add_zero, zero_comp, kernelSubobject_arrow_comp_assoc]
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
h : Split f g
⊢ Exact f g
[PROOFSTEP]
obtain ⟨φ, χ, -, -, h1, -, h2⟩ := h
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ g = 0
h2 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Exact f g
[PROOFSTEP]
exact exact_of_split h1 h2
[GOAL]
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
h : Split f g
⊢ Split (F.map f) (F.map g)
[PROOFSTEP]
obtain ⟨φ, χ, h1, h2, h3, h4, h5⟩ := h
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Split (F.map f) (F.map g)
[PROOFSTEP]
refine ⟨⟨F.map φ, F.map χ, ?_⟩⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ F.map f ≫ F.map φ = 𝟙 (F.obj A) ∧
    F.map χ ≫ F.map g = 𝟙 (F.obj C) ∧
      F.map f ≫ F.map g = 0 ∧ F.map χ ≫ F.map φ = 0 ∧ F.map φ ≫ F.map f + F.map g ≫ F.map χ = 𝟙 (F.obj B)
[PROOFSTEP]
simp only [← F.map_comp, ← F.map_id]
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ F.map (f ≫ φ) = F.map (𝟙 A) ∧
    F.map (χ ≫ g) = F.map (𝟙 C) ∧ F.map (f ≫ g) = 0 ∧ F.map (χ ≫ φ) = 0 ∧ F.map (φ ≫ f) + F.map (g ≫ χ) = F.map (𝟙 B)
[PROOFSTEP]
rw [← F.map_add]
  -- porting note: `simp only` fails to use this lemma
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ F.map (f ≫ φ) = F.map (𝟙 A) ∧
    F.map (χ ≫ g) = F.map (𝟙 C) ∧ F.map (f ≫ g) = 0 ∧ F.map (χ ≫ φ) = 0 ∧ F.map (φ ≫ f + g ≫ χ) = F.map (𝟙 B)
[PROOFSTEP]
simp only [F.map_zero, *, true_and]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ biprod.inl ≫ h.iso.inv = f
[PROOFSTEP]
rw [Iso.comp_inv_eq, h.comp_iso_eq_inl]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ h.iso.inv ≫ g = biprod.snd
[PROOFSTEP]
rw [Iso.inv_comp_eq, h.iso_comp_snd_eq]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ section h ≫ g = 𝟙 C
[PROOFSTEP]
simp [Splitting.section]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ retraction h = 𝟙 A
[PROOFSTEP]
simp [retraction]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ section h ≫ retraction h = 0
[PROOFSTEP]
delta Splitting.section retraction
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ (biprod.inr ≫ h.iso.inv) ≫ h.iso.hom ≫ biprod.fst = 0
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.48802, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ retraction h = 𝟙 A
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.49754, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ section h ≫ g = 𝟙 C
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{?u.54404, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : HasZeroMorphisms 𝒜
inst✝¹ : HasBinaryBiproducts 𝒜
h : Splitting f✝ g
X Y Z : 𝒜
f : X ⟶ Y
inst✝ : IsIso f
hZ : IsZero Z
⊢ f ≫ ((asIso f).symm ≪≫ isoBiprodZero hZ).hom = biprod.inl
[PROOFSTEP]
simp [hZ.eq_of_tgt _ 0]
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{?u.54404, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : HasZeroMorphisms 𝒜
inst✝¹ : HasBinaryBiproducts 𝒜
h : Splitting f✝ g
X Y Z : 𝒜
f : X ⟶ Y
inst✝ : IsIso f
hZ : IsZero Z
⊢ ((asIso f).symm ≪≫ isoBiprodZero hZ).hom ≫ biprod.snd = 0
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.60340, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Mono (section h)
[PROOFSTEP]
delta Splitting.section
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.60340, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Mono (biprod.inr ≫ h.iso.inv)
[PROOFSTEP]
infer_instance
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.61269, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Epi (retraction h)
[PROOFSTEP]
delta retraction
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.61269, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Epi (h.iso.hom ≫ biprod.fst)
[PROOFSTEP]
apply epi_comp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ retraction h ≫ f + g ≫ section h = 𝟙 B
[PROOFSTEP]
delta Splitting.section retraction
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ (h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv = 𝟙 B
[PROOFSTEP]
rw [← cancel_mono h.iso.hom, ← cancel_epi h.iso.inv]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ h.iso.inv ≫ ((h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv) ≫ h.iso.hom = h.iso.inv ≫ 𝟙 B ≫ h.iso.hom
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, Category.assoc, Iso.inv_hom_id_assoc, Iso.inv_hom_id,
  Limits.biprod.total, Preadditive.comp_add, Preadditive.add_comp, Splitting.comp_iso_eq_inl,
  Splitting.iso_comp_eq_snd_assoc]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
[PROOFSTEP]
haveI := h.mono
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
[PROOFSTEP]
rw [← cancel_mono f]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ (section h' ≫ retraction h) ≫ f = (-section h ≫ retraction h') ≫ f
[PROOFSTEP]
simp [retraction_ι_eq_id_sub]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ g = 0
[PROOFSTEP]
rw [← h.inl_comp_iso_eq, Category.assoc, h.iso_comp_eq_snd, biprod.inl_snd]
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact f g
[PROOFSTEP]
rw [exact_iff_exact_of_iso f g (biprod.inl : A ⟶ A ⊞ C) (biprod.snd : A ⊞ C ⟶ C) _ _ _]
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact biprod.inl biprod.snd
[PROOFSTEP]
exact exact_inl_snd _ _
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk f ≅ Arrow.mk biprod.inl
[PROOFSTEP]
refine Arrow.isoMk (Iso.refl _) h.iso ?_
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk biprod.inl).hom = (Arrow.mk f).hom ≫ h.iso.hom
[PROOFSTEP]
simp only [Iso.refl_hom, Arrow.mk_hom, Category.id_comp, comp_iso_eq_inl]
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ biprod.inl = biprod.inl
[PROOFSTEP]
rfl
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk g ≅ Arrow.mk biprod.snd
[PROOFSTEP]
refine Arrow.isoMk h.iso (Iso.refl _) ?_
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ (Arrow.mk biprod.snd).hom = (Arrow.mk g).hom ≫ (Iso.refl (Arrow.mk g).right).hom
[PROOFSTEP]
dsimp
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ biprod.snd = g ≫ 𝟙 C
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Arrow.isoMk (Iso.refl (Arrow.mk f).left) h.iso).hom.right =
    (Arrow.isoMk h.iso (Iso.refl (Arrow.mk g).right)).hom.left
[PROOFSTEP]
rfl
