Commit 2022-05-17 15:34 e2eea550

View on Github →

feat(algebra/homology): short exact sequences (#14009) Migrating from LTE. (This is all Johan and Andrew's work, I think, I just tidied up some.) Please feel free to push changes directly without consulting me. :-)

Estimated changes

Modified src/algebra/category/Module/adjunctions.lean

Created src/algebra/homology/short_exact/abelian.lean

added theorem category_theory.is_iso_of_short_exact_of_is_iso_of_is_iso

added def category_theory.left_split.splitting

added def category_theory.splitting.mk'

Created src/algebra/homology/short_exact/preadditive.lean

added theorem category_theory.exact_inl_snd

added theorem category_theory.exact_inr_fst

added theorem category_theory.exact_of_split

added theorem category_theory.left_split.short_exact

added structure category_theory.left_split

added theorem category_theory.right_split.short_exact

added structure category_theory.right_split

added structure category_theory.short_exact

added theorem category_theory.split.exact

added theorem category_theory.split.left_split

added theorem category_theory.split.map

added theorem category_theory.split.right_split

added theorem category_theory.split.short_exact

added structure category_theory.split

added theorem category_theory.splitting.comp_eq_zero

added theorem category_theory.splitting.inl_comp_iso_eq

added theorem category_theory.splitting.inr_iso_inv

added theorem category_theory.splitting.iso_comp_eq_snd

added theorem category_theory.splitting.iso_hom_fst

added def category_theory.splitting.retraction

added theorem category_theory.splitting.retraction_ι_eq_id_sub

added def category_theory.splitting.section

added theorem category_theory.splitting.section_retraction

added theorem category_theory.splitting.section_π

added theorem category_theory.splitting.short_exact

added theorem category_theory.splitting.split

added theorem category_theory.splitting.split_add

added def category_theory.splitting.splitting_of_is_iso_zero

added theorem category_theory.splitting.splittings_comm

added theorem category_theory.splitting.ι_retraction

added theorem category_theory.splitting.π_section_eq_id_sub

added structure category_theory.splitting

Modified src/category_theory/limits/shapes/biproducts.lean

added def category_theory.limits.iso_biprod_zero

added def category_theory.limits.iso_zero_biprod

Modified src/category_theory/limits/shapes/zero_objects.lean