Commit 2025-10-28 13:23 15729257
View on Github →feat(AlgebraicGeometry): generalise Proj and HomogeneousLocalization to graded rings (#30302)
This PR generalises AlgebraicGeometry.Proj to take in a graded ring (with an arbitrary AddSubgroupClass in a CommRing). Currently it takes in a GradedAlgebra. HomogeneousLocalization is also generalised to graded ring.
Zulip discussion: #mathlib4 >Proj should take GradedRing