Commit 2026-10-07 11:50 6a70a27c

chore(CategoryTheory/Limits/Shapes/Products): deprecate duplicates piFunctor and sigmaFunctor (#44592) Mathlib/CategoryTheory/Limits/Shapes/Products.lean defines the functor C ⥤ Type wᵒᵖ ⥤ C, (X, n) ↦ ∏ᶜ fun _ : n ↦ X, twice: as piConst (L504) and as piFunctor (L715). It also defines its dual C ⥤ Type w ⥤ C, (X, n) ↦ ∐ fun _ : n ↦ X, twice: as sigmaConst (L521) and as sigmaFunctor (L725). The two definitions in each pair have the same obj/map fields (Pi.map' f.unop fun _ ↦ 𝟙 _ and Pi.map fun _ ↦ f, and dually), so they are equal by rfl. Their @[simps] lemmas (_obj_obj, _obj_map, _map_app) have the same statements up to bound-variable names. This PR keeps piConst and sigmaConst: piConstAdj/sigmaConstAdj are stated in terms of them, and sigmaConst is used throughout Mathlib (Limits/Preserves/SigmaConst.lean, Limits/MonoCoprod.lean, Preadditive/AdditiveFunctor.lean, ModuleCat/Sheaf/Free.lean, simplicial homology). piFunctor and sigmaFunctor become deprecated aliases of piConst and sigmaConst, and their six simps lemmas become deprecated aliases of the matching piConst_*/sigmaConst_* lemmas. The only use of either deprecated name was piFunctor.{w}.flip in GrothendieckTopology.Point.skyscraperPresheafFunctor (Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean:35). It now reads (Φ.fiber.op ⋙ piConst.flip).flip. The @[simps!] lemmas of skyscraperPresheafFunctor keep the same statements. (AlgebraicGeometry.Scheme.Cover.sigmaFunctor is an unrelated declaration and is not touched.)