Formalizing Multi-graded Brenner–Schröer Proj Schemes and Dilatations of Rings in Lean4

Abstract We present a formalization in Lean4 of some multi-graded algebraic geometry constructions, focusing on the Brenner–Schröer Proj construction and algebraic dilatations of rings. Multi-graded Proj schemes, defined from rings graded by more general monoids than \(\mathbb {N}\) or \(\mathbb {Z}\), have recently attracted increasing attention and play an important role in several areas of modern algebraic geometry. Our work follows the algebraic approach developed in the literature and provides a formal implementation of multi-graded Proj within the Lean4 theorem prover. In addition, we formalize dilatations of rings, an operation in commutative algebra closely related to localization and to blowup constructions. This article gives a comprehensive account of the definitions, main results, and design choices underlying the formalization. It is intended both as documentation of the development and as a foundation for future extensions in formalized algebraic geometry. The corresponding code is made publicly available, supporting further developments in the formalization of advanced geometric structures. 1 Introduction 1.1 Overview and Objectives of the Formalization Multi-graded algebraic geometry refers to constructions in algebraic geometry built on rings graded by monoids or groups more general than \(\mathbb {N}\) or \(\mathbb {Z}\). In this work, we implement such constructions in Lean 4 [4]. The main focus of this work is the Brenner–Schröer Proj construction, introduced by Brenner and Schröer in [2]. This construction has recently been studied in several works [7, 12] and is poised to become a classical topic in algebraic geometry. Multi-graded Proj schemes are used in several areas of contemporary algebraic geometry, including Lie theory and geometric representation theory [1, §2.3.7] as well as the minimal model program [17]. If A is a ring graded by the natural numbers and regarded as graded by the integers, then Grothendieck’s \(\operatorname {Proj}(A)\) [6] and Brenner–Schröer’s \(\operatorname {Proj}(A)\) [2] are canonically identified [2]. In this work, we provide an implementation of the Brenner–Schröer construction of multi-graded Proj schemes within the Lean 4 theorem prover [4], following the algebraic treatment in Mayeux-Riche [12]. We also formalize dilatations of rings, a fundamental operation in commutative algebra analogous to localization (cf. [5, 11, 15]) and related to blowups and part of the broader area of multi-graded algebraic geometry. Dilatations form a process that adds fractions to rings, refining localizations. They allow one to control that both the numerator and denominator are prescribed [11]. Part of this formalization was announced in the short note [10] and already discussed in the thesis of Jujian Zhang. The code is available on GitHub [9]. This article presents a complete account of the formalization and serves as a guide for future work building on these fundamental constructions. 1.2 Relation to Other Works We now discuss the methods and related works used in this paper. The Grothendieck \(\mathbb {N}\)-graded Proj construction [6] was formalized in Lean by Zhang in [18] and is now in mathlib. The work [18] provided the first example of non-affine schemes ever formalized in a theorem prover. In contrast to [6, 18], where Proj is first defined as a set of prime ideals, in the present work we define multi-graded Proj directly by gluing, following the approach of [12] (itself a minor variation of the approach of [2]), without passing through a set-theoretic construction involving graded ideals. The present development also relies on and is closely inspired by the pioneering formalization of graded algebra in Lean carried out by Zhang and Wieser in [16]. Of course, our work builds on the implementation of the foundations of the theory of schemes in Lean [3], which is now part of mathlib. 1.3 Mathematical Description of Multi-graded Proj Schemes We now describe the technical core of the mathematical content formalized in this paper. We also formalize related results, but the main achievement of this formalization effort concerns the following material. We recommend that readers familiarize themselves with the structure of this section before proceeding with the remainder of the paper, as it provides a roadmap for the material developed in subsequent sections. Let A be a commutative unital ring graded by a finitely generated abelian group \(\iota \). A (multiplicative) submonoid S of A is homogeneous if every element of S is homogeneous. Equivalently a submonoid of A is homogeneous if it is generated by homogeneous elements. In this situation, the localization \(A_S\) of A with respect to S is canonically \(\iota \)-graded. Given a homogeneous (multiplicative) submonoid \(S \subset A\), we will denote by \(\overline{S}\) the homogeneous submonoid consisting of homogeneous divisors of elements in S. Note that we have a canonical isomorphism of graded rings \(A_{ \overline{S}} \cong A_{S}. \) Definition 1 ([2, 12]) Let S be a homogeneous subset of A. We denote by \(\deg (S)\) the subset of M defined as \(\deg (S):= \{ m \in \iota : \exists s \in S, s \in A_m \}. \) Note that \(\deg (\{0\})=\iota \). More generally, if S is a homogeneous submonoid of A, then \(\deg (S)\) is a submonoid of \(\iota \). Definition 2 ([2, 12]) Let S be a homogeneous (multiplicative) submonoid of A. We put \(\iota [S]=\iota [S \rangle ^{\textrm{gp}}= M[S \rangle - M[S \rangle \), the subgroup of M generated by \(\deg (S)\). Formalizations of Definitions 1 and 2 are documented below in Definition 7. Definition 3 ([2, 12]) A homogeneous submonoid S of A is called \(\iota \)-relevant (or just relevant if \(\iota \) is clear from the context) if for any m in \(\iota \) there exists \(n \in \textbf{Z}_{> 0}\) such that nm belongs to \(\iota [\overline{S}]\), i.e. if \(\iota /(\iota [\overline{S}])\) is a torsion abelian group. Formalization of Definition 3 is documented below in Definition 8 (Definition 8 also formalizes related notions of mathematical interest used in [2, 12]). Example 1 For example, let \(A= \mathbb {Z}[X,Y]\) graded by \(\mathbb {Z}^2\) with \(\deg (X)=(1,0)\) and \(\deg (Y)=(0,1)\). The homogeneous submonoid S generated by X in A is not relevant because \(\iota [\overline{S}]= \mathbb {Z} \times 0 \subset \mathbb {Z}^2\). The homogeneous submonoid T generated by XY in A is relevant because \(\iota [\overline{T}]= \mathbb {Z}^2\). Let S be a homogeneous submonoid of A. The degree-0 part \((A_S)_0\) of the localization \(A_{S}\) is denoted \(A_{(S)}\) and is called the potion of A with respect to S. We have a canonical identification \(A_{(\overline{S})} \cong A_{(S)}\). If S and T are submonoids of A, we will denote by ST the submonoid of A generated by \(S \cup T\), i.e. \(ST = \{st: s \in S, \, t \in T \}\). Of course, ST is homogeneous if S and T are. The following is the key result that makes the Proj construction work. Proposition 1 ([12]) Let S and T be homogeneous finitely generated submonoids of A. - 1. We have a canonical homomorphism of potion rings \(A_{(S )} \rightarrow A_{(ST )}\). - 2. Assume that S is relevant. The morphism of schemes \( \textrm{Spec} (A_{(ST )}) \rightarrow \textrm{Spec} (A_{(S)}) \) induced by the ring homomorphism in (1) is an open immersion of schemes. The proof of Proposition 1 (2) consists in showing that \(A_{(ST)}\) can be identified with the localisation of \(A_{(S)}\) with respect to a certain finitely generated submonoid. Proposition 1 corresponds to Theorem 20 (and preliminary material) below. We denote by \(\mathcal {F}_A\) the set of all relevant homogeneous submonoids of A which are finitely generated as submonoids of \((A,\times )\). Definition 4 ([2, 12]) Let \(\mathcal {F} \subset \mathcal {F}_A\) be a subset. For each \(S \in \mathcal {F}\), let \(D_{\dagger }(S)\) be the spectrum of the potion \(A_{(S)}\). If \(S,T \in \mathcal {F}\), the affine scheme \(D_{\dagger }(ST)\) identifies canonically with an open subscheme of \(D_{\dagger }(S)\). For each \(S,T \in \mathcal {F}\), we have equalities \( D_{\dagger }({S S}) = D_{\dagger }(S) \) and \( D_{\dagger }({ST})=D_{\dagger }({TS}). \) Moreover, for each triple \(S,T,U \in \mathcal {F}\), we have \( D_{\dagger }({ST} )\cap D_{\dagger }({SU}) = D_{\dagger }({TS}) \cap D_{\dagger }({TU}). \) Now, by glueing, from these data we obtain a scheme \(\textrm{Proj}_{\mathcal {F} } (A)\) and, for each \(S \in \mathcal {F}\), an open immersion \(\varphi _S: D_{\dagger }(S) \rightarrow \textrm{Proj}_{\mathcal {F}} (A)\), such that \( \textrm{Proj}_{\mathcal {F} } (A) = \bigcup _{S \in \mathcal {F} } \varphi _S( D_{\dagger }(S)). \) In practice, we will often identify \(D_{\dagger }(S) \) and \(\varphi _S (D_{\dagger }(S))\). In the case when \(\mathcal {F} = \mathcal {F}_A\), the scheme \(\textrm{Proj}_{\mathcal {F}_A} (A)\) is the Brenner–Schröer multi-graded Proj scheme. The formalization of Definition 4 is documented below in Construction 6 and Definition 11. 1.4 Relation to Other Multi-graded Constructions and Limits of the Present Work Recall that multi-graded algebraic geometry refers to constructions in algebraic geometry involving rings graded by commutative monoids or groups more general than \(\mathbb {N}\) or \(\mathbb {Z}\). The multi-graded Proj construction also makes sense for multi-graded quasi-coherent algebras; see [12]. Blowups of schemes (possibly multi-centered, cf. [12, 13]) are defined via Proj of multi-graded quasi-coherent algebras. To define the multi-graded Proj of a quasi-coherent algebra, one may glue the Proj constructions of graded rings locally. However, as a limitation of the present work, we do not carry out this global case. We plan to formalize it in a future project, but doing so would require developing a substantial amount of foundational material on schemes in mathlib, going beyond the formalization of multi-graded algebraic geometry. However, this is not out of reach. We believe that, within a few years, the methods developed in the present paper, combined with new material on quasi-coherent sheaves in mathlib, will make it possible to formalize global multi-graded Proj constructions. This limitation provides yet another motivation for pursuing the formalization of the Stacks Project [15]. Another closely related notion is that of affine blowups, also called dilatations. Dilatations of schemes are likewise defined locally via dilatations of rings. They are open subschemes of projective blowups [11, 12]. In the present work, we formalize dilatations of rings. Although the formalization of Proj presented in this paper is very general and involves non-affine schemes, it can still be viewed as a local construction (its input is a ring, rather than a scheme or a quasi-coherent algebra) underlying a more general Proj construction. Similarly, dilatations of rings or affine schemes can be regarded as local special (and necessary) cases of the more general global construction of dilatations of schemes. In future independent works, one may envision a complete formalization of multi-graded algebraic geometry in Lean. 1.5 Content Section 2 is about the general setup we use throughout the paper about graded rings. In this work, a graded ring is a commutative unital ring A together with a grading \(A= \bigoplus _{i \in \iota } A_i\) where \(\iota \) is an abelian monoid \((A_i \cdot A_j \subset A_{i+j})\). From now on, we assume that \(\iota \) is an abelian group in this introduction. A multiplicative submonoid of a graded ring is called homogeneous if its elements are homogeneous. An homogeneous submonoid S is called relevant if the group generated by the degrees of the homogeneous divisors of S is a torsion subgroup of \(\iota \). Section 3 is about homogeneous and relevant submonoids. In Sects. 4 and 5, we study localization of graded rings. Section 6 is devoted to tensor product of graded rings and related technical results. Section 7 formalizes the definition of potions. Potions are rings defined as degree zero part of homogeneous localizations. They are at the heart of the Proj construction. We establish many results on potions in Sects. 7, 8 and 9, these are preliminary to define Proj schemes. The definition of Brenner–Schröer Proj schemes is in Sect. 8. The functoriality of the Proj construction is established in Sect. 10. Section 11 formalizes the definition and the universal property of dilatations of rings. This paper also contains the formalization of several facts on multi-graded algebra, not strictly required to define the definition multi-graded Proj schemes, but are part of the theory of multi-graded Proj schemes. In particular, we formalized material on tensor products of graded rings, lemmas on relevant elements, and the ideal generated by relevant elements. These results will help to apply the theory in relation to applications mentioned in [2, 12]. Finally, we invite the interested reader to consult the full content of the present paper for a complete account of the formalization presented here. 2 General Setup A ring R is said to be graded by a monoid \(\iota \) if \(R \cong \bigoplus _{i\in \iota } R_i\) where \(R_i\) are subgroups of R such that \(R_i R_j \subseteq R_{i + j}\). When working with graded rings on paper, the two rings R and \(\bigoplus _{i\in \iota }R_i\) are often identified. However, during formalisation, in order to have an ergonomic framework for graded rings, we need a way to be able to talk about the two rings as different objects (typically for type theoretical reasons) while maintaining the ability to switch between the two with ease. A full discussion of how graded ring is implemented in Lean4 can be found in [16]. The most general setup is as following: and together assert that the terms of are subgroups of A. In particular, for each term i of , \(\mathcal {A}_i\) is a subgroup of A. In the general setup, we do not use a concrete type like ; this is to avoid code duplication: for example if we assume A to be an R-algebra, by using , we can specialize to be R-submodules of A and realize A as a graded algebra without the needs to duplicate any general result. is an abbreviation for and where is an abbreviation for asserting that 1 has grade zero and asserting that \(\mathcal {A}_i\mathcal {A}_j \subseteq \mathcal {A}_{i+j}\). Similarly, asserts that \(\mathcal {A}_i \cdot \mathcal {M}_j \subseteq \mathcal {M}_{i+j}\) where \(i + j\) is provided by . The general setup here is versatile: by allowing and to be different types, we can have graded rings and modules that are not graded by the same monoid — for example the ring is graded by \(\mathbb {N}\) and the module by \(\mathbb {Z}\). 2.1 Graded Ring Homomorphism Let \(\iota \) be a monoid. Suppose A and B are two \(\iota \)-graded rings with grading \(\mathcal {A}\) and \(\mathcal {B}\) respectively. Definition 5 A graded ring homomorphism from A to B is a ring homomorphism \(f: A \rightarrow B\) such that for all \(i \in \iota \), we have \(f(\mathcal {A}_i) \subseteq \mathcal {B}_i\). In Listing 2, we keep the same notation for ring homomorphisms — is a graded ring homomorphism from A to B. To continue the philosophy that there should be easy ways to switch between the internally graded ring A and the externally graded ring \(\bigoplus _{i\in \iota } \mathcal {A}_i\), for a graded ring homomorphism \(f: A \rightarrow B\), we define the corresponding ring homomorphism \(\bigoplus _{i\in \iota }\mathcal {A}_i \rightarrow \bigoplus _{i\in \iota }\mathcal {B}_i\) by Lemma 2 The kernel of a graded ring homomorphism \(f: A \rightarrow B\) is a homogeneous ideal of A. Proof Suppose \(x = \sum _i x_i\) is mapped to 0 by f where each \(x_i \in \mathcal {A}_i\). We need to show \(f(x_i)\) is zero as well. \(f(x_i) = \left( f_{\oplus }\left( \bigoplus _i x_i \right) \right) _i = \texttt {decomp}(f(x))_i = 0\). \(\square \) Remark 1 Similarly, we define the notion of a graded ring isomorphism and a grade algebra homomorphism. 2.2 Lemmas About Homogeneous Elements The following lemma is used repetitively in the formalisation of multi-graded Proj construction. Lemma 3 Let A be a commutative \(\iota \)-graded ring where \(\iota \) is an abelian group. Suppose a and c are homogeneous elements of A such that \(a \mid c\). Then there exists a homogeneous element b such that \(ab = c\). Proof Let \(b = \dots + b_0 + b_1 + \dots \) be an arbitrary element of A such that \(ab = c\). Suppose a has degree i and c has degree j, by looking at the j-th coordinate of the equaltion \(ab = c\), we see that \(a b_{j - i} = c\) as well. \(\square \) 3 Relevance In this section, we assume that A is a commutative \(\iota \)-graded rings where \(\iota \) is an abelian group. We develop the notion a relevant homogeneous submonoid of A. 3.1 Homogeneous Submonoid A homogeneous submonoid of A is a submonoid such that every element is homogeneous. Equivalently, it is a submonoid generated by homogeneous elements. Since this equivalent characterization is more convenient for our purposes, we adopt the following definition. Definition 6 (Homogeneous Submonoid) A homogeneous submonoid of a graded ring A is a submonoid S of A such that S can be generated by homogeneous elements. By definition, if a set s only contains homogeneous elements, then the submonoid \(\left\langle s \right\rangle \) generated by s is a homogeneous submonoid. The submonoid \(\{1\}\) is a homogeneous submonoid of any graded ring A. Lemma 4 Let S be a homogeneous submonoid of A and \(\Phi : A \rightarrow B\) be a graded ring homomorphism, then \(\Phi _{\star }S:= \left\langle \Phi (S) \right\rangle \) is a homogeneous submonoid of B. Proof Suppose S is generated by s where s is a set of homogeneous elements, \(\left\langle \Phi (S) \right\rangle \) is generated by \(\Phi (s)\). \(\square \) Lemma 5 Let S be a homogeneous submonoid, the set \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) of homogeneous divisors of elements in S is another homogeneous submonoid. Proof Obviously, \(1\in \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) and \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) contains only homogeneous elements. Let x and y be two homogeneous elements in \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\), suppose x divides \(a_{x} \in S\) and y divides \(a_{y} \in S\). Then xy is also homogeneous and divides \(a_{x}a_{y} \in S\). \(\square \) Construction 1 The collection of all homogeneous submonoids of a graded ring A forms a commutative monoid. The multiplication is defined by the pointwise multiplication and the identity is the trivial homogeneous submonoid \(\{1\}\). The product of two homogeneous submonoids S and T is still homogeneous because ST is generated by the set \(S \cup T\) of homogeneous elements. We note that the following useful equalities: - For any homogeneous submonoid S, \(S \cdot S = S\). - If s and t are two sets of homogeneous elements, the closure of \(s\cup t\) is equal to \(\left\langle s \right\rangle \left\langle t \right\rangle \). - For any homogeneous submonoids S and T of A, if \(\Phi : A \rightarrow B\) is a graded ring homomorphism, \(\Phi _{\star }\left( ST \right) = \Phi _{\star }(S)\Phi _{\star }(T)\). 3.2 Relevant Homogeneous Submonoid Definition 7 Let S be a homogeneous submonoid, we use \(\deg (S)\) to denote the additive submonoid \(\iota \) containing the degrees of elements in S, that is, \(i \in \deg (S)\) if and only if there exists an \(x\in S\) such that x is homogeneous of degree i. We denote \(\iota [S]\) to be the subgroup of \(\iota \) generated by \(\deg (S)\). Remark 2 If 0 is in S, \(\deg S\) is equal to \(\iota \). This is not problematic, because if S contains 0, in the context of localizations, \(A_{S}\) is the trivial ring. Remark 3 As a set, \(\iota [S]\) is the set of elements of the form \(i - j\) where i and j are in \(\deg (S)\). Definition 8 (Relevance) - A homogeneous submonoid S is relevant if for all \(i \in \iota \), there exists a positive natural number n such that \(n\cdot i\) is in \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). - A set of homogeneous elements \(\left\{ a_i | i \in I \right\} \) is relevant if the homogeneous submonoid generated by \(\left\{ a_i | i \in I \right\} \) is relevant. - A homogeneous element a is relevant if the set \(\{a \}\) is relevant. - The homogeneous ideal of A generated by the set of relevant homogeneous elements of A is denoted as \(A_{\dagger }\). Remark 4 A more succinct way to say that a homogeneous submonoid S is relevant is that the quotient is a torsion abelian group. Hence, when \(\iota \) is finitely generated, S is relevant if and only if is finite if and only if \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \) is subgroup of finite index. We begin with several lemmas about relevant homogeneous submonoids. Lemma 6 relevant-mul If S and T are two relevant homogeneous submonoids, then ST is also relevant. Proof Let \(i \in \iota \), since S is relevant, there exists a positive natural number m such that \(m\cdot i\) is in \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). Since T is relevant, there exists a positive natural number n such that \(n\cdot i\) is in \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}T\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). One can show that \((m + n)\cdot i\) is in \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}ST\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \): since \(m\cdot i \in \iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \), we can find a and b in \(\deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \) such that \(m\cdot i = a - b\). Similarly, we can find c and d in \(\deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}T\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \) such that \(n\cdot i = c - d\). Then \((a + c) - (b + d) = (m + n)\cdot i\) is in \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}ST\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). \(\square \) Lemma 7 Let \(f: A\rightarrow B\) be a graded ring homomorphism and S be a relevant homogeneous submonoid of A, \(f_\star S = \left\langle f(S) \right\rangle \) is a relevant homogeneous submonoid of B. Proof It is sufficient show that \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \le \iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}f_\star S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \); or equivalently \(\deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \le \deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}f_\star S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \). Let \(i \in \deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \). There exists an \(x \in \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) such that x is homogeneous of degree i. Hence, there exists an \(y \in S\) such that x divides y. Since f is graded, f(x) also has degree i and \(f(y) \in f_\star S\) is homogeneous and f(x) divides f(y). Therefore, f(x) is in \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}f_\star S\hspace{-0.88882pt}}\hspace{0.88882pt}\) and i is in \(\deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}f_\star S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \). \(\square \) Lemma 8 If \(T \le S\) are two relevant homogeneous submonoids where T is relevant, then S is also relevant. Proof Since T is relevant, is a torsion abelian group. Since \(T \le S\), we have a surjection . Hence, is also a torsion abelian group. \(\square \) Theorem 9 Suppose \(\iota \) is a finitely generated abelian group. Then \(a \in A\) is a relevant homogeneous element if and only if there exists elements \(x_1, \dots , x_n\) in A where each \(x_i\) is homogeneous of degree \(d_i\) such that the subgroup generated by \(\left\{ d_i \right\} \) is of finite index in \(\iota \) and there exists a natural number k such that \(a^k = \prod _{i=1}^{n}x_i\). Proof For the forward implication, suppose a is a relevant homogeneous element, we see that \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle a \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \) is a subgroup of finite index in \(\iota \). Therefore, \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle a \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \) is finitely generated. Let \(\left\{ i_1,\dots ,i_N \right\} \subseteq \iota \) be a generating set of \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle a \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). For each \(i_k \in \left\{ i_1, \dots , i_n \right\} \), we see that there exists an \(x_k \in A\) homogeneous of degree \(i_k\) such that \(x_l\) divides \(a^n_k\) for some \(n_j\). We can take \(K = \sum _{k=1}^N n_k\), and we see that \(\prod _{k=1}^{N}x_k\) divides \(a^K\). Hence, by Lemma 3, there exists a homogeneous element b of degree j such that \(\left( \prod _{k=1}^{N} x_k\right) b = a^K\). All there remains is to show that the subgroup generated by \(\left\{ i_1, \dots , i_N, j \right\} \) is of finite index in \(\iota \). Since \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle a \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] = \left\langle i_1, \dots , i_N \right\rangle \) is a subgroup of finite index in \(\iota \), and \(\left\langle i_1, \dots , i_N, j \right\rangle \) is at least as large as, if not larger than, \(\left\langle i_1, \dots , i_N \right\rangle \), it is also a subgroup of finite index in \(\iota \). Conversely, suppose \(a^k = \prod _{i=1}^n x_i\) such that \(x_i\) is homogeneous of degree \(d_i\) and the subgroup generated by \(\left\{ d_i \right\} \) is of finite index in \(\iota \). It is sufficient to show that \(\left\langle d_1,\dots , d_n \right\rangle \) is smaller than or equal to \(\iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle a \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). This is true because for any i, \(d_i\) is in \(\deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle a \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right) \): due to the factorization \(\prod _i x_i = a^k\), \(x_i\) has degree \(d_i\) and is a homogeneous divisor of \(a^k \in \left\langle a \right\rangle \). \(\square \) Corollary 10 If a and b are two relevant homogeneous elements, ab is also a relevant homogeneous element. Corollary 11 If \(f: A \rightarrow B\) is a graded ring homomorphism and a is a relevant homogeneous element in A, f(a) is a relevant homogeneous element in B. Corollary 12 Let \(f: A \rightarrow B\) be a graded ring homomorphism, \(f_{\star }\left( A_{\dagger } \right) \) is smaller than or equal to \(B_{\dagger }\). Corollary 13 Let \(f: A \rightarrow B\) be a surjective graded ring homomorphism, the radical ideals of \(f_{\star }\left( A_{\dagger } \right) \) and \(B_{\dagger }\) are equal: Proof By Corollary 12, we have \(f_{\star }\left( A_{\dagger } \right) \subseteq B_{\dagger }\), hence we only need to show \(\sqrt{B_{\dagger }} \le \sqrt{f_{\star }\left( A_{\dagger } \right) }\). Equivalently, we need to show that for any relevant homogeneous element \(b \in B\), b is in \(\sqrt{f_{\star }\left( A_{\dagger } \right) }\). Since b is relevant, by Theorem 9, there exists a positive natural number k such that \(b^k = \prod _{i=1}^{n} x_i\) where each \(x_i\) is homogeneous of degree \(d_i\) and \(\left\langle d_i \right\rangle \) is a subgroup of finite index. Since f is surjective, we can write b as f(a) for some \(a \in A\) and \(f(a_i) = x_i\) for each \(i = 1,\dots , n\). In order to show that \(b = f(a)\) is in \(\sqrt{f_{\star }\left( A_{\dagger } \right) }\), we show that \(f(a)^k = f\left( \prod _i a_i\right) \) is in \(f_{\star }\left( A_{\dagger } \right) \). This is true, because \(\prod _i a_i\) is relevant by Theorem 9. \(\square \) 4 Homogeneous Localization In this section, let R be a commutative ring and A a commutative graded R-algebra. Let x be a submonoid of A. In general, unless x contains only homogeneous elements, the localized ring \(A_x\) is not graded.Footnote 1 However, we can still investigate set \(A_{(x)}\) of elements of degree zero in the localized ring. Construction 2 Consider the type of triples of (i, a, b) where a and b are homogeneous elements of the degree i and b is in x, we have a function defined by \((i, a, b) \mapsto =\frac{a}{b}\). We define the homogeneous localization \(A_{(x)}\) to be the quotient where . The function \(\textsf {frac}\) descends to an embedding . We choose not to define \({A}_{\left( x\right) }\) as a subring of the localized ring \(A_x\). In the current approach, for any fraction \(f \in {A}_{\left( x\right) }\), we can use the tactic to obtain a pair (i, a, b) such that \(f = [(i, a,b)]\). Hence, the numerator, the denominator, and the degree of them are easily available and more organized. Theorem 14 Let \(\mathfrak {p}\) be a prime ideal of A, the homogeneous localization \({A}_{\left( \mathfrak {p}\right) }\) is a local ring. Proof Since \(A_{\mathfrak {p}}\) is a local ring, it is sufficient to prove that for any fraction \(f \in {A}_{\left( \mathfrak {p}\right) }\), f is a unit in \(A_{\mathfrak {p}}\) if and only if f is a unit in \({A}_{\left( \mathfrak {p}\right) }\) as well. This is because, we write \(f=[(i, a, b)]\), the inverse of f is [i, b, a]. \(\square \) Homogeneous localization of a graded module can be defined similarly. Lemma 15 Let \(\phi : A \rightarrow B\) be a graded ring homorphism, suppose P is a submonoid of A and Q is a submonoid of B are submonoids such that \(\phi ^{-1}(Q) \le P\). Then \(\phi \) induces a ring homomorphism \({A}_{\left( P\right) } \rightarrow {B}_{\left( Q\right) }\). [14, HomogeneousLocalization.map] Proof \(\phi \) induces a map \(A_{P} \rightarrow A_{Q}\); since \(\phi \) preserves degrees, we can restrict the map to the degree zero part of the localized rings. \(\square \) Remark 5 Since the homogeneous localization is not implemented as a subring of the localized ring, we can not restrict \(\phi \) to the degree zero part; we have to construct the map by hand: Luckily, with structure, the numerator and the denominator are easily accessible. 5 Localization of Graded Ring and Modules In section 4, we see that not every localized ring is graded. If we restrict our attention to homogeneous submonoids, we can define the grading of the localized rings and modules. In this section, we assume the indexing set for the grading of A is an additive group. Let S be a homogeneous submonoid of A, we construct the quotient grading for the localized ring \(A_S\). We will adopt a similar approach to the construction of homogeneous localization in section 4. Construction 3 Let denote the set of qudraples \((a, b, d_a, d_b)\) where \(d_a\) and \(d_b\) are in \(\iota \) such that \(d_a - d_b = i\), \(a \in A\) is homogeneous of degree \(d_a\) and \(b \in S\) is homogeneous of degree \(d_b\). For each \(i \in \iota \), we give \(P_i\) a group structure by: - The zero element is (0, 1, 0, 0). - The result of adding \((a, b, d_a, d_b)\) and \((a', b', d_{a'}, d_{b'})\) is defined as \((ab' + a'b, bb', d_a + d_{a'}, d_b + d_{b'})\). - The negation of \((a, b, d_a, d_b)\) is defined as \((-a, b, d_a, d_b)\). Hence, we have . Consider the quotient formed by where . We take . To construct the decomposition ring homomorphism \(A_{S} \rightarrow \bigoplus _i A_{S, i}\), we first construct a ring homomorphism \(A \rightarrow \bigoplus _{i} A_{S, i}\) and check that every element in S is sent to an invertible element. The ring homomorphism is defined as the following: To summarize, an element \(x \in A_{S}\) has degree i if and only if there exists \(m,n\in \iota \) such that \(m - n = \iota \) and \(x = \frac{a}{b}\) for some \(a \in A\) with degree m and \(b \in S\) with degree n. [9, file location: Grading/Localization.lean] If M is a graded A-module also with \(\iota \) as the indexing set for the grading, we can construct the localized module \(M_{S}\) as a graded \(A_{S}\)-module in the same way as Construction 3. As graded rings, we can always enlarge the submonoid S to \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) and have the rings \(A_S\) isomorphic to \(A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}}\): Theorem 16 The localized rings \(A_{S}\) and \(A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}}\) are isomorphic as graded rings. Proof Since \(S \le \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\), we have a ring homomorphism \(\small {\texttt {localizationToLocalizationBar}}: A_{S} \rightarrow A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}}\). Let \(s \in \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\), there exists an \(y \in S\) such that s divides y. In order to descend the map \(A \rightarrow A_S\) to a map \(A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}} \rightarrow A_S\), we need to check each element \(s \in \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) is invertible in \(A_{S}\). By Theorem 3, there exists a homogeneous element z such that \(sz = y\). Therefore, the fraction \(\frac{s}{1} \in A_{S}\) has an inverse \(\frac{z}{y} \in A_{S}\). Hence, we have a well-defined ring homomorphism \(\small {\texttt {localizationBarToLocalization}}: A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}} \rightarrow A_{S}\). The two ring homomorphisms are inverses of each other. We show that the ring isomorphism \(A_{S} \rightarrow A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}}\) is a graded: suppose \(x \in A_{S}\) is homogeneous of degree i, by construction 3, x can be written as \(\frac{a}{b}\) with a homogeneous of degree m and \(b \in S\) homogeneous of degree n such that \(m - n = i\). Thus image of x in \(A_{S}\) is still \(\frac{a}{b}\) where b is seen as an element of \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\); hence x still has degree i in \(A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}}\). Similarly, if \(x \in A_{\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}}\) is homogeneous of degree i, then it can be written as \(\frac{a}{b}\) where a is homogeneous of degree m and \(b \in \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) is homogeneous of degree n such that \(m - n = i\). Suppose b divides \(y \in S\), then there exists a homogeneous element z such that \(bz = y\). Therefore, the image of x in \(A_{S}\) is \(\frac{a z}{b z}\), which is still homogeneous of degree i. \(\square \) 6 Tensor Product of Graded Rings In this section, we assume A and B are graded commutative R-algebras where A is graded by \(\iota _{A}\) and B is graded by \(\iota _B\). We will realize \(A \otimes _R B\) as an \(\iota _A \times \iota _B\)-graded R-algebra. Construction 4 (Graded Tensor Product) For any \(i \in \iota _A\) and \(j \in \iota _B\), the (i, j)-th graded piece of the tensor product \(A \otimes _R B\) is the \(A_i \otimes _R B_j\). Since type theoretically, we need \(A_i \otimes _R B_j\) as a submodule of \(A \otimes _R B\), we use the range of the linear map \(A_i \otimes _R B_j \rightarrow A \otimes _R B\). We can check that 1 has degree (0, 0) and that the product of an element of degree (i, j) and an element of degree \((i', j')\) has degree \((i + i', j + j')\). To show that is indeed a grading, we construct a linear map where the second map is defined as [9, file location: Grading/TensorProduct.lean] Theorem 17 (Tensor product of relevant element) If x is a relevant homogeneous element in A and y is a relevant homogeneous element in B, \(x \otimes y\) is a relevant homogeneous element in \(A \otimes _R B\). Proof Let us denote M to be the subgroup \(\iota _{A}\left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle x \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \) of \(\iota _A\), N to be the subgroup \(\iota _{B}\left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle y \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \) of \(\iota _B\) and X to be the subgroup \(\left( \iota _A \times \iota _{B} \right) \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}\left\langle x\otimes y \right\rangle \hspace{-0.88882pt}}\hspace{0.88882pt}\right] \). We will show that is torsion. Let be the surjective group homomorphism induced by the two group homomorphisms and . Hence, we only need to show that is torsion. Since x is relevant, is torsion, and since y is relevant, is torsion; consequently, their product is torsion. \(\square \) Theorem 18 Suppose \(\iota _A\) and \(\iota _{B}\) are both finitely generated abelian groups. For any relevant homogeneous element \(x \in A \otimes _R B\), there exists \(s^{A}_1, \dots , s^{A}_n\) in A and \(s^{B}_1, \dots , s^{B}_n\) in B such that each \(s^{A}_i\) and \(s^{B}_j\) are relevant homogeneous elements and for some natural number k, Proof Since x is relevant, by Theorem 9, we can find elements \(y_1, \dots , y_N\) in \(A \otimes _R B\) such that each \(y_i\) has degree \(\left( d^{A}_i, d^{B}_i\right) \in \iota _{A} \times \iota _{B}\) where \(\left\langle \left( d^{A}_i, d^{B}_i\right) \big | i = 1,\dots ,N \right\rangle \) is a subgroup of finite index in \(\iota _{A} \times \iota _{B}\) and \(x^k = \prod _i y_i\). Hence, \(\left\langle d^{A}_{i} \big | i = 1,\dots , N \right\rangle \) and \(\left\langle d^{B}_{i} \big | i = 1,\dots , N \right\rangle \) are subgroups of finite index in \(\iota _A\) and \(\iota _B\) respectively. Since each \(y_i\) has degree \(\left( d^{A}_i, d^{B}_i\right) \), we can write each \(y_i\) as \(\sum _{j \in J_i} s^{A}_{j} \otimes s^{B}_j\) where \(J_i\) is a finite set of indices and for any \(j \in J_i\), \(s^{A}_{j}\) and \(s^{B}_{j}\) as degree \(d^{A}_i\) and \(d^{B}_i\) respective. Hence, By Theorem 9 again, all the products \(\prod _{i = 1}^N s^{A}_{j_i}\) and \(\prod _{i = 1}^N s^{B}_{j_i}\) are relevant homogeneous elements. Thus, the theorem holds. \(\square \) Theorem 19 The range of the linear map \(A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B\) is an ideal of \(A \otimes _R B\), and we have Proof We first check that the range of the linear map \(A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B\) is an ideal of \(A \otimes _R B\). Suppose \(a \otimes b \in A_{\dagger } \otimes _R B_{\dagger }\) and \(a' \otimes b' \in A \otimes _R B\) is in \({{\,\textrm{im}\,}}\left( A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B \right) \). Since \(a \in A_{\dagger }\), \(aa'\) is in \(A_{\dagger }\), and since \(b \in B_{\dagger }\), \(bb'\) is in \(B_{\dagger }\). Therefore, \((a' \otimes b')(a \otimes b)\) is in the range of the linear map \(A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B\). We then demonstrate \(\sqrt{\left( A\otimes _R B \right) _{\dagger }} \le \sqrt{{{\,\textrm{im}\,}}\left( A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B \right) }\). It is sufficient to show that every relevant homogeneous element \(x \in A \otimes _R B\) is in the range. By Theorem 18, we can find relevant homogeneous elements \(s^{A}_1, \dots , s^{A}_n\) in A and \(s^{B}_1, \dots , s^{B}_n\) in B such that \(x^k = \sum s_{i}^{A} \otimes s_{i}^{B}\) for some natural number k. Since each \(s^{A}_{i}\) is in \(A_{\dagger }\) and each \(s^{B}_{i}\) is in \(B_{\dagger }\), we have \(\sum s^{A}_{i} \otimes s^{B}_{i}\) is in \({{\,\textrm{im}\,}}\left( A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B \right) \) and consequently, x is the radical. For the other direction, we demonstrate \({{\,\textrm{im}\,}}\left( A_{\dagger } \otimes _R B_{\dagger } \rightarrow A \otimes _R B \right) \le \left( A\otimes _R B \right) _{\dagger }\). Since \(\left( A\otimes _R B \right) _{\dagger }\) is an R-submodule of \(A \otimes _R B\) as well, it is sufficient to show that for every element \(a \otimes b \in A_{\dagger } \otimes _R B_{\dagger }\), \(a \otimes b\) is in \(\left( A\otimes _R B \right) _{\dagger }\). This is precisely Theorem 17. \(\square \) 7 Potions In this section, we assume A is a commutative \(R_0\)-algebra that is graded by an abelian group \(\iota \). We use the same terminology found in [12]. Definition 9 For a homogeneous submonoid \(S \subseteq A\), the homogeneous localization \({A}_{\left( S\right) }\) is called the potion of A with respect to S. Since we will be working with multiple submonoids at once, the notation \({A}_{\left( S\right) }\) can be confusing — for example \({A}_{\left( (S_1 S_2)S_3\right) }\) and \({A}_{\left( S_1(S_2S_3)\right) }\) could be potentially misread to mean (normal) localization at \((S_1S_2)S_3\) with a redundant bracket in the notation. Therefore, we use \({{\,\mathrm{\vartheta }\,}}(S)\) to denote the ring \({A}_{\left( S\right) }\). Type theoretically, since S is a homogeneous submonoid of A, the absence of A in the notation \({{\,\mathrm{\vartheta }\,}}(S)\) should cause no issue. If the ring of which S is a submonoid could not be inferred from the context, we will use \({{\,\mathrm{\vartheta }\,}}_A(S)\) instead. We first collect some useful morphisms between potions defined by Lemma 15 - If \(\phi : A \rightarrow B\) is a graded ring homomorphism between two \(\iota \)-graded rings, there is a ring homomorphism \(\small {\texttt {potionToMap}}: {{\,\mathrm{\vartheta }\,}}(S) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( \phi _{\star } S\right) \) induced by \(\phi \). - If \(S = T\) are two homogeneous submonoids of A, we have a ring isomorphism \(\small {\texttt {potionEquiv}}: {{\,\mathrm{\vartheta }\,}}(S) \cong {{\,\mathrm{\vartheta }\,}}(T)\) induced by the \(\textsf {id}_A\). In particular, since \(S S = S\), we have a ring isomorphism \({{\,\mathrm{\vartheta }\,}}(S)\cong {{\,\mathrm{\vartheta }\,}}(SS)\). - For any two homogeneous submonoids S and T, there is a ring homomorphism \(\small {\texttt {potionToMul}}:{{\,\mathrm{\vartheta }\,}}(S) \rightarrow {{\,\mathrm{\vartheta }\,}}(ST)\) induced by \(\textsf {id}_A\) and the following commutative square: With the ring homomorphism \(\small {\texttt {potionToMul}}\), we view \({{\,\mathrm{\vartheta }\,}}(ST)\) as a \({{\,\mathrm{\vartheta }\,}}(S)\)-algebra. - There is a ring homomorphism \(\small {\texttt {toBarPotion}}: {{\,\mathrm{\vartheta }\,}}(S) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \) induced by \(\textsf {id}_A\). Since \(\small {\texttt {toBarPotion}}\) is bijective, we have a ring isomorphism \(\small {\texttt {equivBarPotion}}: {{\,\mathrm{\vartheta }\,}}(S) \cong {{\,\mathrm{\vartheta }\,}}\left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \). For any homogeneous elements \(a, b\in A\) of degree i and \(c \in A\) of degree j such that \(bc \in S\), the image of the homogeneous fraction \(\frac{m}{n} \in {{\,\mathrm{\vartheta }\,}}\left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \) under \(\small {\texttt {equivBarPotion}}^{-1}\) is the homogeneous fraction \(\frac{az}{bz} \in {{\,\mathrm{\vartheta }\,}}(S)\). Definition 10 Suppose S and T be homogeneous submonoids of A. A potion generator of T over S is the following data: - ; - ; - ; For each i, the fraction \(\frac{t_i^{n_i}s'_i}{s_i}\) is in \({{\,\mathrm{\vartheta }\,}}\left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \). We denote \(\textsf {s}(T')\) to . When the indexing set I is finite, we say that \(T'\) is a finite potion generator of T over S. Remark 6 For any three R, S, T homogeneous submonoids of A, if \(R' = \left( I_R, t_R, s_R, {s'}_R, i_R,\right. \left. {i'}_R, n_R \right) \) is a potion generator of R over S and \(T' = \left( I_T, t_T, s_T, {s'}_T, i_T, {i'}_T, n_T \right) \) is a potion generator of T over S, we have a potion generator of RT over S given by the disjoint union of the two potion generators: It is useful to note that \(\textsf {s}\left( R'\oplus T' \right) \) is equal to \(\textsf {s}(R')\textsf {s}(T')\). The motivation for the definition of potion generator is the following theorem. Theorem 20 Let \(T' = \left( I, t, s, s', i, i', n \right) \) be a potion generator of T over S. We have a \({{\,\mathrm{\vartheta }\,}}(S)\)-algebra isomorphism between \({{\,\mathrm{\vartheta }\,}}( ST )\) and \({{\,\mathrm{\vartheta }\,}}(S)_{\textsf {s}(T')}\). Proof In order to descend the ring homomorphism \(\small {\texttt {potionToMul}}: {{\,\mathrm{\vartheta }\,}}(S) \rightarrow {{\,\mathrm{\vartheta }\,}}(ST)\) to a ring homomorphism \({{\,\mathrm{\vartheta }\,}}(S)_{\textsf {s}(T')} \rightarrow {{\,\mathrm{\vartheta }\,}}(ST)\), we need to show that the image of \(\small {\texttt {equivBarPotion}}^{-1}\left( \frac{t_i^{n_i}s'_i}{s_i} \right) \) is sent to a unit in \({{\,\mathrm{\vartheta }\,}}(ST)\). Since \(s_i\) and \(s'_i\) are in \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\), we can find y and \(y'\) in S such that \(s_i\mid y\) and \(s_i' \mid y'\). Hence, by Theorem 3, there exists two homogeneous elements z and \(z'\) such that \(y = s_i z\) and \(y' = s_i' z'\). Therefore, when seen as a fraction in \({{\,\mathrm{\vartheta }\,}}(S)\), \(\frac{t_i^{n_i}s'_i}{s_i}\) is equal to \(\frac{t_i^{n_i}s'_iz}{s_i z}\) and, its image under \(\small {\texttt {potionToMul}}\) is \(\frac{t_i^{n_i}s'_iz}{s_i z}\) with inverse \(\frac{s_i z'}{t_i^{n_i}s'_iz'}\). Therefore, we have a well-defined ring homomorphism \(\phi : {{\,\mathrm{\vartheta }\,}}(S)_{\textsf {s}(T')} \rightarrow {{\,\mathrm{\vartheta }\,}}(ST)\). An element in \({{\,\mathrm{\vartheta }\,}}(S)_{\textsf {s}(T')}\) has the form where in the denominator, the indices i runs through a finite subset of I and \(k_i\) are positive natural numbers. With this notation, we see that the image under \(\phi \) is equal to \(\frac{a}{s}\cdot \prod _i \left( \frac{s_i}{t_i^{n_i}s'_i} \right) ^{k_i}\). Since, \(\prod _i \left( \frac{s_i}{t_i^{n_i}s'_i} \right) ^{k_i}\) is invertible in \({{\,\mathrm{\vartheta }\,}}(ST)\), the image is zero if and only the numerator \(\frac{a}{s} \in {{\,\mathrm{\vartheta }\,}}(ST)\) is zero. We first show that \(\phi \) is injective. Suppose an element is sent to zero under \(\phi \). We want to show that is equal to zero. It is sufficient to find an element x in \(\textsf {s}(T')\) such that \(x \cdot \frac{a}{s}\) is zero as elements of \({{\,\mathrm{\vartheta }\,}}(S)\). Since is zero, we see that \(\frac{a}{s}\) is equal to zero in \({{\,\mathrm{\vartheta }\,}}(ST)\), therefore, there exists an element \(\mathfrak {s} \in S\) and \(\mathfrak {t} \in T\) such that \(\mathfrak {s} \mathfrak {t} a = 0\). Since \(\left\{ t_i | i \in I \right\} \) generates T, we can write \(\mathfrak {t}\) as \(\prod _i {t_i}^{k_i}\). Set \(x = \prod _i \small {\texttt {equivBarPotion}}^{-1}\left( \frac{\mathfrak {s}t_i^{n_i}s'_i}{\mathfrak {s}s_i} \right) ^{k_i}\), we see that \(x\cdot \frac{a}{s}\) is equal to zero. Then, we show that \(\phi \) is surjective. Suppose \(\frac{a}{\mathfrak {s}\mathfrak {t}}\) is an element in \({{\,\mathrm{\vartheta }\,}}(ST)\) and we write \(\mathfrak {t}\) as \(\prod _i t_i^{k_i}\). We have the following equality in \({{\,\mathrm{\vartheta }\,}}(ST)\): Hence, \(\frac{a}{\mathfrak {s}\mathfrak {t}}\) is in the image of \(\phi \). Thus, \(\phi \) is a ring isomorphism between \({{\,\mathrm{\vartheta }\,}}(S)_{\textsf {s}(T')}\) and \({{\,\mathrm{\vartheta }\,}}(ST)\). One can check that \(\phi \) is a \({{\,\mathrm{\vartheta }\,}}(S)\)-algebra isomorphism as well. \(\square \) Corollary 21 Suppose there exists a finite potion generator \(T' \) of T over S. The morphism of scheme \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(ST) \rightarrow {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(S)\) is an open immersion. Proof We have the following commutative triangle: Therefore, the morphism \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(ST) \rightarrow {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(S)\) factors as Hence, it is sufficient to show that \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(S)_{\textsf {s}(T')} \rightarrow {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(S) \) is an open immersion. This is true because \(\textsf {s}(T')\) is generated by a finite set. \(\square \) Theorem 22 If S is relevant and T is finitely generated as a submonoid of A, there exists a finite potion generator \(T'\) of T over S. Proof We claim that for every homogeneous element \(t \in A\), there exists a positive natural number n, and two homogeneous elements \(s, s' \in \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) of degree i and \(i'\) respectively such that \(t^n \in A_{i - i'}\): The claim is true: let t be a homogeneous element of degree m. Since S is relevant, there exists a positive natural number n such that \(t^n \in \iota \left[ \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right] \), that is, there exists i and \(i'\) in \(\iota \) such that \(n\cdot m = i - i'\) and \(i, i'\) are elements of \(\deg \left( \hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\right) \). Hence, there exists s and \(s'\) in \(\hspace{0.88882pt}\overline{\hspace{-0.88882pt}S\hspace{-0.88882pt}}\hspace{0.88882pt}\) with degree i and \(i'\) respectively. Since T is finitely generated, we can choose an arbitrary finite set \(T' \subseteq T\) which generates T as a submonoid. Hence, we can define functions \(n: T' \rightarrow \mathbb {N}_{>0}\), \(s, s': T' \rightarrow A\), and \(i, i': T' \rightarrow \iota \) such that for each \(t \in T'\), s(t) and \(s'(t)\) are homogeneous elements of degree i(t) and \(i'(t)\) respectively, and \(t^{n(t)}\) is homogeneous of degree \(i(t) - i'(t)\). These are exactly the data we need to define a finite potion generator of T over S. \(\square \) Corollary 23 If S is relevant and T is finitely generated as a submonoid of A, then \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(ST) \rightarrow {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(S)\) is an open immersion. 8 Gluing Potions and Defining Proj Now, we restrict our attention to relevant and finitely generated homogeneous submonoids; we call such submonoids good potion ingredients. We immediately notice that product of good potion ingredients is another good potion ingredient, hence the set of good potion ingredients is a commutative semigroup. If \(\phi : A \rightarrow B\) is a graded ring homomorphism, and S is a good potion ingredient of A, then \(\phi _{\star } S\) is a good potion ingredient of B. For any three good potion ingredients R, S, T, we view \({{\,\mathrm{\vartheta }\,}}(RST)\) as a \({{\,\mathrm{\vartheta }\,}}(S)\)-algebra via the ring homomorphism \({{\,\mathrm{\vartheta }\,}}(S) \rightarrow {{\,\mathrm{\vartheta }\,}}(S(RT)) \rightarrow {{\,\mathrm{\vartheta }\,}}(RST)\). Let \(R'\) be a potion generator of R over S and \(T'\) be a potion generator of T over S. Construction 5 We have a \({{\,\mathrm{\vartheta }\,}}(S)\)-algebra isomorphism \(e: {{\,\mathrm{\vartheta }\,}}(ST) \otimes _R {{\,\mathrm{\vartheta }\,}}(SR) \cong {{\,\mathrm{\vartheta }\,}}(RST)\) by composing the isomorphisms in Table 1. We notice that for any \(x \in {{\,\mathrm{\vartheta }\,}}(ST)\), \(e(x\otimes 1)\) is equal to the image of x under \({{\,\mathrm{\vartheta }\,}}(ST) \rightarrow {{\,\mathrm{\vartheta }\,}}(STR) \rightarrow {{\,\mathrm{\vartheta }\,}}(RST)\) and for any \(x \in {{\,\mathrm{\vartheta }\,}}(SR)\), \(e(1\otimes x)\) is equal to the image of x under \({{\,\mathrm{\vartheta }\,}}(SR)\rightarrow {{\,\mathrm{\vartheta }\,}}(SRT) \rightarrow {{\,\mathrm{\vartheta }\,}}(RST)\). With the same construction, we have an isomorphism \({{\,\mathrm{\vartheta }\,}}(RS) \otimes _{{{\,\mathrm{\vartheta }\,}}(R)} {{\,\mathrm{\vartheta }\,}}(RT) \cong {{\,\mathrm{\vartheta }\,}}(TRS) \cong {{\,\mathrm{\vartheta }\,}}(RST)\). Hence, we have an isomorphismFootnote 2\(t'_{RST}: {{\,\mathrm{\vartheta }\,}}(ST)\otimes _{{{\,\mathrm{\vartheta }\,}}(S)}{{\,\mathrm{\vartheta }\,}}(SR) \cong {{\,\mathrm{\vartheta }\,}}(RS) \otimes _{{{\,\mathrm{\vartheta }\,}}(R)} {{\,\mathrm{\vartheta }\,}}(RT)\). [9, file location: Potions/GoodPotionIngredient.lean] Corollary 24 For any three good potion ingredients R, S, T, \(t'_{TRS} \circ t'_{STR}\circ t'_{RST}\) is the identity isomorphism. Corollary 25 For any three good potion ingredients R, S, T, the following diagram commutes: Now we are ready to proceed with \({{\,\textrm{Proj}\,}}\) construction. Let \(\mathscr {F} = \left\{ S_i \big | i \in \tau \right\} \) be a family of good potion ingredients of A indexed by \(\tau \). We aim to glue the family of schemes together \(\left\{ {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}\left( S_i \right) \big | i \in \tau \right\} \). Construction 6 To proceed with the gluing, we need the following data: - an indexing type J; - a scheme \({U_i}\) for each \({i} \in J\); - a scheme \({V_{ij}}\) for each pair \({(i,j)\in J\times J}\) representing the intersection of \({U_i}\) and \({U_j}\); - an open immersion of schemes \(f_{ij}: V_{ij} \rightarrow U_i\) for each pair \({(i,j)\in J\times J}\) such that \(f_{ii}\) is an isomorphism; - a morphism of schemes \(t'_{ijk}: V_{ij} \times _{U_i} V_{ik} \rightarrow V_{jk} \times _{U_j} V_{ji}\) such that for each triple \({(i,j,k)\in J\times J\times J}\), the composition is the identity map; - a transition map \(t_{ij}: V_{ij} \rightarrow V_{ji}\) for each pair \({(i,j)\in J\times J}\) such that \(t_{ii}\) is the identity map, and for each triple \({(i,j,k)\in J\times J\times J}\), the following diagram commutes: In our case, we will take \(J = \tau \), \(U_i = {{\,\textrm{Spec}\,}}\left( {{\,\mathrm{\vartheta }\,}}(S_i)\right) \), \(V_{ij} = {{\,\textrm{Spec}\,}}\left( {{\,\mathrm{\vartheta }\,}}(S_i S_j)\right) \), and \(f_{ij} = {{\,\textrm{Spec}\,}}\left( {{\,\mathrm{\vartheta }\,}}(S_i) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( S_i S_j \right) \right) \), \(t_{ij} = {{\,\textrm{Spec}\,}}\left( {{\,\mathrm{\vartheta }\,}}\left( S_i S_j \right) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( S_j S_i \right) \right) \) and \(t'_{ijk}\) to be the composition where \(t'_{S_iS_jS_k}\) is defined in Construction 5. Since for any homogeneous submonoid S, \(SS = S\), we see that \(f_{ii}\) is the identity morphism. We have already shown that \(f_{ij}\) are open immersions in Theorem 21. Since \(t_{ii}\) is defined as \({{\,\textrm{Spec}\,}}\left( {{\,\mathrm{\vartheta }\,}}\left( S_i S_i\right) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( S_i S_i \right) \right) \), it is certainly the identity morphism. Now, we verify eq. (1) and eq. (2): modulo the isomorphisms of the form \({{\,\textrm{Spec}\,}}A \times _{{{\,\textrm{Spec}\,}}B} {{\,\textrm{Spec}\,}}C \cong {{\,\textrm{Spec}\,}}\left( A\otimes _B C \right) \), Eqs. (1) and (2) are \({{\,\textrm{Spec}\,}}\) applied to Theorems 24 and 25 respectively. Hence, for any collection of good potion ingredients \(\mathscr {F} = \left\{ S_i \big | i \in \tau \right\} \), we have a scheme \({{\,\textrm{Proj}\,}}\mathscr {F}\). Definition 11 The (full) multi-graded Brenner–Schröer Proj scheme of A is the scheme obtained by gluing the potion schemes associated with all good potion ingredients of A. 9 Enlarging Families of Good Potion Ingredients In this section, we will show that given any family of good potion ingredients \(\mathscr {F}\), we can replace it with a larger family \(\mathscr {F'}\) while having \({{\,\textrm{Proj}\,}}\mathscr {F}\) and \({{\,\textrm{Proj}\,}}\mathscr {F'}\) being isomorphic as schemes. By enlarging the family of good potion ingredients, we will have more open sets of the form \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(S)\) at our disposal. Suppose \(\mathscr {F}\) and \(\mathscr {F'}\) are two families of good potion ingredients indexed by \(\tau \) and \(\tau '\) respectively. We use the notation \(\small {\texttt {le}}: \mathscr {F} \le \mathscr {F'}\) to mean an injective function \(\small {\texttt {le}}: \tau \rightarrow \tau '\) such that \(\mathscr {F}'\circ \small {\texttt {le}} = \mathscr {F}\). We shall refer to such a map \(\small {\texttt {le}}\) as an embedding of families of good potion ingredients. Remark 7 In Lean4, the type class is a proposition, our type contains data, hence writing \(\mathscr {F} \le \mathscr {F'}\) without specifying the underlying function \(\small {\texttt {le}}\) is not accurate. Construction 7 Suppose \(\small {\texttt {le}}: \mathscr {F} \le \mathscr {F}'\) and \(i \in \tau \), we have an isomorphism of rings \({{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}'_{\small {\texttt {le}}(i)} \right) \cong {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_i \right) \). Hence, we can glue a family of scheme morphisms to form a morphism of schemes \({{\,\textrm{Proj}\,}}\small {\texttt {le}}: {{\,\textrm{Proj}\,}}\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}'\), One can check that at every point \(x \in {{\,\textrm{Proj}\,}}\mathscr {F}\), the morphism on stalks induced by \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\) is an isomorphism. Lemma 26 Topologically, \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\) is injective. Proof Suppose \(x \in {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_j \right) \) and \(x' \in {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_{j'} \right) \) are two points such that \({{\,\textrm{Proj}\,}}\small {\texttt {le}}(x) = {{\,\textrm{Proj}\,}}\small {\texttt {le}}(x')\). Let us denote \(X \in {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}'_{\small {\texttt {le}}(j)} \right) \) and \(X' \in {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}'_{\small {\texttt {le}}(j')} \right) \) to be the points corresponding to x and \(x'\) respectively. From \({{\,\textrm{Proj}\,}}\small {\texttt {le}}(x) = {{\,\textrm{Proj}\,}}\small {\texttt {le}}(x')\), we have the image of X and \(X'\) in \({{\,\textrm{Proj}\,}}\mathscr {F}'\) are the same. Therefore, either \(\small {\texttt {le}}(j) =\small {\texttt {le}}(j')\) and \(X = X'\) or there exists some point \(y \in {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}'_{\small {\texttt {le}}(j)} \mathscr {F}'_{\small {\texttt {le}}(j')}\right) \) and \(X = X' = y\) as points in \({{\,\textrm{Proj}\,}}\mathscr {F}'\). In either cases, we have \(x = x'\). \(\square \) Lemma 27 Let U be an open set in \({{\,\textrm{Proj}\,}}\mathscr {F}\) and \(i \in \tau \), \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\left( U \cap {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_i \right) \right) \) is an open set. Proof We consider the following diagram: where x is defined as \({{\,\textrm{Spec}\,}}\left( {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}'_{\small {\texttt {le}}(i)} \right) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_{i} \right) \right) \). \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\left( U \cap {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_i \right) \right) \) is equal to the range of the second row; since the second row is a composition of open map, the range is open. \(\square \) Corollary 28 The morphism \({{\,\textrm{Proj}\,}}\small {\texttt {le}}: {{\,\textrm{Proj}\,}}\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}'\) is an open immersion. Proof Since the induced stalk map at each point is an isomorphism, we only need to show that the morphism is a topological embedding. By Theorem 26, the morphism is injective; hence, we only need to show that the morphism is an open map. Let U be an open set in \({{\,\textrm{Proj}\,}}\mathscr {F}\), then \(U = \bigcup _i \left( U \cap {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(\mathscr {F}_i) \right) \). Thus, the image of U is equal to the union of the images of \(U \cap {{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(\mathscr {F}_i)\) under \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\); being a union of open sets, it is open as well. \(\square \) Definition 12 For any family \(\mathscr {F}= \left\{ S_i \big | i \in \tau \right\} \) of good potion ingredients, we denote \(\mathscr {F}^{+}\) to be the family indexed by the disjoint union of \(\tau \) and \(\tau \times \left\{ S \big | S~\text {is a good potion ingredient} \right\} \) We define \(\small {\texttt {le}}: \mathscr {F}\le \mathscr {F}^{+}\) by the left inclusion. Theorem 29 The morphism \({{\,\textrm{Proj}\,}}\small {\texttt {le}}: {{\,\textrm{Proj}\,}}\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}^{+}\) is an isomorphism. Proof Since the morphism is an open immersion, we only need to show that topologically, it is surjective. Suppose \(x \in {{\,\textrm{Proj}\,}}\mathscr {F}^{+}\), then either x is in \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(\mathscr {F}_i)\) for some \(i \in \tau \) or x is in \({{\,\textrm{Spec}\,}}{{\,\mathrm{\vartheta }\,}}(\mathscr {F}_i T)\) for some \(i \in \tau \) and some good potion ingredient T. In the first case, the preimage of x under \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\) is the point x itself. In the second case, let \(T'\) be a potion generator of T over \(\mathscr {F}_i\). By Theorem 20, we have a ring isomorphism \(e: {{\,\mathrm{\vartheta }\,}}(\mathscr {F}_i)_{\textsf {s}(T')} \cong {{\,\mathrm{\vartheta }\,}}\left( \mathscr {F}_i T \right) \). Hence, the preimage of x under \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\) is the pullback of x along the morphism \(\square \) Remark 8 \(\mathscr {F}^+\) is the type theoretic version of \(\mathscr {F}\cup \mathscr {F}\cdot \left\{ S\big |S~\text { is a good potion ingrient} \right\} \). We have to use the construction in Definition 12 because the generality we choose is families of good potion ingredients indexed by a type. If \(\mathscr {F}\) is a set of good potion ingredients, we see \(\mathscr {F}\) as a family indexed by \(\mathscr {F}\) itself. If \(\mathscr {F}\subseteq \mathscr {F}'\) are two sets of good potion ingredients, we can define \(\small {\texttt {le}}: \mathscr {F}\le \mathscr {F}'\) by the usual inclusion. Then, we can repeat the proof in Theorem 29 and show that the morphism \({{\,\textrm{Proj}\,}}\small {\texttt {le}}: {{\,\textrm{Proj}\,}}\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}^{+}\) is an isomorphism where \(\mathscr {F}^{+}\) is the set \(\mathscr {F}\cup \mathscr {F}\cdot \left\{ S\big |S~\text { is a good potion ingrient} \right\} \). 10 Functoriality In this section, we work with graded ring homomorphisms \(\Phi : A \rightarrow B\) and \(\Psi : B \rightarrow C\) among \(\iota \)-graded \(R_0\) algebras where \(\iota \) is an abelian group. Theorem 30 Let \(\mathscr {F}\) be a family of good potion ingredients indexed by \(\tau \), we have a morphism of schemes \({{\,\textrm{Proj}\,}}\Phi : {{\,\textrm{Proj}\,}}\Phi _{\star }\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}\), where \(\Phi _{\star }\mathscr {F}\) is the family defined by \(i \mapsto \Phi _{\star }\mathscr {F}_i\). Proof For each \(i \in \tau \), we have a ring homomorphismFootnote 3\(\small {\texttt {potionToMap}}: {{\,\mathrm{\vartheta }\,}}(\mathscr {F}_i) \rightarrow {{\,\mathrm{\vartheta }\,}}\left( \Phi _{\star }\mathscr {F}_i \right) \). Therefore, we have a family of morphisms of schemes We can glue these morphisms to form a morphism of schemes \({{\,\textrm{Proj}\,}}\Phi _{\star }\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}\). \(\square \) Corollary 31 \({{\,\textrm{Proj}\,}}\textsf {id}_A: {{\,\textrm{Proj}\,}}\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}\) is the identity and \({{\,\textrm{Proj}\,}}(\Psi \circ \Phi ) = {{\,\textrm{Proj}\,}}\Phi \circ {{\,\textrm{Proj}\,}}\Psi \). Remark 9 Since \({\textsf {id}_A}_{\star }\mathscr {F}\) is not definitionally equal to \(\mathscr {F}\), will not type-check. Hence, we use \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\) constructed in construction 7 to create a morphism \({{\,\textrm{Proj}\,}}{\textsf {id}_A}_{\star }\mathscr {F}\rightarrow {{\,\textrm{Proj}\,}}\mathscr {F}\). Similarly, since \((\Psi \circ \Phi )_{\star }\mathscr {F}\) is not definitionally equal to \(\Psi _{\star }\left( \Phi _{\star }\mathscr {F}\right) \), we formalise \({{\,\textrm{Proj}\,}}(\Psi \circ \Phi ) = {{\,\textrm{Proj}\,}}\Phi \circ {{\,\textrm{Proj}\,}}\Psi \) as follows: In both cases, \(\small {\texttt {le}}\) is nothing but the identity function on \(\tau \), but nevertheless, \({{\,\textrm{Proj}\,}}\small {\texttt {le}}\) is not literally the identity map. Hence, set theoretically, we have checked that \({{\,\textrm{Proj}\,}}\) is a contravriant functor from the category of graded ring to the category of schemes; however, type theoretically, we cannot write the functor down, at least not in the current formulation. 11 Dilatations of Rings [9, file location: Dilatation] In this section, we formalize the notion of dilatations of rings as studied in [5, 11, 15]. We fix a commutative unital ring A. A multi-center in A is a a collection \(\{ [M_i, a_i]\}_{i \in I}\) where each \(M_i\) is an ideal of A and each \(a_i\) is an element in A [11]. For each index, we define a larger ideal as \(L_i= M_i + (a_i)\). Let \(\mathbb {N}_I \) be the monoid \(\bigoplus _{i \in I} \mathbb {N} \). If \(\nu = (\nu _1, \ldots , \nu _i, \ldots ) \in \mathbb {N} _I \) we put \(L^{\nu }= L_1 ^{\nu _1} \cdots L_i ^{\nu _i} \cdots \) (product of ideals of A) and \(a^{\nu }= a_1^{\nu _1 } \cdots a_i ^{\nu _i} \cdots \) (product of elements of A). Note that if \(\nu \in \mathbb {N} _{I}\) is such that \(\nu _i =0\) for all i, then \(L_i^{\nu _i}= L^\nu =A\). We also put \(a^{\mathbb {N} _I} = \{ a^\nu | \nu \in \mathbb {N} _I \} \subset A\). Definition 13 The dilatation of A with multi-center \(\{[M_i, a_i] \}_{i \in I}\) is the unital commutative ring \(A[\big \{ \frac{M_i}{a_i}\big \}_{i \in I}]\) defined as follows: \(\bullet \) The underlying set of \(A[\big \{ \frac{M_i}{a_i}\big \}_{i \in I}]\) is the set of equivalence classes of symbols \(\frac{m}{a^{\nu }} \) where \( \nu \in \mathbb {N} _I\) and \(m \in L^{\nu }\) under the equivalence relation From now on, we abuse notation and denote a class by any of its representative \(\frac{m}{a^{\nu }}\) if no confusion is likely. \(\bullet \) The addition law is given by \(\frac{m}{a^{\nu }}+ \frac{p}{a^{\beta }}= \frac{m a^{\beta } + p a^{\nu }}{a^{\beta + \nu }}\). \(\bullet \) The multiplication law is given by \(\frac{m}{a^{\nu }}\times \frac{p}{a^{\beta }} = \frac{ mp}{a^{\nu + \beta }}\). \(\bullet \) The additive neutral element is \(\frac{0}{1}\) and the multiplicative neutral element is \(\frac{1}{1}\). We have a canonical morphism of rings \(A \rightarrow A[\big \{ \frac{M_i}{a_i}\big \}_{i \in I}]\) given by \(a \mapsto \frac{a}{1}\). We sometimes use the notations \(A[\frac{M}{a}]\) or \(A[\big \{ \frac{M_i}{a_i}:i \in I \big \}]\) to denote \(A[\big \{ \frac{M_i}{a_i}\big \}_{i \in I}]\). In the formalization, we first introduce a structure encoding all symbolic fractions. We then introduce the equivalence class on fractions to define the dilatation as a set. We then implement the addition and the multiplication on fractions and check compatibility with the equivalence relation. We thus obtain the formalization of the dilatation semiring. We formalize that A[F] is an A-algebra. We prove that the image of \(a^\nu \) in the dilatation is always a nonzerodivisor. As another fundamental property, we prove that \((a^\nu )= L^\nu \) in the dilatation. We now implement that if A is a ring (not only a semiring), then the dilatation is also a ring as it is compatible with opposite. We now come to the universal property [11]. Proposition 32 (Universal property) If \(\chi : A \rightarrow B\) is a morphism of rings such that \(\chi (a_i) \) is a non-zero-divisor and generates \(\chi (L_i) B\) for all \(i\in I\), then there exists a unique morphism \(\chi '\) of A-algebras \(A[\big \{ \frac{M_i}{a_i}\big \}_{i \in I}] \rightarrow B\). The morphism \(\chi '\) sends \(\frac{l}{a^\nu } \) to the unique element \(b \in B \) such that \(\chi ( a^\nu ) b = \chi (l)\). We split the formalization as follows. Data Availability No datasets were generated or analysed during the current study. Notes When x is not the complement of a prime ideal, the better notation for localized ring is \(x^{-1}A\). But we use this notation to keep align with homogeneous localization defined below. This isomorphism motivates the name “good potion ingredients”, because the potions made from R, S and T mix well. See Sect. 7. References Bouthier, A., Vasserot, E.: On the geometric Satake equivalence for Kac–Moody groups (2025). arXiv:2510.11466 Brenner, H., Schröer, S.: Ample families, multihomogeneous spectra, and algebraization of formal schemes. Pac. J. Math. 208(2), 209–230 (2003) Buzzard, K., Hughes, C., Lau, K., Livingston, A., Fernandez Mir, R., Morrison, S.: Schemesin Lean. Exp. Math. 31(2), 355–363 (2022) de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Automated Deduction—CADE vol. 28. Lecture Notes in Computer Science, 12699, pp. 625–635. Springer, Cham (2021) Dubouloz, A., Mayeux, A., dos Santos, J.P.: A survey on algebraic dilatations. Fields Institute Monographs (to appear) Grothendieck, A.: EGA: II. Etude globale elementaire de quelques classes de morphismes Publications mathématiques de l’I.H.E.S., tome 8, 5–222 (1961) Kuronya, A., Souza, P., Ulirsch, M.: Tropicalization of toric prevarieties. Preprint (2025). arXiv:2107.03139 Li, F., Zhang, J.: Dimension Theory in Lean4, (2025). https://github.com/jjaassoonn/DimensionTheory Mayeux, A., Zhang, J.: Multi-graded Proj construction in Lean4 (2025). https://github.com/ProjConstruction/Proj Mayeux, A., Zhang, J.: The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction. In: Lie Theory and Its Applications in Physics. Springer Proc. Math. Stat.(to appear). arXiv:2509.15116 Mayeux, A.: Multi-centered dilatations congruent isomorphisms and Rost double deformation space. Transf. Groups. 31, 1801–1850 (2026) Mayeux, A., Riche, S.: On multi-graded Proj schemes. Publ. Res. Inst. Math. Sci. 62(1), 115–176 (2026) Tang, L.: The \(P^1\)-motivic Gysin map (2026). arXiv:2604.24888 The mathlib Community: Mathlib4 Documentation The Stacks Project Authors: The Stacks Project. (2026). https://stacks.math.columbia.edu Wieser, E., Zhang, J.: Graded rings in Lean’s dependent type theory. In: Intelligent Computer Mathematics. Lecture Notes in Computer Science. Lecture Notes in Artificial Intelligence, vol. 13467, pp. 122–137. Springer, Cham (2022) Yasuda, T.: An algorithm for the minimal model program in dimension three (2026). arXiv:2603.13703 Zhang, J.: Formalising the Proj construction in Lean. In: 14th International Conference on Interactive Theorem Proving, Art. No. 35. LIPIcs. Leibniz Int. Proc. Inform., vol. 268. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) Acknowledgements We thank the referee for a careful reading of the manuscript and for providing valuable comments that helped improve the exposition of the formalized results. We also thank the referee for pointing out several issues and typos in the mathematical presentation. A. M. acknowledges support from ISF Grant No. 1577/23 at the Einstein Institute of Mathematics, The Hebrew University of Jerusalem. Author information Authors and Affiliations Contributions A.M. initiated the project and led the mathematics, while J.Z. led coding; both contributed to mathematics, coding, and manuscript preparation. Corresponding author Ethics declarations Conflict of interest The authors declare no competing interests.. Additional information Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Rights and permissions Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. About this article Cite this article Mayeux, A., Zhang, J. Formalizing Multi-graded Brenner–Schröer Proj Schemes and Dilatations of Rings in Lean4. J Autom Reasoning 70, 17 (2026). https://doi.org/10.1007/s10817-026-09764-x Received: Accepted: Published: Version of record: DOI: https://doi.org/10.1007/s10817-026-09764-x