Commit 2023-04-24 12:12 76525aae

View on Github →

feat: port Algebra.Homology.ShortExact.Preadditive (#3611)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ShortExact/Preadditive.lean

added theorem CategoryTheory.LeftSplit.shortExact

added structure CategoryTheory.LeftSplit

added theorem CategoryTheory.RightSplit.shortExact

added structure CategoryTheory.RightSplit

added structure CategoryTheory.ShortExact

added theorem CategoryTheory.Split.exact

added theorem CategoryTheory.Split.leftSplit

added theorem CategoryTheory.Split.map

added theorem CategoryTheory.Split.rightSplit

added theorem CategoryTheory.Split.shortExact

added structure CategoryTheory.Split

added theorem CategoryTheory.Splitting.comp_eq_zero

added theorem CategoryTheory.Splitting.inl_comp_iso_eq

added theorem CategoryTheory.Splitting.inr_iso_inv

added theorem CategoryTheory.Splitting.iso_comp_eq_snd

added theorem CategoryTheory.Splitting.iso_hom_fst

added def CategoryTheory.Splitting.retraction

added theorem CategoryTheory.Splitting.retraction_ι_eq_id_sub

added theorem CategoryTheory.Splitting.section_retraction

added theorem CategoryTheory.Splitting.section_π

added theorem CategoryTheory.Splitting.split

added theorem CategoryTheory.Splitting.split_add

added def CategoryTheory.Splitting.splittingOfIsIsoZero

added theorem CategoryTheory.Splitting.splittings_comm

added def CategoryTheory.Splitting.«section»

added theorem CategoryTheory.Splitting.ι_retraction

added theorem CategoryTheory.Splitting.π_section_eq_id_sub

added structure CategoryTheory.Splitting

added theorem CategoryTheory.exact_inl_snd

added theorem CategoryTheory.exact_inr_fst

added theorem CategoryTheory.exact_of_split