Graded rings in Lean's dependent type theorys

Eric Wieser¹, Jujian Zhang²
¹Cambridge University Engineering Department, ²Imperial College London

slides: eric-wieser.github.io/cicm-2022 2022-09-22

IntroductionGraded monoids

Axioms: $\forall (x \in A_i) (y \in A_j), xy \in A_{i+j}$, $1 \in A_0$

Free monoid over $a$:

$A_n = \{a^n\}, n : \mathbb{N}$

$$ \phantom{\smallunderbrace{a^{\smash2}b}{\tiny[2, 1]} \times \smallunderbrace{a^{\smash3}b}{\tiny[3, 1]}} \mathllap{\smallunderbrace{a^{\smash2}}{2} \times \smallunderbrace{a^{\smash3}}3} = \mathrlap{\smallunderbrace{a^{\smash5}}{\mathclap{2 + 3}}} \phantom{\smallunderbrace{a^{\smash2}ba^{\smash3}b}{3 + 4}}$$

Free monoid over $a, b$:

$A_n = \{\prod_{i=1}^n x_i \,|\, \forall i, x_i \in \{a, b\}\}, n : \mathbb{N}$

$$ \phantom{\smallunderbrace{a^2b}{\tiny[2, 1]} \times \smallunderbrace{a^3b}{\tiny[3, 1]}} \mathllap{\smallunderbrace{a^2b}3\times \smallunderbrace{a^3b}4} = \smallunderbrace{a^2ba^3b}{3 + 4}$$

Free abelian monoid $a, b$:

$A_n = \{a^ib^j\,|\, i + j = n\}, n : \mathbb{N}$

$$\phantom{\smallunderbrace{a^2b}{\tiny[2, 1]} \times \smallunderbrace{a^3b}{\tiny[3, 1]}} \mathllap{\smallunderbrace{a^2b}3\times \smallunderbrace{a^3b}4} = \mathrlap{\smallunderbrace{a^5b^2}{3 + 4}} \phantom{\smallunderbrace{a^2ba^3b}{3 + 4}}$$

… or $A_n = \{a^{n_0}b^{n_1}\}, n : \mathbb{N} \times \mathbb{N}$

$$\smallunderbrace{\hphantom{a^2b}}{\tiny[2, 1]} \hphantom{{}\times{}} \smallunderbrace{\hphantom{a^3b}}{\tiny[3, 1]} \hphantom{{}={}} \mathrlap{\smallunderbrace{\hphantom{a^5b^2}}{\tiny\mathclap{[2 + 3, 1 + 1]}}} \hphantom{\smallunderbrace{a^2ba^3b}{3 + 4}}$$

I'll start by introducing what a graded monoid is. We say that "A" is a graded monoid if is a monoid, and it decomposes into a indexed family of grades such that the product of two elements of grades "i" and "j" belongs to the grade of index "i" plus "j". We also require that that the identity belongs to grade zero.

The simplest example is the free monoid over one generator; here the indices of the grades are natural numbers, and each grade consists of just the generator raised to the appropriate power. We can see that the graduation obviously respects our axioms.

Adding another generator, we can extend this to grading a free monoid by the length of its monomials.

We can do exactly the same thing if our free monoid is forced to be abelian...

...but this choice of grading is not the only option. The axioms do not force us to pick our indices as the natural numbers, but any additive monoid would suffice. Here, we can use pairs of naturals as our grade, which separately count the degrees of "a" and "b".

IntroductionGraded rings

Extra axioms: $\forall (x \!\in\!A_i) (y \!\in\!A_i), x + y \!\in\!A_{i}$, $0 \in A_i$

Polynomials in $x$:

$A_n = \{rx^n| r : R\}, n : \mathbb{N}$

$$\smallunderbrace{37}0 + \smallunderbrace{x}1 + \smallunderbrace{x^3}3$$

Tensor algebra, $\mathcal{T}(V)$:

$A_n = \operatorname{span}\{\bigotimes_{i=1}^n v_i \,|\, \forall i, v_i : V \}, n : \mathbb{N}$

$$\smallunderbrace{37}0 + \smallunderbrace{u}1 + \smallunderbrace{u\!\otimes\!v\!\otimes\!u}3$$

Multivariate polynomials:

$A_n = \operatorname{span} \{x^iy^j\,|\, i + j = n\}, n : \mathbb{N}$

$$\smallunderbrace{\mathrlap{\phantom{y}}x^{\smash2}}2 + \smallunderbrace{y^{\smash3}}3 + \smallunderbrace{x^{\smash5}y^{\smash2}}7$$

… or $A_n = \{ra^{n_0}b^{n_1}\,|\,r : R\}, n : \mathbb{N} \times \mathbb{N}$

$$\smallunderbrace{\hphantom{x^2}}{\mathclap{\tiny[2, 0]}} \hphantom{{} + {}} \smallunderbrace{\hphantom{y^3}}{\mathclap{\tiny[0, 3]}} \hphantom{{} + {}} \smallunderbrace{\hphantom{x^5y^2}}{\mathclap{\tiny[5, 2]}}$$

Clifford algebra, $\mathcal{Cl}(Q)$:

$A_n = \operatorname{span} \{\prod_{u \in s} u\,|\, |s| \% 2 = n \}, n : \mathbb{Z}/2\mathbb{Z}$

$$\smallunderbrace{uv + 1}{0\text{ (even)}} + \smallunderbrace{uvw + v}{1\text{ (odd)}}$$

Graded rings build upon graded monoids and rings, by requiring that each grade is additionally closed under addition and contains zero. Additionally, instead of our terms consisting of a single grade, they now consist of a sum of terms of different grades.

The simplest example is the polynomials in one variable, which can be very obviously expressed in this kind of sum.

Like the free monoid on the previous slide, we can grade the tensor algebra by the number of generators in each term.

Multivariate polynomials fit naturally in this pattern too, either by using the total degree of the monomial as the index, or as we did on the previous slide, using separate degrees for each variable.

The final example of a graded ring I include here is the clifford algebra, which can only be split into even and odd parts.

IntroductionSummary of examples

Graded monoids

Graded rings

Axioms

Monoid, $1 \in A_0$, $\forall (x \in A_i) (y \in A_j), xy \in A_{i+j}$

Ring, graded monoid, $0 \in A_i$, $\forall (x \!\in\!A_i) (y \!\in\!A_i), x + y \!\in\!A_{i}$

Examples

Free monoids

Free abelian monoids

Tensor powers

Polynomials in $x$

Tensor algebra, $\mathcal{T}(V)$

Multivariate polynomials

Clifford algebra, $\mathcal{Cl}(Q)$

IntroductionExisting formalizations

Coq

Graded modules as nat -> FreeModule R, no mention of multiplication.

Effective homology of bicomplexes, formalized in Coq Domínguez, C., Rubio, J. (Mar 2011)

Agda

One specific graded ring, but no* abstraction

Synthetic Integral Cohomology in Cubical Agda Brunerie, G., Ljungström, A., Mörtberg, A. (Feb 2022)

(^*after submission of our work; a new GradedRing abstraction!)

Lean

Lots of discussion, no implementation

Lean Zulip > #maths > CDGAs Barton, R., Commelin, J., Buzzard, K., Lau, K., … (Jun 2019)

IntroductionWhy generalize?

Unified spelling for graded operations
Some constructions build upon this generalization:
- The $\operatorname{Proj} S$ in algebraic geometry needs homogeneous ideals
- Homogeneous ideals needs graded rings
One proof of Gordan's lemma, needed for Lean's Liquid Tensor Experiment, uses graded rings.

External or Internal?

External: `A : ι → Type*`

$A_0$

$\cdots$

$A_i$

$\cdots$

$A_j$

$\Sigma_i A_i$ or $\bigoplus_i A_i$

Tuples, A n := fin n → M

Tensor powers,
A n := ⨂[R]^n M

Internal: `A : ι → set α`

$A_0$

$\cdots$

$A_i$

$\cdots$

$A_j$

$\alpha$

α := free_monoid X

α := polynomial R

α := tensor_algebra R M

Let's move on to representing graded objects in type theory. There are two ways we can do this.

The first option is to start with a collection of independent types $A$, and glue them together into a single type using either dependent pairs or direct sums, depending on whether we are working with graded monoids or graded rings.

The second option is to start with the carrier type alpha, and divide it into a collection of suitable subsets $A$.

Which is more natural will depend on the object in question.

External gradings appear naturally when working with n-tuples, or with nth powers formed by quotienting those tuples.

Internal gradings are more useful when we already have a carrier type defined without reference to grade, such as the free monoid, polynomials, or the tensor algebra.

We want to be able to use both viewpoints; and in the case of tensor algebra, we want to translate between the two! We will come back to this.

External or Internal?

External: `A : ι → Type*`

$A_0$

$\cdots$

$A_i$

$\cdots$

$A_j$

$\Sigma_i A_i$ or $\bigoplus_i A_i$

Tuples, A n := fin n → M

Tensor powers,
A n := ⨂[R]^n M

Internal: `A : ι → set α`

$A_0$

$\cdots$

$A_i$

$\cdots$

$A_j$

$\alpha$

α := free_monoid X

α := polynomial R

α := tensor_algebra R M

External gradingsEquality difficulties

Given an indexed family of types,


            variables {ι : Type*} {A : ι → Type*}

what's a graded semigroup?


            class «fails».g_semigroup [has_add ι][add_semigroup ι] :=
            (mul {i j} : A i → A j → A (i + j))
            (mul_assoc {i j k} (x : A i) (y : A j) (z : A k) :
              mul (mul x y) z = mul x (mul y z))

Equal:


                example {i j k : ι}
                  [add_semigroup ι] :
                  (i + j) + k = i + (j + k) :=
                add_assoc _ _ _

But not definitionally so:


                example {i j k : ι}
                  [add_semigroup ι] :
                  (i + j) + k = i + (j + k) :=
                rfl

We start with a index type iota, and a family of types A. To keep things short, we'll try to define a graded semigroup, which is a graded monoid without a unit.

We can start by writing down that we want a multiplication function whose output grade is the sum of the input grades, which means we need an addition on iota.

However, when we try and write down that this multiplication is associative, lean complains about the equality

Specifically, it complains that the indices of the family on the LHS and the RHS are not equal!

If we want these to be equal, we certainly will require that addition in the indices is associative, which we do by putting add_semigroup here. This doesn't make our error go away though!

Here's what's going on; while the two indices causing us trouble are equal, as we can prove with add_assoc…

…lean doesn't consider them equal by definition. We're going to have to try something else to state associativity.

External gradingsEquality alternatives

1. Heterogenous equality


              class «heq».g_semigroup [add_semigroup ι] :=
              (mul {i j} : A i → A j → A (i + j))
              (mul_assoc {i j k} (x : A i) (y : A j) (z : A k) :
                mul (mul x y) z == mul x (mul y z))

2. Equality of dependent pairs


              class «sigma».g_semigroup [add_semigroup ι] :=
              (mul {i j} : A i → A j → A (i + j))
              (mul_assoc {i j k} (x : A i) (y : A j) (z : A k) :
                (⟨_, mul (mul x y) z⟩ : Σ i, A i) = ⟨_, mul x (mul y z)⟩)

3. Propositional enforcement


              class «extends».g_semigroup [add_semigroup ι]
                extends semigroup (Σ i, A i) :=
              (fst_mul {i j} (x : A i) (y : A j) :
                (⟨_, x⟩ * ⟨_, y⟩ : Σ i, A i).fst = i + j)

4. Equality via a cast


              class «eq.rec».g_semigroup [add_semigroup ι] :=
              (mul {i j} : A i → A j → A (i + j))
              (mul_assoc {i j k : ι} (x : A i) (y : A j) (z : A k) :
                (add_assoc i j k).rec (mul (mul x y) z) = mul x (mul y z))

5. Equality via a user-provided cast


              class «cast».g_semigroup [add_semigroup ι] :=
              (cast {i j} (h : i = j) : A i → A j)
              (cast_rfl {i} (x : A i) : cast rfl x = x)
              (mul {i j} : A i → A j → A (i + j))
              (mul_assoc {i j k : ι} (x : A i) (y : A j) (z : A k) :
                cast (add_assoc i j k) (mul (mul x y) z) = mul x (mul y z))

6. Folding the cast into the multiplication itself


              class «h : i+j=k».g_semigroup [add_semigroup ι] :=
              (mul {i j k} (h : i + j = k) : A i → A j → A k)
              (mul_assoc {i j k ij jk ijk : ι} (hij : i + j = ij) (hjk : j + k = jk)
                (hi_jk : i + jk = ijk) (hij_k : ij + k = ijk)
                (x : A i) (y : A j) (z : A k) :
                  (mul hij_k (mul hij x y) z) = mul hi_jk x (mul hjk y z))

Approach	1	2	3	4	5	6
producer difficulty	medium	harder	easier	hardest	easier	medium
consumer `rw` directions	—	↔	↔	←	←	↔*
`(i+j)+k=i+(j+k)` proved by	producer	producer Our choice	—	—	—	consumer

There are plenty of alternative ways to state this equality that would avoid the problem. Let's look at a handful of them

The first option is to use heterogenous equality, which lets us state equalities between types that are not equal by definition.

The second option is state the equality in terms of dependent pairs, which we write with a sigma.

The third option is rather different, and instead says that a graded monoid is just a monoid on dependent pairs such that the indices combining additively is enforced propositionally, rather than by definition.

The next three options are similar, and involve inserting a cast between the two non-equal types; either via the recursor for equality, …

…a user-provided cast that is shown to be well-behaved,…

…or by even putting the casting within the multiplication operator itself; though this is very messy!

Mathematically all these approaches are valid; so at best we can evaluate the choice qualitatively.

One thing we could estimate is how hard it is to prove a type satisfies this typeclass, which we'll call the producer.

Another thing we can look at is how easy it is to use the mul_assoc axiom, and whether it's stated in a way that is symmetric and so can be used in both directions by the rewrite tactic in consumer code.

Finally, we should consider whether the producer or consumer will have to repeatedly prove that addition of the indices is associative. Option 6 is particularly bad for this.

In this work we opted for option 2; while option 3 appears to win out in this table, it turns out to be awkward when we start looking at graded rings.

External gradingsGraded monoids


            def graded_monoid (A : ι → Type*) : Type* := sigma A
            notation `Σᵍ` binders `, ` r:(scoped A, graded_monoid A) := r

Graded instances imply instances on the type alias Σᵍ i, A i:


              class ghas_one [has_zero ι] :=
              (one : A 0)
            
              instance ghas_one.to_has_one
                [has_zero ι] [ghas_one A] :
                has_one (Σᵍ i, A i) :=
              { one := ⟨_, ghas_one.one⟩ }


              class ghas_mul [has_add ι] :=
              (mul {i j} : A i → A j → A (i + j))
            
              instance ghas_mul.to_has_mul
                [has_add ι] [ghas_mul A] :
                has_mul (Σᵍ i, A i) :=
              { mul := λ x y, ⟨_, ghas_mul.mul x.2 y.2⟩ }


          class gmonoid [add_semigroup ι] extends ghas_one A, ghas_mul A :=
          (one_mul       (a : Σᵍ i, A i) :       1 * a = a)
          (mul_one       (a : Σᵍ i, A i) :       a * 1 = a)
          (mul_assoc (a b c : Σᵍ i, A i) : (a * b) * c = a * (b * c))
          
          instance gmonoid.to_monoid [add_monoid ι] [gmonoid A] :
            monoid (Σᵍ i, A i) :=
          { one_mul := gmonoid.one_mul, mul_one := gmonoid.mul_one,
            mul_assoc := gmonoid.mul_assoc }

Instead of working directly with dependent pairs, which lean calls sigma, we define a type alias to remind ourselves that we are equiping it with graded operators, which we'll write as sigma g. As a reminder, this is just a pair of an index and a value of the corresponding grade.

We can start by defining a typeclass on our family A to say that grade 0 has a one. The trick here is that we can use this typeclass to a one for the new type alias.

We do the same thing for multiplication, again using the new typeclass to define multipliation for our alias.

The payoff is that when we define the axioms of a graded monoid in the style of the previous slide, we can now use notation instead of writing the word mul.

The final step is to show that if the family of grades obeys this typeclass, then the type alias forms a monoid, which we can do trivially by just copying the axioms.

External gradingsGraded monoids

Example

The $n$-tuples fin n → α, with
$1 \coloneqq ()$ and $(a, b) \times (c) \coloneqq (a, b, c)$:


                instance : gmonoid (λ n : ℕ, fin n → α) :=
                { one := ![],
                  mul := λ i j, fin.append',
                  one_mul := λ b, sigma_eq_of_eq_comp_cast _ (elim0_append' _),
                  mul_one := λ a, sigma_eq_of_eq_comp_cast _ (append'_elim0 _),
                  mul_assoc := λ a b c, sigma_eq_of_eq_comp_cast _ $
                    (append'_assoc a.2 b.2 c.2).trans rfl }

External gradingsGraded (semi)rings

Use the direct sum ⨁ i, A i instead of Σᵍ i, A i


              class gsemiring [add_monoid ι] [Π i, add_comm_monoid (A i)]
                extends gmonoid A :=
              (mul_zero {i j} (a : A i)            : mul a (0 : A j) = 0)
              (zero_mul {i j} (b : A j)            : mul (0 : A i) b = 0)
              (mul_add {i j} (a : A i) (b c : A j) : mul a (b + c) = mul a b + mul a c)
              (add_mul {i j} (a b : A i) (c : A j) : mul (a + b) c = mul a c + mul b c)

(= is equality of A k for some k, not Σᵍ i, A i)


            instance gsemiring.to_semiring [add_monoid ι] [gsemiring A]
              [Π i, add_comm_monoid (A i)] :
              semiring (⨁ i, A i) := sorry /- tedious but explained in the paper -/

bonus: works* for rings too!


              instance gsemiring.to_semiring [add_monoid ι] [gsemiring A]
                [Π i, add_comm_group (A i)] :
                ring (⨁ i, A i) := sorry /- *but not a good idea, see the paper -/

Lets move on to graded rings; or rather semirings, as these are more general. Here, we will be working with the direct sum instead of the dependent pair we used for graded monoids.

We proceed by defining yet another typeclass; this time, defining a graded semiring as a graded monoid whose grades are already equiped with addition, and that multiplication distributes appropriately. Note that we do not face the equality problems we had for associativity in these new axioms; the types are all definitionally equal.

Imitating what we did for monoids, our goal is now to use this typeclass to provide a semiring structure on the direct sum. This requires some care, and I'll leave the details to the paper.

A nice benefit of this approach is that we don't need a new `gring` typeclass; the axioms of gsemiring are enough if we already know that the individual grades form additive groups.

External gradingsGraded (semi)rings

Example

The $n$^th tensor powers form a graded (semi)ring


                variables {R} [field R] [add_comm_group V] [module R V]

                instance : gsemiring (λ n : ℕ, ⨂[R]^n V) :=
                sorry /- ~200 lines of prework to solve this -/

This is a prerequisite to state the
ring isomorphism to the tensor algebra:


                  def equiv_direct_sum : tensor_algebra R V ≃+* (⨁ n, ⨂[R]^n V) :=
                  sorry /- another ~200 lines of prework to solve this  -/

(uses gsemiring.to_semiring from the previous slide)

External or Internal?

External: `A : ι → Type*`

$A_0$

$\cdots$

$A_i$

$\cdots$

$A_j$

$\Sigma_i A_i$ or $\bigoplus_i A_i$

Tuples, A n := fin n → M

Tensor powers,
A n := ⨂[R]^n M

Internal: `A : ι → set α`

$A_0$

$\cdots$

$A_i$

$\cdots$

$A_j$

$\alpha$

α := free_monoid X

α := polynomial R

α := tensor_algebra R M

Internal gradingsGraded monoids


            class set.graded_monoid
              [monoid M] [add_monoid ι] (A : ι → set M) : Prop :=
            (one_mem : 1 ∈ A 0)
            (mul_mem ⦃i j : ι⦄ {gi gj : M} : gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j))
            
            class set_like.graded_monoid {S : Type*} [set_like S M]
              [monoid M] [add_monoid ι] (A : ι → S) : Prop :=
            (one_mem : 1 ∈ A 0)
            (mul_mem ⦃i j : ι⦄ {gi gj : M} : gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j))

We don't want to repeat ourselves for:

graded monoids
A : ι → set R

graded semi-rings
A : ι → add_submonoid R

graded rings
A : ι → add_subgroup R

graded algebras
A : ι → submodule S R

Solution:


              class set_like (S : Type*) (α : out_param Type*) :=
              (coe : S → set α) -- indirectly provides `∈` and `↥` notation
              (coe_injective' : function.injective coe)
              
              instance : set_like (add_submonoid R) R := ⟨add_submonoid.carrier, sorry⟩
              instance : set_like (add_subgroup R)  R := ⟨add_subgroup.carrier,  sorry⟩
              instance : set_like (submodule S R)   R := ⟨submodule.carrier,     sorry⟩

At this point it should be expected that I'm going to define yet another typeclass. Now that we're working with families of sets and there are no dependent types to worry about, the axioms are easier to state.

Unfortunately, we now have a new problem; while for graded monoids, we want to work with a family of sets…

…we also want to be able to work with families of additive subgroups in the context of graded rings, and other similar cases.

To save ourselves repeating every result four times, we introduce yet another typeclass, set_like! This one is used to indicate that a type behaves like a set.

We can then provide an instance for each of the cases above. The final step is to replace our family of sets

with a family of set_like objects.

Internal gradingsGraded rings

To get an internally-graded monoid:


            variables [monoid M]   [add_monoid ι] (A : ι → set M)
            variables [set_like.graded_monoid A]

To get an internally-graded semiring:


            variables [semiring R] [add_monoid ι] (A : ι → add_submonoid R)
            variables [set_like.graded_monoid A]

To get an internally-graded ring:


            variables [ring R]     [add_monoid ι] (A : ι → add_subgroup R)
            variables [set_like.graded_monoid A]

This isn't quite enough; we also need to require that the A i don't overlap!

Internal gradingsDecompositions

Monoids

(⋃ i, A i) = set.univ ∧ pairwise (disjoint on A)
grade : α → ι where a ∈ A i ↔ grade a = i

Rings

(⨆ i, A i) = ⊤ ∧ complete_lattice.independent A* *Insufficient for semirings! Consider even/odd grading by $\mathbb{Z}_{\ge0}$ and $\mathbb{Z}_{\le0}$…
bijectivity of the canonical map ⨁ i, ↥(A i) → α


                  -- constructively, where `coe_add_monoid_hom : ⨁ i, ↥(A i) →+ α` 
                  class direct_sum.decomposition (A : ι → S) :=
                  (decompose' : α → ⨁ i, A i)  -- split elements into their grades
                  (left_inv : left_inverse (coe_add_monoid_hom A) decompose')
                  (right_inv : right_inverse (coe_add_monoid_hom A) decompose')

Internal gradingsinterpreted externally

Any internal representation, A : ι → set α …

A 0

$\cdots$

A i

$\cdots$

A j

$\alpha$

… can be written externally via ↥s = subtype (∈ s):

↥(A 0)

$\cdots$

↥(A i)

$\cdots$

↥(A j)

Σᵍ i, ↥(A i) or ⨁ i, ↥(A i)

Σᵍ i, ↥(A i) and α should be isomorphic as monoids ⨁ i, ↥(A i) and α should be isomorphic as rings

What's the monoid/ring structure on the left?

Internal gradingsinterpreted externally


            instance set_like.gmonoid [monoid M] [add_monoid ι] [set_like S M]
              (A : ι → S) [set_like.graded_monoid A] : gmonoid (λ i, ↥(A i)) :=
            { one :=            ⟨1,     set_like.graded_monoid.one_mem⟩,
              mul := λ i j a b, ⟨a * b, set_like.graded_monoid.mul_mem a.prop b.prop⟩,
              one_mul := λ ⟨i, a, h⟩, sigma.subtype_ext (zero_add _) (one_mul _),
              mul_one := λ ⟨i, a, h⟩, sigma.subtype_ext (add_zero _) (mul_one _),
              mul_assoc := λ ⟨i, a, ha⟩ ⟨j, b, hb⟩ ⟨k, c, hc⟩, sorry /- etc -/ }
            
            -- finds `gmonoid.to_monoid`
            instance : monoid (Σᵍ i, ↥(A i)) := by apply_instance


            instance set_like.gsemiring [semiring R] [add_monoid ι]
              [set_like S R] [add_submonoid_class S R]
              (A : ι → S) [set_like.graded_monoid A] : gsemiring (λ i, ↥(A i)) :=
            { mul_zero := λ i j _, subtype.ext (mul_zero _),
              zero_mul := λ i j _, subtype.ext (zero_mul _),
              mul_add := λ i j _ _ _, subtype.ext (mul_add _ _ _),
              add_mul := λ i j _ _ _, subtype.ext (add_mul _ _ _),
              ..set_like.gmonoid A }
            
            -- finds `gsemiring.to_semiring`
            instance : semiring (⨁ i, ↥(A i)) := by apply_instance

Internal gradingsinterpreted externally

The payoff: a graded ring is isomorphic
to the direct sum of its parts


          variables [ring R] [add_monoid ι] (A : ι → add_subgroup R)
          variables [set_like.graded_monoid A] [direct_sum.decomposition A]

          -- ok!
          #check (direct_sum.decompose_ring_equiv : R ≃+* ⨁ i, ↥(A i))

Internal gradingsSummary of typeclasses

Graded $R$-algebra A : ι → submodule R α

↓

Graded ring A : ι → add_subgroup α

↓

Graded semiring A : ι → add_submonoid α

↓

Graded monoid A : ι → set α

Graded $R$-module A : ι → submodule R α

↓

Graded additive group A : ι → add_subgroup α

↓

Graded additive submonoid A : ι → add_submonoid α

⟶ ⟶ ⟶

set_like.graded_monoid A

direct_sum.decomposition A

What's next?

Graded modules over graded rings, with
$\forall (x \in R_i) (y \in M_j), xy \in M_{i+j}$
Algebraic geometry that uses graded objects

Contributions

Typeclasses, definitions, and lemmas for internally- and externally-graded algebra, rings, and monoids.

~1200sloc
API

~1300sloc
Applications

~5000sloc
Alg. geom.

github.com/eric-wieser/lean-graded-rings

Over 30 PRs to Lean's mathlib.

Graded rings in Lean's dependent type theorys

IntroductionGraded monoids

IntroductionGraded rings

IntroductionSummary of examples

Graded monoids

Graded rings

Axioms

Examples

IntroductionExisting formalizations

IntroductionWhy generalize?

External or Internal?

External: A : ι → Type*

Internal: A : ι → set α

External or Internal?

External: A : ι → Type*

Internal: A : ι → set α

External gradingsEquality difficulties

External gradingsEquality alternatives

External gradingsGraded monoids

External gradingsGraded monoids

Example

External gradingsGraded (semi)rings

External gradingsGraded (semi)rings

Example

External or Internal?

External: A : ι → Type*

Internal: A : ι → set α

Internal gradingsGraded monoids

Internal gradingsGraded rings

Internal gradingsDecompositions

Monoids

Rings

Internal gradingsinterpreted externally

Internal gradingsinterpreted externally

Internal gradingsinterpreted externally

Internal gradingsSummary of typeclasses

What's next?

Contributions

External: `A : ι → Type*`

Internal: `A : ι → set α`

External: `A : ι → Type*`

Internal: `A : ι → set α`

External: `A : ι → Type*`

Internal: `A : ι → set α`