Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 18:31 8d2ffb8f

View on Github →

feat(category_theory): (co)kernels of biproduct projection and inclusion (#12394) add kernels and cokernels of biproduct projections and inclusions

Estimated changes

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

added def category_theory.limits.biprod.fst_kernel_fork

added theorem category_theory.limits.biprod.fst_kernel_fork_ι

added def category_theory.limits.biprod.inl_cokernel_fork

added theorem category_theory.limits.biprod.inl_cokernel_fork_π

added def category_theory.limits.biprod.inr_cokernel_fork

added theorem category_theory.limits.biprod.inr_cokernel_fork_π

added def category_theory.limits.biprod.is_cokernel_inl_cokernel_fork

added def category_theory.limits.biprod.is_cokernel_inr_cokernel_fork

added def category_theory.limits.biprod.is_kernel_fst_kernel_fork

added def category_theory.limits.biprod.is_kernel_snd_kernel_fork

added def category_theory.limits.biprod.snd_kernel_fork

added theorem category_theory.limits.biprod.snd_kernel_fork_ι

added def category_theory.limits.biproduct.from_subtype

added theorem category_theory.limits.biproduct.from_subtype_eq_lift

added theorem category_theory.limits.biproduct.from_subtype_to_subtype

added theorem category_theory.limits.biproduct.from_subtype_π

added theorem category_theory.limits.biproduct.from_subtype_π_subtype

added def category_theory.limits.biproduct.is_colimit_to_subtype

added def category_theory.limits.biproduct.is_limit_from_subtype

modified theorem category_theory.limits.biproduct.lift_map

modified def category_theory.limits.biproduct.map'

modified def category_theory.limits.biproduct.map

modified theorem category_theory.limits.biproduct.map_desc

modified theorem category_theory.limits.biproduct.map_eq_map'

modified def category_theory.limits.biproduct.map_iso

modified theorem category_theory.limits.biproduct.map_π

added def category_theory.limits.biproduct.to_subtype

added theorem category_theory.limits.biproduct.to_subtype_eq_desc

added theorem category_theory.limits.biproduct.to_subtype_from_subtype

added theorem category_theory.limits.biproduct.to_subtype_π

added theorem category_theory.limits.biproduct.ι_from_subtype

modified theorem category_theory.limits.biproduct.ι_map

added theorem category_theory.limits.biproduct.ι_to_subtype

added theorem category_theory.limits.biproduct.ι_to_subtype_subtype