Commit 2024-11-10 09:28 b696b352

chore(Topology/Sheaves): split off results on sheaves of rings (#18762) I noticed when debugging #18734 that Topology/Sheaves/Stalks.lean imports ordered rings / groups / monoids, but those are not at all used. This will be fixed if we split off the import of CommRingCat in the sheaf constructions into their own files. This moves all declarations in Topology/Sheaves involving CommRingCat into a new file Sheaves/CommRingCat.lean, except those of Sheaves/Operations.lean since that file is already entirely about sheaves of rings. (I am not at all comfortable in this area of the library, so I expect the file name and docs are highly suboptimal. I welcome all corrections to my ignorance :D)