Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3's typeclasses are used by mathlib for scalar actions with examples, illustrate some of the problems which come up when using them such as compatibility of actions and non-definitionally-equal diamonds, and note how these problems can be solved. We outline where more work is needed in mathlib in this area.
In this paper, we explore some of the design decisions made in mathlib [
A central language feature used by mathlib in expressing algebraic structure is that of typeclasses [1, section 4], which are used to equip types with canonical operators and properties of those operators. A simple example is the typeclass semigroup M , which equips the type M with the operator * and an associativity axiom mul_assoc . Working with typeclasses breaks down into three parts; declaring them with the class keyword, providing them with the instance keyword, and consuming them with [ ] around a typeclass name.
The semigroup typeclass from mathlib is declared roughly as follows, which reads “a type G has a multiplication if it has a binary operator called mul ” and “a type G is a semigroup if it has a multiplication and that multiplication is associative”. Note that the use of extends additionally tells Lean how to obtain an instance of has_mul G if it has semigroup G . class has_mul (G : Type*) := (mul : G → G → G) infix * := has_mul.mul class semigroup (G : Type*) extends has_mul G := (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
With this typeclass in place, we can write a theorem that applies to any semigroup by writing [semigroup G] in our argument list, as we do in mul_assoc₂ below. This tells Lean that whenever the mul_assoc₂ lemma is used on a type G , it should perform a typeclass search for a term of type semigroup G . In turn, it means that inside mul_assoc₂ we have access to the mul_assoc axiom of semigroups on G . lemma mul_assoc₂ {G : Type*} [semigroup G] (a b c d : G) :
a * (b * (c * d)) = ((a * b) * c) * d := by rw [mul_assoc, mul_assoc]
The final piece of the puzzle is how to inform the typeclass search that semigroup G is available for a particular type G . To demonstrate this, we define a structure opposite α that wraps a single element of an arbitrary type α . Using the instance keyword, we then equip it with a reversed multiplication structure, and express “For any type α such that α is itself a semigroup, opposite α is also a semigroup”. This method of “chaining” instances is central to the power of typeclasses, and is used extensively by mathlib in situations like equipping a product of groups with a group structure, or polynomials over a ring with a ring structure. -- `op` is the constructor name, `unop` is the projection structure opposite (α : Type*) := op :: (unop : α) instance (T : Type*) [semigroup T] : semigroup (opposite T) := { mul := λ a b, opposite.op (b.unop * a.unop),
mul_assoc := λ a b c, congr_arg opposite.op (mul_assoc c.unop b.unop a.unop).symm }
The typeclass we are most interested in this paper is has_scalar M α , which equips a type α with an action by elements of M denoted m • a . In practice, this is almost always used for group actions, which are actions that satisfies the additional fields in mul_action M α : class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α) infixr ` • `:73 := has_scalar.smul class mul_action (M : Type*) (α : Type*) [monoid M] extends has_scalar M α := (one_smul : ∀ a : α, (1 : M) • a = a) (mul_smul : ∀ (x y : M) (a : α), (x * y) • a = x • y • a) Note here that because we use [monoid M] instead of extends monoid M , we are stating that mul_action M α requires M to already be equipped with a monoid structure, rather than allowing mul_action M α to itself provide that structure.
mathlib extends these two typeclasses with a variety of additional axioms (i.e., fields holding proofs) for when M and α are themselves equipped with extra structures, such as distributivity over addition and actions by zero. The left hand side of fig. 1 shows the majority of these typeclasses, while details of their fields can be found either in [ 1, section 5.1] or in the mathlib docs.
Scalar actions can be roughly divided into two types: elementary actions which are intrinsic to a particular family of types, and derived actions which operate elementwise on “bigger” types built out of smaller types. We will start by giving some examples of the former.
One of the simplest actions we can construct is that of left-multiplication, with a * b = a • b , which mathlib provides as follows. instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := { smul := (*) } As the properties of the multiplication on α becomes stronger, so do those of this scalar action on α ; for instance when we have monoid α we can deduce mul_action α α , and when we have semiring α we can deduce module α α . The right-hand side of fig. 1 shows these available left multiplication structures with grey arrows.
mul_semiring_action algebra module comm_semiring semiring distrib_mul_action mul_action_with_zero
monoid_with_zero mul_action smul_with_zero mul_zero_class monoid has_scalar has_mul
Another simple action we can construct is that of repeated addition when α is a commutative additive monoid, an instance of module ℕ α , which can be defined recursively for a natural number as (0 : ℕ) • x = 0 and ∀ n : ℕ, (n + 1) • x = n • x + x . A similar approach can be used to define a module ℤ α instance when α additionally forms an additive group. These are respectively promoted to algebra ℕ α and algebra ℤ α structures when α forms a semiring or ring .
A typical example of a module action might be that of a scalar ℝ on the vector space ℝ3 ( fin 3 → ℝ ), which multiplies each component separately. After making the obvious generalization to an arbitrary type and index set, the easy way to write this down would be as follows, where again we can provide a stronger module α (ι → α) if we know α forms a semiring . instance function.has_scalar (ι α : Type*) [has_mul α] :
has_scalar α (ι → α) := { smul := λ r v, (λ i, r * v i) } This definition is perfectly fine for the action we wanted, but we can still generalize it much more. Consider now the action on matrices ι₁ → ι₂ → R by their coeficients R . We would like to show has_scalar R (ι₁ → ι₂ → R) , but that doesn’t match the function.has_scalar instance we just defined. While we could obviously define this operation trivially just as we did there, we would have to do so again if working with a vector of matrices or similar.
A better approach here is to exploit the chaining that occurs during typeclass search, and define our action as: instance function.has_scalar' (ι M α : Type*) [has_scalar M α] :
has_scalar M (ι → α) := { smul := λ r v, (λ i, r • v i) } This instance is strictly more general; typeclass search will recover our original has_scalar α (ι → α) instance by setting M = α and finding has_scalar α α from has_mul.to_has_scalar , but can also find the has_scalar R (ι₁ → ι₂ → R) we wanted by setting M = R and α = (ι₂ → R) , and finding has_scalar R (ι₂ → α) by recursive application of this instance. This approach is used extensively throughout mathlib, for actions on 1. sets and products defined in terms of actions on their elements 2. polynomials defined in terms of actions on their coeficients 3. bundled homomorphisms defined in terms of actions on their codomain Most of these actions propagate their axioms; for instance where we used [has_scalar M α] to implement has_scalar M (ι → α) , the stronger assumption of [module M α] would let us implement module M (ι → α) .
In section 3, the action we describe contains no proof obligations; we did not need to know any properties of [has_scalar M α] to define has_scalar M (ι → α) . Sometimes, the typeclasses in fig. 1 are enough to resolve this—for instance, while we can’t conclude has_scalar R (M →+ N) from [has_scalar R N] as we don’t know enough about this action to know if additive maps remain additive, we can conclude distrib_mul_action R (M →+ N) from [distrib_mul_action R N] .
Once we start working with types that themselves ingrain a preferred action though, we need some additional tools. For instance, the closely related types for R -linear maps M →ₗ[R] N and R -submodules submodule R N ingrain a preferred R -action. We can start by attempting to a general action by an arbitrary type α . If we do this we find ourselves left with two proof obligations, indicated by the show ..., from syntax. instance {α R M N : Type*} [semiring R] [add_comm_monoid M] [add_comm_monoid N] [has_scalar α N] [module R M] [module R N] : has_scalar α (M →ₗ[R] N) := { smul := λ a f, { to_fun := λ m, a • f m, map_add' := λ m₁ m₂, (congr_arg _ $ f.map_add _ _).trans $
show a • (f m₁ + f m₂) = a • f m₁ + a • f m₂, from sorry, map_smul' := λ r m, (congr_arg _ $ f.map_smul _ _).trans $
show a • r • f m = r • a • f m, from sorry } } The goal at the sorry in map_add' tells us we need to strengthen [has_scalar α N] to [monoid α] [distrib_mul_action α N] .
The goal in map_smul' is more troublesome. The easy way out is to replace α with a commutative R so our statement becomes instance {α M N : Type*} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] : has_scalar R (M →ₗ[R] N) := and the sorry can be closed with a • r • f m = (a * r) • f m = (r * a) • f m = r • a • f m which follows from the axioms of mul_action and commutativity of R . Another approach would be to require R to be an α -algebra [algebra α R] , and that the α -action on R and N is compatible with the R -action on N .
To best solve this problem, mathlib provides two additional typeclasses about scalar actions. The first expresses the compatibility condition we would need to use [algebra α R] as mentioned above, as class is_scalar_tower
(M N α : Type*) [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop :=
(smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • (y • z))
The name alludes to towers of algebras, which is described in more detail in [3,
Section 3.2]. Our particular problem can be solved more directly with the second typeclass,
[smul_comm_class α R N] , which expresses exactly the condition we require:
class smul_comm_class (M N α : Type*) [has_scalar M α] [has_scalar N α] : Prop :=
(smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a)
After this typeclass was introduced in [
The mathlib algebra R A describes an associative unital R -algebra over A given a comm_semiring R and semiring A . The definition is roughly class algebra (R A : Type*) [comm_semiring R] [semiring A] extends has_scalar R A := (algebra_map : R →+* A) (commutes : ∀ r x, algebra_map r * x = x * algebra_map r) (smul_def : ∀ r x, r • x = algebra_map r * x) which states that there is a canonical ring homomorphism from R to A which agrees with • and sends R to the center of A . This parameterization of the axioms is dificult to generalize to A being non-unital and non-associative ring. However, mathlib also provides this definition to construct an algebra from an alternate set of axioms: def algebra.of_module (R A : Type*) [comm_semiring R] [semiring A] [module R A] (h₁ : ∀ (r : R) (x y : A), (r • x) * y = r • (x * y)) (h₂ : ∀ (r : R) (x y : A), x * (r • y) = r • (x * y)) : algebra R A := sorry If we look carefully, we note that h₁ and h₂ closely resemble smul_assoc and smul_comm from section 3.1, but with some * s substituted for • . But if we look back to section 2.1, we remember that when x and y are the same type, x * y = x • y by definition! This means that h₁ and h₂ correspond directly with is_scalar_tower R A A and smul_comm_class R A A , respectively.
This is a valuable insight, because it allows us to use the follow sequences of typeclass arguments interchangeably: variables [comm_semiring R] [semiring A] [algebra R A] variables [comm_semiring R] [semiring A] [module R A]
[is_scalar_tower R A A] [smul_comm_class R A A]
Knowing this, it becomes immediately obvious how to generalize various statements to
nonunital algebras (which were needed in [
Frequently, there are multiple ways for Lean to construct a typeclass. For instance, consider the problem: example {ι A B} [add_comm_monoid A] [add_comm_monoid B] : module ℕ (ι → A →+ B) := by apply_instance Depending on the order of the search, Lean could take any of the paths in fig. 2. While Lean does not care about the existance of multiple paths and will happily just pick one, for the typeclass to be useful we need it to be predictable to the user; all they see is a • in the goal state. This means that whenever we have a diamond, we want all the paths to produce the same • such that the actual path taken does not matter.
add_comm_monoid B add_comm_monoid (A →+ B)
module ℕ B add_comm_monoid (ι → A →+ B)
module ℕ (A →+ B) module ℕ (ι → A →+ B)
There are two relevant notions of “same” here. The first is propositional equality, which for the case in fig. 2 can be stated as roughly ∀ (M : Type*) [add_comm_monoid M], subsingleton (module ℕ M) (that is that all ℕ -module structures are equal), and is straightforward to prove. This is enough to convince the user that the goal they’re looking at is mathematically the one they’re interested in. The second is definitional equality, which is needed by Lean in order to allow lemmas about one path for the tree in fig. 2 to apply for lemmas about another path.
In older versions of mathlib, the diamonds in fig. 2 resulted in paths creating instances that
were propositionally equal, but not definitionally equal. This was problematic, as lemmas
about the natural ℕ -action (blue path, fig. 2) such as ∑ x in s, c = s.card • c would fail to
match goals containing a derived ℕ -action (green and red paths, fig. 2). This was fixed in [
The scalar action typeclass in mathlib is intended for left-actions, which is apparent both in the definition of the mul_smul axiom, and in the order in which the arguments appear in the notation. However this does not mean that right actions are impossible.
The author has introduced preliminary support for right actions in [
Unfortunately, mathlib does not have typeclasses for another common interaction of right actions with left actions. Introducing briefly for clarity the notation a •> b for a • b and a <• b for op a • b , there is no typeclass capable of expressing (a <• b) •> c = a •> (b •> c) . Some examples of when this situation arises are [monoid M] (a b c : M) (all three variables belong to the same non-commutative monoid), [monoid M] (a c : M) (S : submonoid M) (b : S) (the second belongs to a submonoid of the monoid containing the other two), and [monoid M] (a b : M) (c : ι → M) (the third variable is a coordinate vector).
The future of right actions in mathlib might be improved by the eventual switch to Lean 4 [
While [
The author is supported by a scholarship from the Cambridge Trust.