Commit 2026-10-07 19:00 2d39771f

View on Github →

chore(CategoryTheory/Limits/Shapes/Equalizers): use to_dual (#44215) This PR uses to_dual on Fork/Cofork and Equalizer/Coequalizer. It is done such that the objects zero and one in WalkingParallelPair are dual to each other, and the left and right morphisms in WalkingParallelPairHom are both dual to themselves.

Estimated changes

Modified Mathlib/CategoryTheory/Functor/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

deleted def CategoryTheory.Limits.Cocone.ofCofork

deleted theorem CategoryTheory.Limits.Cocone.ofCofork_ι

deleted def CategoryTheory.Limits.Cofork.IsColimit.desc'

deleted def CategoryTheory.Limits.Cofork.IsColimit.desc

deleted theorem CategoryTheory.Limits.Cofork.IsColimit.epi

deleted theorem CategoryTheory.Limits.Cofork.IsColimit.existsUnique

deleted def CategoryTheory.Limits.Cofork.IsColimit.homIso

deleted theorem CategoryTheory.Limits.Cofork.IsColimit.homIso_natural

deleted theorem CategoryTheory.Limits.Cofork.IsColimit.hom_ext

deleted def CategoryTheory.Limits.Cofork.IsColimit.mk'

deleted def CategoryTheory.Limits.Cofork.IsColimit.mk

deleted theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc'

deleted theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc

deleted theorem CategoryTheory.Limits.Cofork.app_one_eq_π

deleted theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left

deleted theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right

deleted theorem CategoryTheory.Limits.Cofork.coequalizer_ext

deleted theorem CategoryTheory.Limits.Cofork.condition

deleted def CategoryTheory.Limits.Cofork.isoCoforkOfπ

deleted def CategoryTheory.Limits.Cofork.mkHom

deleted def CategoryTheory.Limits.Cofork.ofCocone

deleted theorem CategoryTheory.Limits.Cofork.ofCocone_ι

deleted def CategoryTheory.Limits.Cofork.ofπ

deleted def CategoryTheory.Limits.Cofork.π

added theorem CategoryTheory.Limits.Cofork.π_comp_hom

deleted theorem CategoryTheory.Limits.Cofork.π_ofπ

deleted theorem CategoryTheory.Limits.Cofork.π_precompose

deleted def CategoryTheory.Limits.CoforkOfπ.ext

deleted theorem CategoryTheory.Limits.Fork.π_comp_hom

modified def CategoryTheory.Limits.WalkingParallelPairHom.comp

deleted theorem CategoryTheory.Limits.WalkingParallelPairHom.id_comp

deleted theorem CategoryTheory.Limits.coconeOfIsSplitEpi_π

deleted theorem CategoryTheory.Limits.coequalizer.cofork_ι_app_one

deleted theorem CategoryTheory.Limits.coequalizer.cofork_π

deleted theorem CategoryTheory.Limits.coequalizer.condition

deleted theorem CategoryTheory.Limits.coequalizer.existsUnique

deleted theorem CategoryTheory.Limits.coequalizer.hom_ext

deleted theorem CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom

deleted theorem CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv

deleted theorem CategoryTheory.Limits.coequalizer.π_desc

deleted theorem CategoryTheory.Limits.coequalizer.π_of_eq

deleted theorem CategoryTheory.Limits.coequalizerComparison_map_desc

deleted theorem CategoryTheory.Limits.epi_of_isColimit_cofork

modified theorem CategoryTheory.Limits.eq_of_epi_fork_ι

deleted theorem CategoryTheory.Limits.eq_of_mono_coequalizer

deleted theorem CategoryTheory.Limits.eq_of_mono_cofork_π

deleted theorem CategoryTheory.Limits.hasCoequalizer_epi_comp

deleted theorem CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair

deleted theorem CategoryTheory.Limits.hasEqualizer_comp_mono

deleted def CategoryTheory.Limits.idCofork

deleted def CategoryTheory.Limits.isCoequalizerEpiComp

deleted def CategoryTheory.Limits.isColimitIdCofork

deleted theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq

deleted theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self

deleted theorem CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi

modified theorem CategoryTheory.Limits.mono_of_isLimit_fork

deleted theorem CategoryTheory.Limits.parallelPair_obj_one

deleted def CategoryTheory.Limits.splitEpiOfCoequalizer

deleted def CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork

deleted theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one

deleted theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one

deleted theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one

deleted theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one

deleted theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one

deleted theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one

deleted theorem CategoryTheory.Limits.walkingParallelPairOp_one

deleted theorem CategoryTheory.Limits.ι_comp_coequalizerComparison

Modified Mathlib/Tactic/Translate/GuessName.lean

Modified Mathlib/Tactic/Translate/ToDual.lean