Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-22 11:32 90d33863

View on Github →

feat(category_theory/kernels): compute kernel (f ≫ g) when one is an iso (#3438)

Estimated changes

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

added def category_theory.limits.cokernel_comp_is_iso

added def category_theory.limits.cokernel_is_iso_comp

added theorem category_theory.limits.cokernel_π_comp_cokernel_comp_is_iso_hom

added theorem category_theory.limits.cokernel_π_comp_cokernel_comp_is_iso_inv

added theorem category_theory.limits.cokernel_π_comp_cokernel_is_iso_comp_hom

added theorem category_theory.limits.cokernel_π_comp_cokernel_is_iso_comp_inv

added def category_theory.limits.kernel_comp_is_iso

added theorem category_theory.limits.kernel_comp_is_iso_hom_comp_kernel_ι

added theorem category_theory.limits.kernel_comp_is_iso_inv_comp_kernel_ι

added def category_theory.limits.kernel_is_iso_comp

added theorem category_theory.limits.kernel_is_iso_comp_hom_comp_kernel_ι

added theorem category_theory.limits.kernel_is_iso_comp_inv_comp_kernel_ι