Commit 2022-06-02 15:58 4bd8c855

View on Github →

feat(category_theory/limits): is_kernel_of_comp (#14409) From LTE. Also rename lift_comp_ι to lift_ι for consistency with the general has_limit versions.

Estimated changes

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

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

deleted theorem category_theory.limits.cofork.is_colimit.π_comp_desc

added theorem category_theory.limits.cofork.is_colimit.π_desc

deleted theorem category_theory.limits.fork.is_limit.lift_comp_ι

added theorem category_theory.limits.fork.is_limit.lift_ι

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

added def category_theory.limits.is_cokernel_of_comp

added def category_theory.limits.is_kernel_of_comp

Modified src/category_theory/monad/monadicity.lean