Commit 2023-04-18 11:49 178f346d

View on Github →

feat: port Algebra.Homology.Exact (#3468)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Exact.lean

added structure CategoryTheory.Exact

added theorem CategoryTheory.Functor.exact_of_exact_map

added theorem CategoryTheory.Preadditive.exact_iff_exact_of_iso

added theorem CategoryTheory.Preadditive.exact_iff_homology_zero

added theorem CategoryTheory.Preadditive.exact_of_iso_of_exact'

added theorem CategoryTheory.Preadditive.exact_of_iso_of_exact

added theorem CategoryTheory.comp_eq_zero_of_exact

added theorem CategoryTheory.comp_eq_zero_of_image_eq_kernel

added theorem CategoryTheory.epi_iff_exact_zero_right

added theorem CategoryTheory.exact_comp_hom_inv_comp

added theorem CategoryTheory.exact_comp_hom_inv_comp_iff

added theorem CategoryTheory.exact_comp_inv_hom_comp

added theorem CategoryTheory.exact_comp_iso

added theorem CategoryTheory.exact_comp_mono

added theorem CategoryTheory.exact_comp_mono_iff

added theorem CategoryTheory.exact_epi_comp

added theorem CategoryTheory.exact_epi_zero

added theorem CategoryTheory.exact_iso_comp

added theorem CategoryTheory.exact_kernelSubobject_arrow

added theorem CategoryTheory.exact_kernel_ι

added theorem CategoryTheory.exact_of_image_eq_kernel

added theorem CategoryTheory.exact_of_zero

added theorem CategoryTheory.exact_zero_left_of_mono

added theorem CategoryTheory.exact_zero_mono

added theorem CategoryTheory.fork_ι_comp_cofork_π

added theorem CategoryTheory.imageToKernel_isIso_of_image_eq_kernel

added theorem CategoryTheory.kernelSubobject_arrow_eq_zero_of_exact_zero_left

added theorem CategoryTheory.kernel_comp_cokernel

added theorem CategoryTheory.kernel_ι_eq_zero_of_exact_zero_left

added theorem CategoryTheory.mono_iff_exact_zero_left