Eric Wieser^{1}, Jujian Zhang^{2}
^{1}Cambridge University Engineering Department, ^{2}Imperial College London
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}$Free monoid over $a, b$:
$A_n = \{\prod_{i=1}^n x_i \,|\, \forall i, x_i \in \{a, b\}\}, n : \mathbb{N}$Free abelian monoid $a, b$:
$A_n = \{a^ib^j\,|\, i + j = n\}, n : \mathbb{N}$… or $A_n = \{a^{n_0}b^{n_1}\}, n : \mathbb{N} \times \mathbb{N}$
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}$Tensor algebra, $\mathcal{T}(V)$:
$A_n = \operatorname{span}\{\bigotimes_{i=1}^n v_i \,|\, \forall i, v_i : V \}, n : \mathbb{N}$Multivariate polynomials:
$A_n = \operatorname{span} \{x^iy^j\,|\, i + j = n\}, n : \mathbb{N}$Clifford algebra, $\mathcal{Cl}(Q)$:
$A_n = \operatorname{span} \{\prod_{u \in s} u\,|\, |s| \% 2 = n \}, n : \mathbb{Z}/2\mathbb{Z}$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}$
Free monoids
Free abelian monoids
Tensor powers
Polynomials in $x$
Tensor algebra, $\mathcal{T}(V)$
Multivariate polynomials
Clifford algebra, $\mathcal{Cl}(Q)$
Graded modules as nat -> FreeModule R
, no mention of multiplication.
Effective homology of bicomplexes, formalized in Coq Domínguez, C., Rubio, J. (Mar 2011)
One specific graded ring, but no* abstraction
Synthetic Integral Cohomology in Cubical Agda Brunerie, G., Ljungström, A., Mörtberg, A. (Feb 2022)
GradedRing
abstraction!)Lots of discussion, no implementation
Lean Zulip > #maths > CDGAs Barton, R., Commelin, J., Buzzard, K., Lau, K., … (Jun 2019)
Liquid Tensor Experiment, uses graded rings.
A : ι → Type*
Tuples, A n := fin n → M
Tensor powers,A n := ⨂[R]^n M
A : ι → set α
α := free_monoid X
α := polynomial R
α := tensor_algebra R M
A : ι → Type*
Tuples, A n := fin n → M
Tensor powers,A n := ⨂[R]^n M
A : ι → set α
α := free_monoid X
α := polynomial R
α := tensor_algebra R M
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
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 |
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 }
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 }
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 -/
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)
A : ι → Type*
Tuples, A n := fin n → M
Tensor powers,A n := ⨂[R]^n M
A : ι → set α
α := free_monoid X
α := polynomial R
α := tensor_algebra R M
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 monoidsA : ι → set R
graded semi-ringsA : ι → add_submonoid R
graded ringsA : ι → add_subgroup R
graded algebrasA : ι → 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⟩
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
!
(⋃ i, A i) = set.univ ∧ pairwise (disjoint on A)
grade : α → ι
where a ∈ A i ↔ grade a = i
(⨆ i, A i) = ⊤ ∧ complete_lattice.independent A
*
*Insufficient for semirings! Consider even/odd grading by $\mathbb{Z}_{\ge0}$ and $\mathbb{Z}_{\le0}$…⨁ 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')
Any internal representation, A : ι → set α
…
A 0
A i
A j
… can be written externally via ↥s = subtype (∈ s)
:
↥(A 0)
↥(A i)
↥(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?
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
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))
A : ι → submodule R α
A : ι → add_subgroup α
A : ι → add_submonoid α
A : ι → set α
A : ι → submodule R α
A : ι → add_subgroup α
A : ι → add_submonoid α
set_like.graded_monoid A
direct_sum.decomposition A
Typeclasses, definitions, and lemmas for internally- and externally-graded algebra, rings, and monoids.
~1200sloc
API
~1300sloc
Applications
~5000sloc
Alg. geom.
Over 30 PRs to Lean's mathlib.