Commit 2023-08-26 20:43 0beb1d08

View on Github →

feat: construct maps between products with different indexing types (#6792)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

added def CategoryTheory.Limits.biproduct.whiskerEquiv

added theorem CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift

added theorem CategoryTheory.Limits.biproduct.whiskerEquiv_inv_eq_lift

deleted def CategoryTheory.Limits.biproduct.whisker_equiv

deleted theorem CategoryTheory.Limits.biproduct.whisker_equiv_hom_eq_lift

deleted theorem CategoryTheory.Limits.biproduct.whisker_equiv_inv_eq_lift

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

added def CategoryTheory.Limits.Pi.map'

added theorem CategoryTheory.Limits.Pi.map'_comp_map'

added theorem CategoryTheory.Limits.Pi.map'_comp_map

added theorem CategoryTheory.Limits.Pi.map'_comp_π

added theorem CategoryTheory.Limits.Pi.map'_id

added theorem CategoryTheory.Limits.Pi.map_comp_map'

added theorem CategoryTheory.Limits.Pi.map_comp_map

added def CategoryTheory.Limits.Pi.whiskerEquiv

deleted def CategoryTheory.Limits.Pi.whisker_equiv

added def CategoryTheory.Limits.Sigma.map'

added theorem CategoryTheory.Limits.Sigma.map'_comp_map'

added theorem CategoryTheory.Limits.Sigma.map'_comp_map

added theorem CategoryTheory.Limits.Sigma.map'_id

added theorem CategoryTheory.Limits.Sigma.map_comp_map'

added theorem CategoryTheory.Limits.Sigma.map_comp_map

added def CategoryTheory.Limits.Sigma.whiskerEquiv

deleted def CategoryTheory.Limits.Sigma.whisker_equiv

added theorem CategoryTheory.Limits.Sigma.ι_comp_map'