Commit 2023-03-24 15:22 386b7cee

View on Github →

feat: port CategoryTheory.Limits.Shapes.Types (#2809)

Estimated changes

Modified Mathlib.lean

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

added inductive CategoryTheory.Limits.Types.CoequalizerRel

added theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff

added def CategoryTheory.Limits.Types.binaryCoproductCocone

added def CategoryTheory.Limits.Types.binaryCoproductColimit

added def CategoryTheory.Limits.Types.binaryCoproductColimitCocone

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom

added theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv

added def CategoryTheory.Limits.Types.binaryProductCone

added theorem CategoryTheory.Limits.Types.binaryProductCone_fst

added theorem CategoryTheory.Limits.Types.binaryProductCone_snd

added def CategoryTheory.Limits.Types.binaryProductFunctor

added theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst

added theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd

added theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst

added theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd

added def CategoryTheory.Limits.Types.binaryProductLimit

added def CategoryTheory.Limits.Types.binaryProductLimitCone

added def CategoryTheory.Limits.Types.coequalizerColimit

added theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv

added theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom

added theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq

added def CategoryTheory.Limits.Types.coproductColimitCocone

added theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv

added theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom

added theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype

added theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι

added def CategoryTheory.Limits.Types.equalizerLimit

added def CategoryTheory.Limits.Types.initialColimitCocone

added theorem CategoryTheory.Limits.Types.pi_lift_π_apply

added theorem CategoryTheory.Limits.Types.pi_map_π_apply

added theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval

added theorem CategoryTheory.Limits.Types.productIso_inv_comp_π

added def CategoryTheory.Limits.Types.productLimitCone

added theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst

added theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd

added theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst

added theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd

added def CategoryTheory.Limits.Types.pullbackLimitCone

added def CategoryTheory.Limits.Types.terminalLimitCone

added theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique

added theorem CategoryTheory.Limits.Types.unique_of_type_equalizer