Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 20:30 3a061790

View on Github →

refactor(category_theory): reverse simp lemmas about (co)forks (#13519) Makes fork.ι instead of t.π.app zero so that we avoid any unnecessary references to walking_parallel_pair in (co)fork homs. This induces quite a lot of changes in other files, but I think it's worth the pain. The PR also changes fork.is_limit.mk to avoid stating redundant morphisms.

Estimated changes

Modified src/algebra/category/Module/kernels.lean

Modified src/analysis/normed/group/SemiNormedGroup/kernels.lean

added def SemiNormedGroup.fork

deleted def SemiNormedGroup.parallel_pair_cone

Modified src/category_theory/abelian/basic.lean

Modified src/category_theory/abelian/non_preadditive.lean

Modified src/category_theory/idempotents/basic.lean

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

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

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

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

modified def category_theory.limits.cocone_of_split_epi

added theorem category_theory.limits.cocone_of_split_epi_π

modified theorem category_theory.limits.coequalizer.π_of_eq

added theorem category_theory.limits.cofork.app_one_eq_π

added theorem category_theory.limits.cofork.app_zero_eq_comp_π_left

added theorem category_theory.limits.cofork.app_zero_eq_comp_π_right

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

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

deleted theorem category_theory.limits.cofork.left_app_one

deleted theorem category_theory.limits.cofork.right_app_one

modified def category_theory.limits.cofork.π

deleted theorem category_theory.limits.cofork.π_eq_app_one

modified theorem category_theory.limits.cofork.π_of_π

modified def category_theory.limits.cone_of_split_mono

added theorem category_theory.limits.cone_of_split_mono_ι

added theorem category_theory.limits.epi_of_is_colimit_cofork

deleted theorem category_theory.limits.epi_of_is_colimit_parallel_pair

added theorem category_theory.limits.fork.app_one_eq_ι_comp_left

added theorem category_theory.limits.fork.app_one_eq_ι_comp_right

added theorem category_theory.limits.fork.app_zero_eq_ι

deleted theorem category_theory.limits.fork.app_zero_left

deleted theorem category_theory.limits.fork.app_zero_right

modified theorem category_theory.limits.fork.equalizer_ext

added theorem category_theory.limits.fork.hom_comp_ι

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

deleted theorem category_theory.limits.fork.is_limit.lift_of_ι_ι

modified def category_theory.limits.fork.ι

deleted theorem category_theory.limits.fork.ι_eq_app_zero

modified theorem category_theory.limits.fork.ι_of_ι

added theorem category_theory.limits.fork.π_comp_hom

modified theorem category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_eq

modified theorem category_theory.limits.is_iso_colimit_cocone_parallel_pair_of_self

modified theorem category_theory.limits.is_iso_limit_cocone_parallel_pair_of_epi

modified theorem category_theory.limits.is_iso_limit_cone_parallel_pair_of_epi

modified theorem category_theory.limits.is_iso_limit_cone_parallel_pair_of_eq

modified theorem category_theory.limits.is_iso_limit_cone_parallel_pair_of_self

added theorem category_theory.limits.mono_of_is_limit_fork

deleted theorem category_theory.limits.mono_of_is_limit_parallel_pair

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

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

modified def category_theory.limits.cokernel.is_colimit_cocone_zero_cocone

deleted def category_theory.limits.cokernel.zero_cocone

added def category_theory.limits.cokernel.zero_cokernel_cofork

deleted theorem category_theory.limits.cokernel_cofork.app_zero

modified theorem category_theory.limits.cokernel_cofork.condition

added theorem category_theory.limits.cokernel_cofork.π_eq_zero

modified def category_theory.limits.kernel.is_limit_cone_zero_cone

deleted def category_theory.limits.kernel.zero_cone

added def category_theory.limits.kernel.zero_kernel_fork

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

modified theorem category_theory.limits.multicofork.condition

modified theorem category_theory.limits.multicofork.snd_app_right

deleted theorem category_theory.limits.multicofork.to_sigma_cofork_ι_app_one

deleted theorem category_theory.limits.multicofork.to_sigma_cofork_ι_app_zero

added theorem category_theory.limits.multicofork.to_sigma_cofork_π

modified theorem category_theory.limits.multicofork.π_eq_app_right

added theorem category_theory.limits.multifork.app_left_eq_ι

deleted theorem category_theory.limits.multifork.app_left_fst

deleted theorem category_theory.limits.multifork.app_left_snd

added theorem category_theory.limits.multifork.app_right_eq_ι_comp_fst

added theorem category_theory.limits.multifork.app_right_eq_ι_comp_snd

added theorem category_theory.limits.multifork.hom_comp_ι

modified theorem category_theory.limits.multifork.pi_condition

modified theorem category_theory.limits.multifork.to_pi_fork_π_app_zero

modified def category_theory.limits.multifork.ι

deleted theorem category_theory.limits.multifork.ι_eq_app_left

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

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

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

added theorem category_theory.is_split_coequalizer.as_cofork_π

Modified src/category_theory/monad/coequalizer.lean

added theorem category_theory.monad.beck_coequalizer_desc

added theorem category_theory.monad.beck_cofork_π

Modified src/category_theory/monad/monadicity.lean

added theorem category_theory.monad.monadicity_internal.unit_cofork_π

Modified src/category_theory/preadditive/default.lean

Modified src/category_theory/sites/limits.lean

Modified src/category_theory/sites/sheaf.lean

Modified src/topology/sheaves/sheaf_condition/pairwise_intersections.lean