Commit 2023-03-02 18:17 49552cd3

View on Github →

feat: port CategoryTheory.Limits.Shapes.Equalizers (#2562)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.Cocone.ofCofork

added theorem CategoryTheory.Limits.Cocone.ofCofork_ι

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

added theorem CategoryTheory.Limits.Cofork.IsColimit.existsUnique

added def CategoryTheory.Limits.Cofork.IsColimit.homIso

added theorem CategoryTheory.Limits.Cofork.IsColimit.homIso_natural

added theorem CategoryTheory.Limits.Cofork.IsColimit.hom_ext

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

added def CategoryTheory.Limits.Cofork.IsColimit.mk

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

added theorem CategoryTheory.Limits.Cofork.app_one_eq_π

added theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left

added theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right

added theorem CategoryTheory.Limits.Cofork.coequalizer_ext

added theorem CategoryTheory.Limits.Cofork.condition

added def CategoryTheory.Limits.Cofork.ext

added def CategoryTheory.Limits.Cofork.isoCoforkOfπ

added def CategoryTheory.Limits.Cofork.mkHom

added def CategoryTheory.Limits.Cofork.ofCocone

added theorem CategoryTheory.Limits.Cofork.ofCocone_ι

added def CategoryTheory.Limits.Cofork.ofπ

added def CategoryTheory.Limits.Cofork.π

added theorem CategoryTheory.Limits.Cofork.π_ofπ

added theorem CategoryTheory.Limits.Cofork.π_precompose

added def CategoryTheory.Limits.Cone.ofFork

added theorem CategoryTheory.Limits.Cone.ofFork_π

added theorem CategoryTheory.Limits.Fork.IsLimit.existsUnique

added def CategoryTheory.Limits.Fork.IsLimit.homIso

added theorem CategoryTheory.Limits.Fork.IsLimit.homIso_natural

added theorem CategoryTheory.Limits.Fork.IsLimit.hom_ext

added def CategoryTheory.Limits.Fork.IsLimit.lift'

added theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι

added def CategoryTheory.Limits.Fork.IsLimit.mk'

added def CategoryTheory.Limits.Fork.IsLimit.mk

added theorem CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left

added theorem CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right

added theorem CategoryTheory.Limits.Fork.app_zero_eq_ι

added theorem CategoryTheory.Limits.Fork.condition

added theorem CategoryTheory.Limits.Fork.equalizer_ext

added def CategoryTheory.Limits.Fork.ext

added theorem CategoryTheory.Limits.Fork.hom_comp_ι

added def CategoryTheory.Limits.Fork.isoForkOfι

added def CategoryTheory.Limits.Fork.mkHom

added def CategoryTheory.Limits.Fork.ofCone

added theorem CategoryTheory.Limits.Fork.ofCone_π

added def CategoryTheory.Limits.Fork.ofι

added def CategoryTheory.Limits.Fork.ι

added theorem CategoryTheory.Limits.Fork.ι_ofι

added theorem CategoryTheory.Limits.Fork.ι_postcompose

added theorem CategoryTheory.Limits.Fork.π_comp_hom

added inductive CategoryTheory.Limits.WalkingParallelPair

added theorem CategoryTheory.Limits.WalkingParallelPairHom.assoc

added def CategoryTheory.Limits.WalkingParallelPairHom.comp

added theorem CategoryTheory.Limits.WalkingParallelPairHom.comp_id

added theorem CategoryTheory.Limits.WalkingParallelPairHom.id.sizeOf_spec'

added theorem CategoryTheory.Limits.WalkingParallelPairHom.id_comp

added inductive CategoryTheory.Limits.WalkingParallelPairHom

added theorem CategoryTheory.Limits.coconeOfIsSplitEpi_π

added theorem CategoryTheory.Limits.coequalizer.cofork_ι_app_one

added theorem CategoryTheory.Limits.coequalizer.cofork_π

added theorem CategoryTheory.Limits.coequalizer.condition

added theorem CategoryTheory.Limits.coequalizer.existsUnique

added theorem CategoryTheory.Limits.coequalizer.hom_ext

added theorem CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom

added theorem CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv

added theorem CategoryTheory.Limits.coequalizer.π_colimMap_desc

added theorem CategoryTheory.Limits.coequalizer.π_desc

added theorem CategoryTheory.Limits.coequalizer.π_of_eq

added theorem CategoryTheory.Limits.coequalizerComparison_map_desc

added theorem CategoryTheory.Limits.coneOfIsSplitMono_ι

added def CategoryTheory.Limits.diagramIsoParallelPair

added theorem CategoryTheory.Limits.epi_of_isColimit_cofork

added theorem CategoryTheory.Limits.eq_of_epi_equalizer

added theorem CategoryTheory.Limits.eq_of_epi_fork_ι

added theorem CategoryTheory.Limits.eq_of_mono_coequalizer

added theorem CategoryTheory.Limits.eq_of_mono_cofork_π

added theorem CategoryTheory.Limits.equalizer.condition

added theorem CategoryTheory.Limits.equalizer.existsUnique

added theorem CategoryTheory.Limits.equalizer.fork_ι

added theorem CategoryTheory.Limits.equalizer.fork_π_app_zero

added theorem CategoryTheory.Limits.equalizer.hom_ext

added theorem CategoryTheory.Limits.equalizer.isoSourceOfSelf_hom

added theorem CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv

added theorem CategoryTheory.Limits.equalizer.lift_ι

added theorem CategoryTheory.Limits.equalizer.ι_of_eq

added theorem CategoryTheory.Limits.equalizerComparison_comp_π

added theorem CategoryTheory.Limits.hasCoequalizer_epi_comp

added theorem CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair

added theorem CategoryTheory.Limits.hasEqualizer_comp_mono

added theorem CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair

added def CategoryTheory.Limits.idCofork

added def CategoryTheory.Limits.idFork

added def CategoryTheory.Limits.isCoequalizerEpiComp

added def CategoryTheory.Limits.isColimitIdCofork

added def CategoryTheory.Limits.isEqualizerCompMono

added theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq

added theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self

added theorem CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi

added theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi

added theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq

added theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self

added def CategoryTheory.Limits.isLimitIdFork

added theorem CategoryTheory.Limits.map_lift_equalizerComparison

added theorem CategoryTheory.Limits.mono_of_isLimit_fork

added def CategoryTheory.Limits.parallelPair.eqOfHomEq

added def CategoryTheory.Limits.parallelPair.ext

added def CategoryTheory.Limits.parallelPair

added def CategoryTheory.Limits.parallelPairHom

added theorem CategoryTheory.Limits.parallelPairHom_app_one

added theorem CategoryTheory.Limits.parallelPairHom_app_zero

added theorem CategoryTheory.Limits.parallelPair_functor_obj

added theorem CategoryTheory.Limits.parallelPair_map_left

added theorem CategoryTheory.Limits.parallelPair_map_right

added theorem CategoryTheory.Limits.parallelPair_obj_one

added theorem CategoryTheory.Limits.parallelPair_obj_zero

added def CategoryTheory.Limits.splitEpiOfCoequalizer

added def CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork

added def CategoryTheory.Limits.splitMonoOfEqualizer

added def CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork

added theorem CategoryTheory.Limits.walkingParallelPairHom_id

added def CategoryTheory.Limits.walkingParallelPairOp

added def CategoryTheory.Limits.walkingParallelPairOpEquiv

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero

added theorem CategoryTheory.Limits.walkingParallelPairOp_left

added theorem CategoryTheory.Limits.walkingParallelPairOp_one

added theorem CategoryTheory.Limits.walkingParallelPairOp_right

added theorem CategoryTheory.Limits.walkingParallelPairOp_zero

added theorem CategoryTheory.Limits.ι_comp_coequalizerComparison