Commit 2023-08-05 10:32 675f2fd9

View on Github →

feat: (co/bi/)products unchanged by reindexing and isomorphism of factors (#6259)

Estimated changes

Modified Mathlib/Algebra/Homology/DifferentialObject.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

added theorem CategoryTheory.eqToHom_iso_hom_naturality

added theorem CategoryTheory.eqToHom_iso_inv_naturality

added theorem CategoryTheory.eqToHom_naturality

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

added def CategoryTheory.Limits.biproduct.whisker_equiv

added theorem CategoryTheory.Limits.biproduct.whisker_equiv_hom_eq_lift

added theorem CategoryTheory.Limits.biproduct.whisker_equiv_inv_eq_lift

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

added def CategoryTheory.Limits.Pi.whisker_equiv

added def CategoryTheory.Limits.Sigma.whisker_equiv