Commit 2026-09-21 22:59 acaacc12

View on Github →

chore(CategoryTheory): use the map attribute (#43863)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean

Modified Mathlib/Algebra/Homology/ShortComplex/Basic.lean

Modified Mathlib/CategoryTheory/Equivalence.lean

Modified Mathlib/CategoryTheory/Functor/Category.lean

Modified Mathlib/CategoryTheory/Functor/Trifunctor.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Iso.lean

Modified Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Localization/SmallHom.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/DayConvolution.lean

Modified Mathlib/CategoryTheory/Monoidal/DayConvolution/Braided.lean

Modified Mathlib/CategoryTheory/Monoidal/DayConvolution/Closed.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

modified theorem CategoryTheory.Functor.Monoidal.map_δ_μ

modified theorem CategoryTheory.Functor.Monoidal.map_ε_η

modified theorem CategoryTheory.Functor.Monoidal.map_η_ε

modified theorem CategoryTheory.Functor.Monoidal.map_μ_δ

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/CategoryTheory/NatIso.lean

Modified Mathlib/CategoryTheory/NatTrans.lean

Modified Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

Modified Mathlib/CategoryTheory/Sites/Descent/DescentDataPrime.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

Modified Mathlib/Tactic/Widget/StringDiagram.lean