Commit 2023-03-04 18:09 061def78

View on Github →

feat: port CategoryTheory.Limits.Shapes.BinaryProducts (#2507)

Estimated changes

Modified Mathlib.lean

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

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

added theorem CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext

added def CategoryTheory.Limits.BinaryCofan.IsColimit.mk

added def CategoryTheory.Limits.BinaryCofan.isColimitFlip

added def CategoryTheory.Limits.BinaryCofan.isColimitMk

added theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl

added theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr

added def CategoryTheory.Limits.BinaryCofan.mk

added theorem CategoryTheory.Limits.BinaryCofan.mk_inl

added theorem CategoryTheory.Limits.BinaryCofan.mk_inr

added theorem CategoryTheory.Limits.BinaryCofan.ι_app_left

added theorem CategoryTheory.Limits.BinaryCofan.ι_app_right

added theorem CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext

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

added def CategoryTheory.Limits.BinaryFan.IsLimit.mk

added def CategoryTheory.Limits.BinaryFan.isLimitFlip

added def CategoryTheory.Limits.BinaryFan.isLimitMk

added theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst

added theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd

added def CategoryTheory.Limits.BinaryFan.mk

added theorem CategoryTheory.Limits.BinaryFan.mk_fst

added theorem CategoryTheory.Limits.BinaryFan.mk_snd

added theorem CategoryTheory.Limits.BinaryFan.π_app_left

added theorem CategoryTheory.Limits.BinaryFan.π_app_right

added def CategoryTheory.Limits.WalkingPair.equivBool

added theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_left

added theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_right

added theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false

added theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true

added def CategoryTheory.Limits.WalkingPair.swap

added theorem CategoryTheory.Limits.WalkingPair.swap_apply_left

added theorem CategoryTheory.Limits.WalkingPair.swap_apply_right

added theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff

added theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt

added inductive CategoryTheory.Limits.WalkingPair

added theorem CategoryTheory.Limits.braid_natural

added def CategoryTheory.Limits.coprod.associator

added theorem CategoryTheory.Limits.coprod.associator_naturality

added def CategoryTheory.Limits.coprod.braiding

added def CategoryTheory.Limits.coprod.desc'

added theorem CategoryTheory.Limits.coprod.desc_comp

added theorem CategoryTheory.Limits.coprod.desc_comp_assoc

added theorem CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr

added theorem CategoryTheory.Limits.coprod.desc_inl_inr

added theorem CategoryTheory.Limits.coprod.diag_comp

added def CategoryTheory.Limits.coprod.functor

added def CategoryTheory.Limits.coprod.functorLeftComp

added theorem CategoryTheory.Limits.coprod.hom_ext

added theorem CategoryTheory.Limits.coprod.inl_desc

added theorem CategoryTheory.Limits.coprod.inl_map

added theorem CategoryTheory.Limits.coprod.inr_desc

added theorem CategoryTheory.Limits.coprod.inr_map

added def CategoryTheory.Limits.coprod.leftUnitor

added def CategoryTheory.Limits.coprod.map

added def CategoryTheory.Limits.coprod.mapIso

added theorem CategoryTheory.Limits.coprod.map_codiag

added theorem CategoryTheory.Limits.coprod.map_comp_id

added theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag

added theorem CategoryTheory.Limits.coprod.map_desc

added theorem CategoryTheory.Limits.coprod.map_id_comp

added theorem CategoryTheory.Limits.coprod.map_id_id

added theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag

added theorem CategoryTheory.Limits.coprod.map_map

added theorem CategoryTheory.Limits.coprod.map_swap

added theorem CategoryTheory.Limits.coprod.pentagon

added def CategoryTheory.Limits.coprod.rightUnitor

added theorem CategoryTheory.Limits.coprod.symmetry'

added theorem CategoryTheory.Limits.coprod.symmetry

added theorem CategoryTheory.Limits.coprod.triangle

added def CategoryTheory.Limits.coprodComparison

added def CategoryTheory.Limits.coprodComparisonNatIso

added def CategoryTheory.Limits.coprodComparisonNatTrans

added theorem CategoryTheory.Limits.coprodComparison_inl

added theorem CategoryTheory.Limits.coprodComparison_inr

added theorem CategoryTheory.Limits.coprodComparison_inv_natural

added theorem CategoryTheory.Limits.coprodComparison_natural

added def CategoryTheory.Limits.coprodIsCoprod

added def CategoryTheory.Limits.diagramIsoPair

added theorem CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair

added theorem CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair

added theorem CategoryTheory.Limits.inv_prodComparison_map_fst

added theorem CategoryTheory.Limits.inv_prodComparison_map_snd

added def CategoryTheory.Limits.isoBinaryCofanMk

added def CategoryTheory.Limits.isoBinaryFanMk

added def CategoryTheory.Limits.mapPair

added def CategoryTheory.Limits.mapPairIso

added theorem CategoryTheory.Limits.mapPair_left

added theorem CategoryTheory.Limits.mapPair_right

added theorem CategoryTheory.Limits.map_inl_inv_coprodComparison

added theorem CategoryTheory.Limits.map_inr_inv_coprodComparison

added def CategoryTheory.Limits.pair

added def CategoryTheory.Limits.pairComp

added def CategoryTheory.Limits.pairFunction

added theorem CategoryTheory.Limits.pairFunction_left

added theorem CategoryTheory.Limits.pairFunction_right

added theorem CategoryTheory.Limits.pair_obj_left

added theorem CategoryTheory.Limits.pair_obj_right

added def CategoryTheory.Limits.prod.associator

added theorem CategoryTheory.Limits.prod.associator_naturality

added def CategoryTheory.Limits.prod.braiding

added theorem CategoryTheory.Limits.prod.comp_diag

added theorem CategoryTheory.Limits.prod.comp_lift

added theorem CategoryTheory.Limits.prod.diag_map

added theorem CategoryTheory.Limits.prod.diag_map_fst_snd

added theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp

added def CategoryTheory.Limits.prod.functor

added def CategoryTheory.Limits.prod.functorLeftComp

added theorem CategoryTheory.Limits.prod.hom_ext

added def CategoryTheory.Limits.prod.leftUnitor

added theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality

added theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality

added def CategoryTheory.Limits.prod.lift'

added theorem CategoryTheory.Limits.prod.lift_fst

added theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp

added theorem CategoryTheory.Limits.prod.lift_fst_snd

added theorem CategoryTheory.Limits.prod.lift_map

added theorem CategoryTheory.Limits.prod.lift_snd

added def CategoryTheory.Limits.prod.map

added def CategoryTheory.Limits.prod.mapIso

added theorem CategoryTheory.Limits.prod.map_comp_id

added theorem CategoryTheory.Limits.prod.map_fst

added theorem CategoryTheory.Limits.prod.map_id_comp

added theorem CategoryTheory.Limits.prod.map_id_id

added theorem CategoryTheory.Limits.prod.map_map

added theorem CategoryTheory.Limits.prod.map_snd

added theorem CategoryTheory.Limits.prod.map_swap

added theorem CategoryTheory.Limits.prod.pentagon

added def CategoryTheory.Limits.prod.rightUnitor

added theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality

added theorem CategoryTheory.Limits.prod.symmetry'

added theorem CategoryTheory.Limits.prod.symmetry

added theorem CategoryTheory.Limits.prod.triangle

added def CategoryTheory.Limits.prodComparison

added def CategoryTheory.Limits.prodComparisonNatIso

added def CategoryTheory.Limits.prodComparisonNatTrans

added theorem CategoryTheory.Limits.prodComparison_fst

added theorem CategoryTheory.Limits.prodComparison_inv_natural

added theorem CategoryTheory.Limits.prodComparison_natural

added theorem CategoryTheory.Limits.prodComparison_snd

added def CategoryTheory.Limits.prodIsProd

added theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality

added def CategoryTheory.Over.coprod

added def CategoryTheory.Over.coprodObj