Commit 2023-12-21 16:16 850c6404

View on Github →

refactor: use the new homology API for the four and the five lemmas (#9022) This PR refactors the four and the five lemmas so as to use the new homology API. The files Algebra.Homology.ShortExact.Abelian and Algebra.Homology.ShortExact.Preadditive are also removed because the content of these files has become redundant with the new homology API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

Modified Mathlib/Algebra/Category/ModuleCat/Free.lean

modified def ModuleCat.Basis.ofShortExact

modified theorem ModuleCat.free_shortExact

modified theorem ModuleCat.free_shortExact_finrank_add

modified theorem ModuleCat.free_shortExact_rank_add

modified theorem ModuleCat.linearIndependent_leftExact

modified theorem ModuleCat.linearIndependent_shortExact

modified theorem ModuleCat.span_exact

modified theorem ModuleCat.span_rightExact

Modified Mathlib/Algebra/Homology/ExactSequence.lean

added theorem CategoryTheory.ComposableArrows.Exact.exact'

deleted theorem CategoryTheory.ComposableArrows.IsExact.exact'

added theorem CategoryTheory.ComposableArrows.exact_iff_δlast

Deleted Mathlib/Algebra/Homology/ShortExact/Abelian.lean

deleted def CategoryTheory.LeftSplit.splitting

deleted def CategoryTheory.RightSplit.splitting

deleted def CategoryTheory.Splitting.mk''

deleted def CategoryTheory.Splitting.mk'

deleted theorem CategoryTheory.isIso_of_shortExact_of_isIso_of_isIso

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

deleted theorem CategoryTheory.LeftSplit.shortExact

deleted structure CategoryTheory.LeftSplit

deleted theorem CategoryTheory.RightSplit.shortExact

deleted structure CategoryTheory.RightSplit

deleted structure CategoryTheory.ShortExact

deleted theorem CategoryTheory.Split.exact

deleted theorem CategoryTheory.Split.leftSplit

deleted theorem CategoryTheory.Split.map

deleted theorem CategoryTheory.Split.rightSplit

deleted theorem CategoryTheory.Split.shortExact

deleted structure CategoryTheory.Split

deleted theorem CategoryTheory.Splitting.comp_eq_zero

deleted theorem CategoryTheory.Splitting.inl_comp_iso_eq

deleted theorem CategoryTheory.Splitting.inr_iso_inv

deleted theorem CategoryTheory.Splitting.iso_comp_eq_snd

deleted theorem CategoryTheory.Splitting.iso_hom_fst

deleted def CategoryTheory.Splitting.retraction

deleted theorem CategoryTheory.Splitting.retraction_ι_eq_id_sub

deleted theorem CategoryTheory.Splitting.section_retraction

deleted theorem CategoryTheory.Splitting.section_π

deleted theorem CategoryTheory.Splitting.split

deleted theorem CategoryTheory.Splitting.split_add

deleted def CategoryTheory.Splitting.splittingOfIsIsoZero

deleted theorem CategoryTheory.Splitting.splittings_comm

deleted def CategoryTheory.Splitting.«section»

deleted theorem CategoryTheory.Splitting.ι_retraction

deleted theorem CategoryTheory.Splitting.π_section_eq_id_sub

deleted structure CategoryTheory.Splitting

deleted theorem CategoryTheory.exact_inl_snd

deleted theorem CategoryTheory.exact_inr_fst

deleted theorem CategoryTheory.exact_of_split

Modified Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

added theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono'

modified theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono

modified theorem CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono

added theorem CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'

modified theorem CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono

Modified Mathlib/CategoryTheory/ComposableArrows.lean

added def CategoryTheory.ComposableArrows.δlastFunctor

added def Fin.castSuccFunctor

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean