Commit 2026-08-30 19:33 e62ea4d7

perf: fix LocalCohomology.lean (#43236) The bump to v4.34.0-rc2 made the (leaf) file Algebra/Homology/LocalCohomology.lean very slow. It seems the culprit was the isomorphism localCohomology.diagramComp, whose body was an Iso.refl _ abusing several definition equalities of functors (strict associativity, Functor.opComp, etc.). It also looks like the universe setup in this file was using the bad pattern of typing rings in max u v to ensure that certain colimits exist, instead of letting the universe be free and assuming that the colimits exist (which is then automatic for reasonable universes). Some time in the file was probably lost to universe normalization. This file will probably have to be refactored further in the future as it relies on the to-be-deprecated Ext, instead of using CategoryTheory.Abelian.Ext.