Commit 2023-03-07 13:12 4037792e

View on Github →

feat: port CategoryTheory.Limits.Shapes.Products (#2564)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.Cofan.mk

added def CategoryTheory.Limits.Fan.mk

added def CategoryTheory.Limits.Fan.proj

added def CategoryTheory.Limits.Pi.reindex

added theorem CategoryTheory.Limits.Pi.reindex_hom_π

added theorem CategoryTheory.Limits.Pi.reindex_inv_π

added def CategoryTheory.Limits.Sigma.reindex

added theorem CategoryTheory.Limits.Sigma.ι_reindex_hom

added theorem CategoryTheory.Limits.Sigma.ι_reindex_inv

added def CategoryTheory.Limits.colimitCoconeOfUnique

added def CategoryTheory.Limits.coproductIsCoproduct

added def CategoryTheory.Limits.coproductUniqueIso

added theorem CategoryTheory.Limits.fan_mk_proj

added theorem CategoryTheory.Limits.hasProducts_of_limit_fans

added theorem CategoryTheory.Limits.has_smallest_coproducts_of_hasCoproducts

added theorem CategoryTheory.Limits.has_smallest_products_of_hasProducts

added def CategoryTheory.Limits.limitConeOfUnique

added theorem CategoryTheory.Limits.map_lift_piComparison

added def CategoryTheory.Limits.mkFanLimit

added def CategoryTheory.Limits.piComparison

added theorem CategoryTheory.Limits.piComparison_comp_π

added def CategoryTheory.Limits.productIsProduct

added def CategoryTheory.Limits.productUniqueIso

added def CategoryTheory.Limits.sigmaComparison

added theorem CategoryTheory.Limits.sigmaComparison_map_desc

added theorem CategoryTheory.Limits.ι_comp_sigmaComparison