Commit 2023-04-25 06:14 ed5009fb

View on Github →

feat: port CategoryTheory.Limits.Shapes.WideEqualizers (#2713)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.Cocone.ofCotrident

added theorem CategoryTheory.Limits.Cocone.ofCotrident_ι

added def CategoryTheory.Limits.Cone.ofTrident

added theorem CategoryTheory.Limits.Cone.ofTrident_π

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

added def CategoryTheory.Limits.Cotrident.IsColimit.homIso

added theorem CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural

added theorem CategoryTheory.Limits.Cotrident.IsColimit.hom_ext

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

added def CategoryTheory.Limits.Cotrident.IsColimit.mk

added theorem CategoryTheory.Limits.Cotrident.app_one

added theorem CategoryTheory.Limits.Cotrident.coequalizer_ext

added theorem CategoryTheory.Limits.Cotrident.condition

added def CategoryTheory.Limits.Cotrident.ext

added def CategoryTheory.Limits.Cotrident.mkHom

added def CategoryTheory.Limits.Cotrident.ofCocone

added theorem CategoryTheory.Limits.Cotrident.ofCocone_ι

added def CategoryTheory.Limits.Cotrident.ofπ

added theorem CategoryTheory.Limits.Cotrident.π_eq_app_one

added theorem CategoryTheory.Limits.Cotrident.π_ofπ

added def CategoryTheory.Limits.Trident.IsLimit.homIso

added theorem CategoryTheory.Limits.Trident.IsLimit.homIso_natural

added theorem CategoryTheory.Limits.Trident.IsLimit.hom_ext

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

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

added def CategoryTheory.Limits.Trident.IsLimit.mk

added theorem CategoryTheory.Limits.Trident.app_zero

added theorem CategoryTheory.Limits.Trident.condition

added theorem CategoryTheory.Limits.Trident.equalizer_ext

added def CategoryTheory.Limits.Trident.ext

added def CategoryTheory.Limits.Trident.mkHom

added def CategoryTheory.Limits.Trident.ofCone

added theorem CategoryTheory.Limits.Trident.ofCone_π

added def CategoryTheory.Limits.Trident.ofι

added theorem CategoryTheory.Limits.Trident.ι_eq_app_zero

added theorem CategoryTheory.Limits.Trident.ι_ofι

added def CategoryTheory.Limits.WalkingParallelFamily.Hom.comp

added inductive CategoryTheory.Limits.WalkingParallelFamily.Hom

added theorem CategoryTheory.Limits.WalkingParallelFamily.hom_id

added inductive CategoryTheory.Limits.WalkingParallelFamily

added def CategoryTheory.Limits.diagramIsoParallelFamily

added theorem CategoryTheory.Limits.epi_of_isColimit_parallelFamily

added theorem CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily

added theorem CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily

added theorem CategoryTheory.Limits.mono_of_isLimit_parallelFamily

added def CategoryTheory.Limits.parallelFamily

added theorem CategoryTheory.Limits.parallelFamily_map_left

added theorem CategoryTheory.Limits.parallelFamily_obj_one

added theorem CategoryTheory.Limits.parallelFamily_obj_zero

added def CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair

added theorem CategoryTheory.Limits.wideCoequalizer.condition

added theorem CategoryTheory.Limits.wideCoequalizer.cotrident_ι_app_one

added theorem CategoryTheory.Limits.wideCoequalizer.cotrident_π

added def CategoryTheory.Limits.wideCoequalizer.desc'

added theorem CategoryTheory.Limits.wideCoequalizer.hom_ext

added theorem CategoryTheory.Limits.wideCoequalizer.π_desc

added def CategoryTheory.Limits.wideCoequalizerIsWideCoequalizer

added theorem CategoryTheory.Limits.wideEqualizer.condition

added theorem CategoryTheory.Limits.wideEqualizer.hom_ext

added def CategoryTheory.Limits.wideEqualizer.lift'

added theorem CategoryTheory.Limits.wideEqualizer.lift_ι

added theorem CategoryTheory.Limits.wideEqualizer.trident_ι

added theorem CategoryTheory.Limits.wideEqualizer.trident_π_app_zero

added def CategoryTheory.Limits.wideEqualizerIsWideEqualizer