feat(category_theory): turn a split mono with cokernel into a biproduct (#13184)

Author: javra

src/category_theory/limits/shapes/biproducts.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Jakob von Raumer
 -/
 import algebra.group.ext
 import category_theory.limits.shapes.finite_products
@@ -1539,6 +1539,106 @@ lemma biprod.map_eq [has_binary_biproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X
   biprod.map f g = biprod.fst ≫ f ≫ biprod.inl + biprod.snd ≫ g ≫ biprod.inr :=
 by apply biprod.hom_ext; apply biprod.hom_ext'; simp
 
+/--
+Every split mono `f` with a cokernel induces a binary bicone with `f` as its `inl` and
+the cokernel map as its `snd`.
+We will show in `is_bilimit_binary_bicone_of_split_mono_of_cokernel` that this binary bicone is in
+fact already a biproduct. -/
+@[simps]
+def binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono f]
+  {c : cokernel_cofork f} (i : is_colimit c) : binary_bicone X c.X :=
+{ X := Y,
+  fst := retraction f,
+  snd := c.π,
+  inl := f,
+  inr :=
+    let c' : cokernel_cofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) :=
+      cokernel_cofork.of_π (cofork.π c) (by simp) in
+    let i' : is_colimit c' := is_cokernel_epi_comp i (retraction f) (by simp) in
+    let i'' := is_colimit_cofork_of_cokernel_cofork i' in
+    (split_epi_of_idempotent_of_is_colimit_cofork C (by simp) i'').section_,
+  inl_fst' := by simp,
+  inl_snd' := by simp,
+  inr_fst' :=
+  begin
+    dsimp only,
+    rw [split_epi_of_idempotent_of_is_colimit_cofork_section_,
+      is_colimit_cofork_of_cokernel_cofork_desc, is_cokernel_epi_comp_desc],
+    dsimp only [cokernel_cofork_of_cofork_of_π],
+    letI := epi_of_is_colimit_parallel_pair i,
+    apply zero_of_epi_comp c.π,
+    simp only [sub_comp, category.comp_id, category.assoc, split_mono.id, is_colimit.fac_assoc,
+      cofork.of_π_ι_app, category.id_comp, cofork.π_of_π],
+    apply sub_eq_zero_of_eq,
+    apply category.id_comp
+  end,
+  inr_snd' := by apply split_epi.id }
+
+/-- The bicone constructed in `binary_bicone_of_split_mono_of_cokernel` is a bilimit.
+This is a version of the splitting lemma that holds in all preadditive categories. -/
+def is_bilimit_binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono f]
+  {c : cokernel_cofork f} (i : is_colimit c) :
+  (binary_bicone_of_split_mono_of_cokernel i).is_bilimit :=
+is_binary_bilimit_of_total _
+begin
+  simp only [binary_bicone_of_split_mono_of_cokernel_fst,
+    binary_bicone_of_split_mono_of_cokernel_inr, binary_bicone_of_split_mono_of_cokernel_snd,
+    split_epi_of_idempotent_of_is_colimit_cofork_section_],
+  dsimp only [binary_bicone_of_split_mono_of_cokernel_X],
+  rw [is_colimit_cofork_of_cokernel_cofork_desc, is_cokernel_epi_comp_desc],
+  simp only [cofork.is_colimit.π_desc_of_π, cokernel_cofork_of_cofork_π,
+    cofork.π_of_π, binary_bicone_of_split_mono_of_cokernel_inl, add_sub_cancel'_right],
+end
+
+/--
+Every split epi `f` with a kernel induces a binary bicone with `f` as its `snd` and
+the kernel map as its `inl`.
+We will show in `binary_bicone_of_split_mono_of_cokernel` that this binary bicone is in fact
+already a biproduct. -/
+@[simps]
+def binary_bicone_of_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [split_epi f]
+  {c : kernel_fork f} (i : is_limit c) : binary_bicone c.X Y :=
+{ X := X,
+  fst :=
+    let c' : kernel_fork (𝟙 X - (𝟙 X - f ≫ section_ f)) :=
+      kernel_fork.of_ι (fork.ι c) (by simp) in
+    let i' : is_limit c' := is_kernel_comp_mono i (section_ f) (by simp) in
+    let i'' := is_limit_fork_of_kernel_fork i' in
+    (split_mono_of_idempotent_of_is_limit_fork C (by simp) i'').retraction,
+  snd := f,
+  inl := c.ι,
+  inr := section_ f,
+  inl_fst' := by apply split_mono.id,
+  inl_snd' := by simp,
+  inr_fst' :=
+  begin
+    dsimp only,
+    rw [split_mono_of_idempotent_of_is_limit_fork_retraction,
+      is_limit_fork_of_kernel_fork_lift, is_kernel_comp_mono_lift],
+    dsimp only [kernel_fork_of_fork_ι],
+    letI := mono_of_is_limit_parallel_pair i,
+    apply zero_of_comp_mono c.ι,
+    simp only [comp_sub, category.comp_id, category.assoc, sub_self, fork.ι_eq_app_zero,
+      fork.is_limit.lift_of_ι_ι, fork.of_ι_π_app, split_epi.id_assoc]
+  end,
+  inr_snd' := by simp }
+
+/-- The bicone constructed in `binary_bicone_of_split_epi_of_kernel` is a bilimit.
+This is a version of the splitting lemma that holds in all preadditive categories. -/
+def is_bilimit_binary_bicone_of_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [split_epi f]
+  {c : kernel_fork f} (i : is_limit c) :
+  (binary_bicone_of_split_epi_of_kernel i).is_bilimit :=
+is_binary_bilimit_of_total _
+begin
+  simp only [binary_bicone_of_split_epi_of_kernel_fst, binary_bicone_of_split_epi_of_kernel_inl,
+    binary_bicone_of_split_epi_of_kernel_inr, binary_bicone_of_split_epi_of_kernel_snd,
+    split_mono_of_idempotent_of_is_limit_fork_retraction],
+  dsimp only [binary_bicone_of_split_epi_of_kernel_X],
+  rw [is_limit_fork_of_kernel_fork_lift, is_kernel_comp_mono_lift],
+  simp only [fork.ι_eq_app_zero, kernel_fork.condition, comp_zero, zero_comp, eq_self_iff_true,
+    fork.is_limit.lift_of_ι_ι, kernel_fork_of_fork_ι, fork.of_ι_π_app, sub_add_cancel]
+end
+
 end
 
 section

src/category_theory/limits/shapes/equalizers.lean

@@ -359,6 +359,7 @@ fork.is_limit.mk t
 
 /-- This is a slightly more convenient method to verify that a cofork is a colimit cocone. It
     only asks for a proof of facts that carry any mathematical content -/
+@[simps]
 def cofork.is_colimit.mk (t : cofork f g)
   (desc : Π (s : cofork f g), t.X ⟶ s.X)
   (fac : ∀ (s : cofork f g), cofork.π t ≫ desc s = cofork.π s)
@@ -940,19 +941,20 @@ lemma has_equalizer_comp_mono [has_equalizer f g] {Z : C} (h : Y ⟶ Z) [mono h]
 ⟨⟨{ cone := _, is_limit := is_equalizer_comp_mono (limit.is_limit _) h }⟩⟩
 
 /-- An equalizer of an idempotent morphism and the identity is split mono. -/
+@[simps]
 def split_mono_of_idempotent_of_is_limit_fork {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
-  {c : fork f (𝟙 X)} (i : is_limit c) : split_mono c.ι :=
+  {c : fork (𝟙 X) f} (i : is_limit c) : split_mono c.ι :=
 { retraction := i.lift (fork.of_ι f (by simp [hf])),
   id' :=
   begin
     letI := mono_of_is_limit_parallel_pair i,
-    rw [← cancel_mono_id c.ι, category.assoc, fork.is_limit.lift_of_ι_ι, c.condition],
+    rw [←cancel_mono_id c.ι, category.assoc, fork.is_limit.lift_of_ι_ι, ←c.condition],
     exact category.comp_id c.ι
   end }
 
 /-- The equalizer of an idempotent morphism and the identity is split mono. -/
 def split_mono_of_idempotent_equalizer {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
-  [has_equalizer f (𝟙 X)] : split_mono (equalizer.ι f (𝟙 X)) :=
+  [has_equalizer (𝟙 X) f] : split_mono (equalizer.ι (𝟙 X) f) :=
 split_mono_of_idempotent_of_is_limit_fork _ hf (limit.is_limit _)
 
 section
@@ -990,12 +992,12 @@ def split_epi_of_coequalizer {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : f ≫ s
 
 variables {C f g}
 
-/-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is 
+/-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is
 a coequalizer. -/
 def is_coequalizer_epi_comp {c : cofork f g} (i : is_colimit c) {W : C} (h : W ⟶ X) [hm : epi h] :
   is_colimit (cofork.of_π c.π (by simp) : cofork (h ≫ f) (h ≫ g)) :=
 cofork.is_colimit.mk' _ $ λ s,
-  let s' : cofork f g := cofork.of_π s.π 
+  let s' : cofork f g := cofork.of_π s.π
     (by apply hm.left_cancellation; simp_rw [←category.assoc, s.condition]) in
   let l := cofork.is_colimit.desc' i s'.π s'.condition in
   ⟨l.1, l.2,
@@ -1008,19 +1010,20 @@ lemma has_coequalizer_epi_comp [has_coequalizer f g] {W : C} (h : W ⟶ X) [hm :
 variables (C f g)
 
 /-- A coequalizer of an idempotent morphism and the identity is split epi. -/
+@[simps]
 def split_epi_of_idempotent_of_is_colimit_cofork {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
-  {c : cofork f (𝟙 X)} (i : is_colimit c) : split_epi c.π :=
+  {c : cofork (𝟙 X) f} (i : is_colimit c) : split_epi c.π :=
 { section_ := i.desc (cofork.of_π f (by simp [hf])),
   id' :=
   begin
     letI := epi_of_is_colimit_parallel_pair i,
-    rw [← cancel_epi_id c.π, ← category.assoc, cofork.is_colimit.π_desc_of_π, c.condition],
+    rw [← cancel_epi_id c.π, ← category.assoc, cofork.is_colimit.π_desc_of_π, ← c.condition],
     exact category.id_comp _,
   end }
 
 /-- The coequalizer of an idempotent morphism and the identity is split epi. -/
 def split_epi_of_idempotent_coequalizer {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
-  [has_coequalizer f (𝟙 X)] : split_epi (coequalizer.π f (𝟙 X)) :=
+  [has_coequalizer (𝟙 X) f] : split_epi (coequalizer.π (𝟙 X) f) :=
 split_epi_of_idempotent_of_is_colimit_cofork _ hf (colimit.is_colimit _)
 
 end category_theory.limits

src/category_theory/limits/shapes/kernels.lean

@@ -136,13 +136,19 @@ def is_limit.of_ι {W : C} (g : W ⟶ X) (eq : g ≫ f = 0)
 is_limit_aux _ (λ s, lift s.ι s.condition) (λ s, fac s.ι s.condition) (λ s, uniq s.ι s.condition)
 
 /-- Every kernel of `f` induces a kernel of `f ≫ g` if `g` is mono. -/
-def is_kernel_comp_mono  {c : kernel_fork f} (i : is_limit c) {Z} (g : Y ⟶ Z) [hg : mono g] :
-  is_limit (kernel_fork.of_ι c.ι (by simp) : kernel_fork (f ≫ g)) :=
+def is_kernel_comp_mono {c : kernel_fork f} (i : is_limit c) {Z} (g : Y ⟶ Z) [hg : mono g]
+  {h : X ⟶ Z} (hh : h = f ≫ g) :
+  is_limit (kernel_fork.of_ι c.ι (by simp [hh]) : kernel_fork h) :=
 fork.is_limit.mk' _ $ λ s,
-  let s' : kernel_fork f := fork.of_ι s.ι (by apply hg.right_cancellation; simp [s.condition]) in
+  let s' : kernel_fork f := fork.of_ι s.ι (by rw [←cancel_mono g]; simp [←hh, s.condition]) in
   let l := kernel_fork.is_limit.lift' i s'.ι s'.condition in
   ⟨l.1, l.2, λ m hm, by apply fork.is_limit.hom_ext i; rw fork.ι_of_ι at hm; rw hm; exact l.2.symm⟩
 
+lemma is_kernel_comp_mono_lift {c : kernel_fork f} (i : is_limit c) {Z} (g : Y ⟶ Z) [hg : mono g]
+  {h : X ⟶ Z} (hh : h = f ≫ g) (s : kernel_fork h) :
+  (is_kernel_comp_mono i g hh).lift s
+  = i.lift (fork.of_ι s.ι (by { rw [←cancel_mono g, category.assoc, ←hh], simp })) := rfl
+
 end
 
 section
@@ -283,7 +289,7 @@ lemma kernel_not_iso_of_nonzero (w : f ≠ 0) : (is_iso (kernel.ι f)) → false
 
 instance has_kernel_comp_mono {X Y Z : C} (f : X ⟶ Y) [has_kernel f] (g : Y ⟶ Z) [mono g] :
   has_kernel (f ≫ g) :=
-⟨⟨{ cone := _, is_limit := is_kernel_comp_mono (limit.is_limit _) g }⟩⟩
+⟨⟨{ cone := _, is_limit := is_kernel_comp_mono (limit.is_limit _) g rfl }⟩⟩
 
 /--
 When `g` is a monomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`.
@@ -452,15 +458,22 @@ def is_colimit.of_π {Z : C} (g : Y ⟶ Z) (eq : f ≫ g = 0)
 is_colimit_aux _ (λ s, desc s.π s.condition) (λ s, fac s.π s.condition) (λ s, uniq s.π s.condition)
 
 /-- Every cokernel of `f` induces a cokernel of `g ≫ f` if `g` is epi. -/
-def is_cokernel_epi_comp  {c : cokernel_cofork f} (i : is_colimit c) {W} (g : W ⟶ X) [hg : epi g] :
-  is_colimit (cokernel_cofork.of_π c.π (by simp) : cokernel_cofork (g ≫ f)) :=
+def is_cokernel_epi_comp  {c : cokernel_cofork f} (i : is_colimit c) {W} (g : W ⟶ X) [hg : epi g]
+  {h : W ⟶ Y} (hh : h = g ≫ f) :
+  is_colimit (cokernel_cofork.of_π c.π (by rw [hh]; simp) : cokernel_cofork h) :=
 cofork.is_colimit.mk' _ $ λ s,
   let s' : cokernel_cofork f := cofork.of_π s.π
-    (by apply hg.left_cancellation; simp [←category.assoc, s.condition]) in
+    (by { apply hg.left_cancellation, rw [←category.assoc, ←hh, s.condition], simp }) in
   let l := cokernel_cofork.is_colimit.desc' i s'.π s'.condition in
   ⟨l.1, l.2,
     λ m hm, by apply cofork.is_colimit.hom_ext i; rw cofork.π_of_π at hm; rw hm; exact l.2.symm⟩
 
+@[simp]
+lemma is_cokernel_epi_comp_desc {c : cokernel_cofork f} (i : is_colimit c) {W}
+  (g : W ⟶ X) [hg : epi g] {h : W ⟶ Y} (hh : h = g ≫ f) (s : cokernel_cofork h) :
+  (is_cokernel_epi_comp i g hh).desc s
+  = i.desc (cofork.of_π s.π (by { rw [←cancel_epi g, ←category.assoc, ←hh], simp })) := rfl
+
 end
 
 section
@@ -625,14 +638,13 @@ def cokernel_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel f
 
 instance has_cokernel_epi_comp {X Y : C} (f : X ⟶ Y) [has_cokernel f] {W} (g : W ⟶ X) [epi g] :
   has_cokernel (g ≫ f) :=
-⟨⟨{ cocone := _, is_colimit := is_cokernel_epi_comp (colimit.is_colimit _) g }⟩⟩
+⟨⟨{ cocone := _, is_colimit := is_cokernel_epi_comp (colimit.is_colimit _) g rfl }⟩⟩
 
 /--
 When `f` is an epimorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`.
 -/
 @[simps]
-def cokernel_epi_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
-  [epi f] [has_cokernel g] :
+def cokernel_epi_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [epi f] [has_cokernel g] :
   cokernel (f ≫ g) ≅ cokernel g :=
 { hom := cokernel.desc _ (cokernel.π g) (by simp),
   inv := cokernel.desc _ (cokernel.π (f ≫ g)) (by { rw [←cancel_epi f, ←category.assoc], simp, }), }

src/category_theory/preadditive/default.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
+Authors: Markus Himmel, Jakob von Raumer
 -/
 import algebra.big_operators.basic
 import algebra.hom.group
@@ -233,13 +233,22 @@ fork.of_ι c.ι $ by rw [← sub_eq_zero, ← comp_sub, c.condition]
 def kernel_fork_of_fork (c : fork f g) : kernel_fork (f - g) :=
 fork.of_ι c.ι $ by rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
 
+@[simp] lemma kernel_fork_of_fork_ι (c : fork f g) : (kernel_fork_of_fork c).ι = c.ι := rfl
+
+@[simp] lemma kernel_fork_of_fork_of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
+  (kernel_fork_of_fork (fork.of_ι ι w)) = kernel_fork.of_ι ι (by simp [w]) := rfl
+
 /-- A kernel of `f - g` is an equalizer of `f` and `g`. -/
 def is_limit_fork_of_kernel_fork {c : kernel_fork (f - g)} (i : is_limit c) :
   is_limit (fork_of_kernel_fork c) :=
 fork.is_limit.mk' _ $ λ s,
   ⟨i.lift (kernel_fork_of_fork s), i.fac _ _,
    λ m h, by { apply fork.is_limit.hom_ext i, rw [i.fac], exact h }⟩
 
+@[simp]
+lemma is_limit_fork_of_kernel_fork_lift {c : kernel_fork (f - g)} (i : is_limit c) (s : fork f g) :
+  (is_limit_fork_of_kernel_fork i).lift s = i.lift (kernel_fork_of_fork s) := rfl
+
 /-- An equalizer of `f` and `g` is a kernel of `f - g`. -/
 def is_limit_kernel_fork_of_fork {c : fork f g} (i : is_limit c) :
   is_limit (kernel_fork_of_fork c) :=
@@ -269,13 +278,24 @@ cofork.of_π c.π $ by rw [← sub_eq_zero, ← sub_comp, c.condition]
 def cokernel_cofork_of_cofork (c : cofork f g) : cokernel_cofork (f - g) :=
 cofork.of_π c.π $ by rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
 
+@[simp] lemma cokernel_cofork_of_cofork_π (c : cofork f g) :
+  (cokernel_cofork_of_cofork c).π = c.π := rfl
+
+@[simp] lemma cokernel_cofork_of_cofork_of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
+  (cokernel_cofork_of_cofork (cofork.of_π π w)) = cokernel_cofork.of_π π (by simp [w]) := rfl
+
 /-- A cokernel of `f - g` is a coequalizer of `f` and `g`. -/
 def is_colimit_cofork_of_cokernel_cofork {c : cokernel_cofork (f - g)} (i : is_colimit c) :
   is_colimit (cofork_of_cokernel_cofork c) :=
 cofork.is_colimit.mk' _ $ λ s,
   ⟨i.desc (cokernel_cofork_of_cofork s), i.fac _ _,
    λ m h, by { apply cofork.is_colimit.hom_ext i, rw [i.fac], exact h }⟩
 
+@[simp]
+lemma is_colimit_cofork_of_cokernel_cofork_desc {c : cokernel_cofork (f - g)}
+  (i : is_colimit c) (s : cofork f g) :
+  (is_colimit_cofork_of_cokernel_cofork i).desc s = i.desc (cokernel_cofork_of_cofork s) := rfl
+
 /-- A coequalizer of `f` and `g` is a cokernel of `f - g`. -/
 def is_colimit_cokernel_cofork_of_cofork {c : cofork f g} (i : is_colimit c) :
   is_colimit (cokernel_cofork_of_cofork c) :=