Commit 2025-06-02 10:27 9c388d14

feat(CommAlgCat): the category of commutative algebras (#23601) Define the category of commutative R-algebras. This is the same as Under R up to two details:

• A : CommAlg R contains the data of both algebraMap R A : R → A and Algebra.smul : R → A → A. A : Under R only contains algebraMap R A, meaning that going back and forth between Under R and unbundled algebras is painful/nigh impossible.
• If A : Under R, then A must live in the same universe as R From Toric, FLT Closes #19299