feat(alegbra/homology/short_exact/abelian.lean): Right split exact se…

…quences + case of modules (#14376)

A right split short exact sequence in an abelian category is split.
Also, in the case of the Module category, a version fully expressed in terms of modules and linear maps is provided.

src/algebra/category/Module/biproducts.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import algebra.group.pi
 import category_theory.limits.shapes.biproducts
 import algebra.category.Module.limits
+import algebra.homology.short_exact.abelian
 
 /-!
 # The category of `R`-modules has finite biproducts
@@ -129,3 +130,32 @@ is_limit.cone_point_unique_up_to_iso
 is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk j)
 
 end Module
+
+section split_exact
+
+variables {R : Type u} {A M B : Type v} [ring R] [add_comm_group A] [module R A]
+  [add_comm_group B] [module R B] [add_comm_group M] [module R M]
+variables {j : A →ₗ[R] M} {g : M →ₗ[R] B}
+open Module
+
+/--The isomorphism `A × B ≃ₗ[R] M` coming from a right split exact sequence `0 ⟶ A ⟶ M ⟶ B ⟶ 0`
+of modules.-/
+noncomputable def lequiv_prod_of_right_split_exact {f : B →ₗ[R] M}
+  (hj : function.injective j) (exac : j.range = g.ker) (h : g.comp f = linear_map.id) :
+  (A × B) ≃ₗ[R] M :=
+(({ right_split := ⟨as_hom f, h⟩,
+    mono := (Module.mono_iff_injective $ as_hom j).mpr hj,
+    exact := (exact_iff _ _).mpr exac } : right_split _ _).splitting.iso.trans $
+  biprod_iso_prod _ _).to_linear_equiv.symm
+
+/--The isomorphism `A × B ≃ₗ[R] M` coming from a left split exact sequence `0 ⟶ A ⟶ M ⟶ B ⟶ 0`
+of modules.-/
+noncomputable def lequiv_prod_of_left_split_exact {f : M →ₗ[R] A}
+  (hg : function.surjective g) (exac : j.range = g.ker) (h : f.comp j = linear_map.id) :
+  (A × B) ≃ₗ[R] M :=
+(({ left_split := ⟨as_hom f, h⟩,
+    epi := (Module.epi_iff_surjective $ as_hom g).mpr hg,
+    exact := (exact_iff _ _).mpr exac } : left_split _ _).splitting.iso.trans $
+  biprod_iso_prod _ _).to_linear_equiv.symm
+
+end split_exact

src/algebra/homology/short_exact/abelian.lean

@@ -1,15 +1,15 @@
 /-
 Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Andrew Yang
+Authors: Johan Commelin, Andrew Yang, Pierre-Alexandre Bazin
 -/
 import algebra.homology.short_exact.preadditive
 import category_theory.abelian.diagram_lemmas.four
 
 /-!
 # Short exact sequences in abelian categories
 
-In an abelian category, a left-split short exact sequence admits a splitting.
+In an abelian category, a left-split or right-split short exact sequence admits a splitting.
 -/
 
 noncomputable theory
@@ -45,8 +45,7 @@ a *morphism* `i : B ⟶ A ⊞ C` such that `f ≫ i` is the canonical map `bipro
 `i ≫ q = g`, where `q` is the canonical map `biprod.snd : A ⊞ C ⟶ C`,
 together with proofs that `f` is mono and `g` is epi.
 
-The morphism `i` is than automatically an isomorphism. -/
--- TODO: we may also want the version that supplies a morphism `A ⊞ C ⟶ B`.
+The morphism `i` is then automatically an isomorphism. -/
 def splitting.mk' (h : short_exact f g) (i : B ⟶ A ⊞ C)
   (h1 : f ≫ i = biprod.inl) (h2 : i ≫ biprod.snd = g) : splitting f g :=
 { iso :=
@@ -60,6 +59,25 @@ def splitting.mk' (h : short_exact f g) (i : B ⟶ A ⊞ C)
   comp_iso_eq_inl := by { rwa as_iso_hom, },
   iso_comp_snd_eq := h2 }
 
+/-- To construct a splitting of `A -f⟶ B -g⟶ C` it suffices to supply
+a *morphism* `i : A ⊞ C ⟶ B` such that `p ≫ i = f` where `p` is the canonical map
+`biprod.inl : A ⟶ A ⊞ C`, and `i ≫ g` is the canonical map `biprod.snd : A ⊞ C ⟶ C`,
+together with proofs that `f` is mono and `g` is epi.
+
+The morphism `i` is then automatically an isomorphism. -/
+def splitting.mk'' (h : short_exact f g) (i : A ⊞ C ⟶ B)
+  (h1 : biprod.inl ≫ i = f) (h2 : i ≫ g = biprod.snd) : splitting f g :=
+{ iso :=
+  begin
+    refine (@as_iso _ _ _ _ i (id _)).symm,
+    refine is_iso_of_short_exact_of_is_iso_of_is_iso _ h _ _ _
+      (h1.trans (category.id_comp _).symm).symm (h2.trans (category.comp_id _).symm),
+    split,
+    apply exact_inl_snd
+  end,
+  comp_iso_eq_inl := by rw [iso.symm_hom, as_iso_inv, is_iso.comp_inv_eq, h1],
+  iso_comp_snd_eq := by rw [iso.symm_hom, as_iso_inv, is_iso.inv_comp_eq, h2] }
+
 /-- A short exact sequence that is left split admits a splitting. -/
 def left_split.splitting {f : A ⟶ B} {g : B ⟶ C} (h : left_split f g) : splitting f g :=
 splitting.mk' h.short_exact (biprod.lift h.left_split.some g)
@@ -68,4 +86,12 @@ splitting.mk' h.short_exact (biprod.lift h.left_split.some g)
   { simp only [biprod.inl_snd, biprod.lift_snd, category.assoc, h.exact.w], } })
 (by { simp only [biprod.lift_snd], })
 
+/-- A short exact sequence that is right split admits a splitting. -/
+def right_split.splitting {f : A ⟶ B} {g : B ⟶ C} (h : right_split f g) : splitting f g :=
+splitting.mk'' h.short_exact (biprod.desc f h.right_split.some)
+(biprod.inl_desc _ _)
+(by { ext,
+  { rw [biprod.inl_snd, ← category.assoc, biprod.inl_desc, h.exact.w] },
+  { rw [biprod.inr_snd, ← category.assoc, biprod.inr_desc, h.right_split.some_spec] } })
+
 end category_theory