Commit 2023-03-08 18:34 e8ba64d9

View on Github →

feat: port CategoryTheory.Limits.Preserves.Shapes.Biproducts (#2727)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean

added def CategoryTheory.Functor.biprodComparison'

added theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison

added def CategoryTheory.Functor.biprodComparison

added theorem CategoryTheory.Functor.biprodComparison_fst

added theorem CategoryTheory.Functor.biprodComparison_snd

added def CategoryTheory.Functor.biproductComparison'

added theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison

added def CategoryTheory.Functor.biproductComparison

added theorem CategoryTheory.Functor.biproductComparison_π

added theorem CategoryTheory.Functor.inl_biprodComparison'

added theorem CategoryTheory.Functor.inr_biprodComparison'

added def CategoryTheory.Functor.mapBicone

added theorem CategoryTheory.Functor.mapBicone_whisker

added def CategoryTheory.Functor.mapBinaryBicone

added def CategoryTheory.Functor.mapBiprod

added theorem CategoryTheory.Functor.mapBiprod_hom

added theorem CategoryTheory.Functor.mapBiprod_inv

added def CategoryTheory.Functor.mapBiproduct

added theorem CategoryTheory.Functor.mapBiproduct_hom

added theorem CategoryTheory.Functor.mapBiproduct_inv

added def CategoryTheory.Functor.splitEpiBiprodComparison

added def CategoryTheory.Functor.splitEpiBiproductComparison

added def CategoryTheory.Functor.splitMonoBiprodComparison'

added def CategoryTheory.Functor.splitMonoBiproductComparison'

added theorem CategoryTheory.Functor.ι_biproductComparison'

added theorem CategoryTheory.Limits.biprod.lift_mapBiprod

added theorem CategoryTheory.Limits.biprod.mapBiprod_hom_desc

added theorem CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc

added theorem CategoryTheory.Limits.biprod.map_lift_mapBiprod

added theorem CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc

added theorem CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc

added theorem CategoryTheory.Limits.biproduct.map_lift_mapBiprod

added def CategoryTheory.Limits.isBilimitOfPreserves

added def CategoryTheory.Limits.isBinaryBilimitOfPreserves

added def CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBiproduct

added def CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBiproducts

added def CategoryTheory.Limits.preservesBiproductsShrink