Commit 2025-07-07 07:35 e7aa4d48

chore(CategoryTheory/Localization): fix morphisms in the category of resolutions (#26375) This PR changes the definition of morphisms in the categories LeftResolution and RightResolution attached to morphisms of localizers. Previously, we assumed that morphisms between resolutions belonged to the given class of morphisms of the localizer, but in downstream applications, it turns out it is more convenient to remove this condition (which would anyway be automatically verified in most situations). (The literature is not very explicit about whether this condition should or should not be part of the definition.)