Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 16:51 bbe25d4d

View on Github →

feat(category_theory): left-exact functors preserve finite limits (#14026) Also adds the following:

Convenient constructors for binary_fan and adjustments to its simp NF
Generalize the (co)kernel constructions in inclusions and projections of binary biproducts
Fixes the name of kernel_fork.is_limit.of_ι
Derives preserves_limits_of_shape (discrete pempty) G from the preservation of just the terminal morphism
Preserving zero morphisms implies preserving terminal morphisms
Isomorphisms from any fork to an application of fork.of_ι

Estimated changes

Modified src/category_theory/abelian/exact.lean

Modified src/category_theory/limits/constructions/finite_products_of_binary_products.lean

Modified src/category_theory/limits/preserves/shapes/terminal.lean

added def category_theory.limits.preserves_colimits_of_shape_pempty_of_preserves_initial

added def category_theory.limits.preserves_limits_of_shape_pempty_of_preserves_terminal

Modified src/category_theory/limits/preserves/shapes/zero.lean

added def category_theory.functor.preserves_initial_object_of_preserves_zero_morphisms

added def category_theory.functor.preserves_terminal_object_of_preserves_zero_morphisms

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

added theorem category_theory.limits.binary_cofan.mk_inl

added theorem category_theory.limits.binary_cofan.mk_inr

deleted theorem category_theory.limits.binary_cofan.mk_ι_app_left

deleted theorem category_theory.limits.binary_cofan.mk_ι_app_right

added theorem category_theory.limits.binary_fan.mk_fst

added theorem category_theory.limits.binary_fan.mk_snd

deleted theorem category_theory.limits.binary_fan.mk_π_app_left

deleted theorem category_theory.limits.binary_fan.mk_π_app_right

added def category_theory.limits.iso_binary_cofan_mk

added def category_theory.limits.iso_binary_fan_mk

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

added def category_theory.limits.binary_bicone.fst_kernel_fork

added theorem category_theory.limits.binary_bicone.fst_kernel_fork_ι

added def category_theory.limits.binary_bicone.inl_cokernel_cofork

added theorem category_theory.limits.binary_bicone.inl_cokernel_cofork_π

added def category_theory.limits.binary_bicone.inr_cokernel_cofork

added theorem category_theory.limits.binary_bicone.inr_cokernel_cofork_π

added def category_theory.limits.binary_bicone.is_colimit_inl_cokernel_cofork

added def category_theory.limits.binary_bicone.is_colimit_inr_cokernel_cofork

added def category_theory.limits.binary_bicone.is_limit_fst_kernel_fork

added def category_theory.limits.binary_bicone.is_limit_snd_kernel_fork

added def category_theory.limits.binary_bicone.snd_kernel_fork

added theorem category_theory.limits.binary_bicone.snd_kernel_fork_ι

added def category_theory.limits.biprod.inl_cokernel_cofork

added theorem category_theory.limits.biprod.inl_cokernel_cofork_π

deleted def category_theory.limits.biprod.inl_cokernel_fork

deleted theorem category_theory.limits.biprod.inl_cokernel_fork_π

added def category_theory.limits.biprod.inr_cokernel_cofork

added theorem category_theory.limits.biprod.inr_cokernel_cofork_π

deleted def category_theory.limits.biprod.inr_cokernel_fork

deleted theorem category_theory.limits.biprod.inr_cokernel_fork_π

modified def category_theory.limits.biprod.is_cokernel_inl_cokernel_fork

modified def category_theory.limits.biprod.is_cokernel_inr_cokernel_fork

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

added def category_theory.limits.cofork.iso_cofork_of_π

added theorem category_theory.limits.cofork.π_precompose

added def category_theory.limits.fork.iso_fork_of_ι

added theorem category_theory.limits.fork.ι_postcompose

added def category_theory.limits.parallel_pair.eq_of_hom_eq

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

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

added def category_theory.limits.cokernel_cofork.is_colimit.of_π

deleted def category_theory.limits.is_colimit.of_π

deleted def category_theory.limits.is_limit.of_ι

added def category_theory.limits.kernel_fork.is_limit.of_ι

Modified src/category_theory/limits/shapes/normal_mono/basic.lean

Modified src/category_theory/preadditive/additive_functor.lean

Modified src/category_theory/preadditive/default.lean

added theorem category_theory.preadditive.cofork_of_cokernel_cofork_π

added theorem category_theory.preadditive.fork_of_kernel_fork_ι

Created src/category_theory/preadditive/left_exact.lean

added def category_theory.functor.is_colimit_map_cocone_binary_cofan_of_preserves_cokernels

added def category_theory.functor.is_limit_map_cone_binary_fan_of_preserves_kernels

added def category_theory.functor.preserves_binary_coproducts_of_preserves_cokernels

added def category_theory.functor.preserves_binary_product_of_preserves_kernels

added def category_theory.functor.preserves_binary_products_of_preserves_kernels

added def category_theory.functor.preserves_coequalizer_of_preserves_cokernels

added def category_theory.functor.preserves_coequalizers_of_preserves_cokernels

added def category_theory.functor.preserves_coproduct_of_preserves_cokernels

added def category_theory.functor.preserves_equalizer_of_preserves_kernels

added def category_theory.functor.preserves_equalizers_of_preserves_kernels

added def category_theory.functor.preserves_finite_colimits_of_preserves_cokernels

added def category_theory.functor.preserves_finite_limits_of_preserves_kernels