Commit 2024-07-10 15:00 d674e2e1

View on Github →

feat: more API for Function.Exact (#14520) If two diagrams involving additive maps are isomorphic, one is exact (in the sense of Function.Exact) iff the other is. In this PR, we also relate Function.Exact and ShortComplex.Exact in the categories of abelian groups and modules over a ring.

Estimated changes

Modified Mathlib/Algebra/Exact.lean

added theorem AddMonoidHom.exact_iff

added theorem AddMonoidHom.exact_of_comp_eq_zero_of_ker_le_range

added theorem AddMonoidHom.exact_of_comp_of_mem_range

added theorem Function.Exact.addMonoidHom_comp_eq_zero

added theorem Function.Exact.addMonoidHom_ker_eq

modified theorem Function.Exact.apply_apply_eq_zero

modified theorem Function.Exact.comp_eq_zero

modified theorem Function.Exact.comp_injective

added theorem Function.Exact.iff_of_ladder_addEquiv

modified theorem Function.Exact.of_comp_eq_zero_of_ker_in_range

modified theorem Function.Exact.of_comp_of_mem_range

added theorem Function.Exact.of_ladder_addEquiv_of_exact'

added theorem Function.Exact.of_ladder_addEquiv_of_exact

modified theorem LinearEquiv.conj_exact_iff_exact

modified theorem LinearMap.exact_iff

modified theorem LinearMap.exact_of_comp_eq_zero_of_ker_le_range

modified theorem LinearMap.exact_of_comp_of_mem_range

Modified Mathlib/Algebra/Homology/ShortComplex/Ab.lean

added theorem CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact

Modified Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

added theorem CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact