Commit 2026-04-23 07:52 dd465758

View on Github →

chore(CategoryTheory/Limits): make Pi.mapIso a def (#38368) Currently, simp unfolds Pi.mapIso which makes the general (co)limit API leak through. We also fix Sigma.mapIso, Pi.map and Sigma.map.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean

Modified Mathlib/CategoryTheory/Limits/FormalCoproducts/Cech.lean

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

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

added def CategoryTheory.Limits.Pi.map

added def CategoryTheory.Limits.Pi.mapIso

added theorem CategoryTheory.Limits.Pi.mapIso_hom_π

added theorem CategoryTheory.Limits.Pi.mapIso_inv_π

added def CategoryTheory.Limits.Sigma.map

added def CategoryTheory.Limits.Sigma.mapIso

added theorem CategoryTheory.Limits.Sigma.ι_mapIso_hom

added theorem CategoryTheory.Limits.Sigma.ι_mapIso_inv

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

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean