# Scalar actions in Lean's mathlib

Eric Wieser
Cambridge University Engineering Department

slides: eric-wieser.github.io/fmm-2021 2021-07-31

## Introduction

Lean 3*
A dependently-typed language suitable for theorem proving
Mathlib
A coherent library of formalized mathematics for Lean 3, assembled via an ongoing collaborative effort from over 170 contributors across disciplines.
This presentation
A case study in the use of the has_scalar typeclass in Mathlib, and difficulties arising around compatibility of actions and around instance diamonds.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von RaumerThe Lean Theorem Prover (System Description) The mathlib CommunityThe Lean Mathematical Library

### IntroductionWhat are typeclasses?

Declaration with class


class has_mul (G : Type*) := (mul : G → G → G)  -- in Lean

infix * := has_mul.mul


class semigroup (G : Type*) extends has_mul G :=  -- in Mathlib
(mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))


Usage with […]


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]


Instantiation with instance


instance (α : Type*) : semigroup (list α) :=
{ mul := list.append,  -- list.append [a, b] [c, d] = [a, b, c, d]
mul_assoc := list.append_assoc }


### IntroductionWhat are scalar actions?

The has_scalar typeclass:

class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α)

infixr  • :73 := has_scalar.smul

Notation: m • a₁ = a₂.

class mul_action (M : Type*) (α : Type*) [monoid M]
extends has_scalar M α :=
(one_smul : ∀ a : α, (1 : M) • a = a)
(mul_smul : ∀ (m₁ m₂ : M) (a : α), (m₁ * m₂) • a = m₁ • m₂ • a)


## Elementary actions

### Elementary actions Left-multiplication

A simple action: a • b = a * b

variables {α : Type*}

instance has_mul.to_has_scalar [has_mul α] :
has_scalar α α := { smul := (*) }


Stronger versions


instance monoid.to_mul_action [monoid α] :
mul_action α α :=
{ one_smul := one_mul, mul_smul := mul_assoc }


### Elementary actions Left-multiplication

Stronger versions

instance has_mul.to_has_scalar [has_mul α] :
has_scalar α α := { smul := (*) }


instance monoid.to_mul_action [monoid α] :
mul_action α α :=
{ one_smul := one_mul, mul_smul := mul_assoc }


instance semiring.to_module [semiring α] :
module α α :=


Another simple action, assuming [add_comm_monoid α]:

(3 : ℕ) • a = a + a + a

| 0 a := 0
| (n + 1) a := a + repeated_add n a

instance nat_scalar [add_comm_monoid α] : has_scalar ℕ α :=


instance nat_module [add_comm_monoid α] : module ℕ α := sorry
instance nat_algebra [semiring α] : algebra ℕ α := sorry


Similarly given [add_comm_group α] / [ring α]:

(-3 : ℤ) • a = -(a + a + a)

Example uses in mathlib:


/-- The sum of a constant is a repeated addition. -/
@[simp] theorem finset.sum_const {β α : Type*} [add_comm_monoid β]
{s : finset α} (b : β) :
∑ x in s, b = s.card • b := sorry


/-- An ordered additive commutative monoid is called archimedean
if for any two elements x, y such that 0 < y there exists a
natural number n such that x ≤ n • y. -/
class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
(arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)


/-- Permuting the arguments of an alternating map scales the
result by the sign of the permutation. -/
theorem alternating_map.map_perm {R M N' ι : Type*}
[module R M] [module R N] [decidable_eq ι] [fintype ι]
(g : alternating_map R M N ι) (v : ι → M) (σ : equiv.perm ι) :
g (v ∘ σ) = (σ.sign : ℤ) • g v := sorry


### Elementary actions Elementwise multiplication

The $\mathbb{R}$-module structure on $\mathbb{R}^3$ (fin 3 → ℝ), $r \left[\begin{smallmatrix}x\mathstrut \\ y\mathstrut \\ z\mathstrut\end{smallmatrix}\right] = \left[\begin{smallmatrix}rx\mathstrut \\ ry\mathstrut \\ rz\mathstrut\end{smallmatrix}\right]$:

r • ![x, y, z] = ![r * x, r * y, r * z]

instance function.has_scalar (ι α : Type*) [has_mul α] :
has_scalar α (ι → α) :=
{ smul := λ r v, (λ i, r * v i) }


The {$\mathbb{R}$, $\mathbb{R}_{\ge 0}$, $\mathbb{Q}$, …}-module structures on $\mathbb{R}^3$:

r • ![x, y, z] = ![r • x, r • y, r • z]

## Derived actions

### Derived actions Elementwise multiplication

The $\mathbb{R}$-module structure on $\mathbb{R}^3$ (fin 3 → ℝ), $r \left[\begin{smallmatrix}x\mathstrut \\ y\mathstrut \\ z\mathstrut\end{smallmatrix}\right] = \left[\begin{smallmatrix}rx\mathstrut \\ ry\mathstrut \\ rz\mathstrut\end{smallmatrix}\right]$:

r • ![x, y, z] = ![r * x, r * y, r * z]

instance function.has_scalar (ι α : Type*) [has_mul α] :
has_scalar α (ι → α) :=
{ smul := λ r v, (λ i, r * v i) }


The {$\mathbb{R}$, $\mathbb{R}_{\ge 0}$, $\mathbb{Q}$, …}-module structures on $\mathbb{R}^3$:

r • ![x, y, z] = ![r • x, r • y, r • z]

instance function.has_scalar' (ι M α : Type*) [has_scalar M α] :
has_scalar M (ι → α) :=
{smul := λ r v, (λ i, r • v i) }


Repeat for [mul_action M α], [module M α], …

### Derived actions Compatibility constraints

has_scalar M (ι → α) was easy. has_scalar α (M →ₗ[R] N) is harder.


instance {α R M N : Type*}
[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 } }

Now we have proof fields to fill out.

instance {α R M N : Type*}
[module α 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$
smul_add a (f m₁) (f m₂),
map_smul' := λ r m, (congr_arg _ $f.map_smul _ _).trans$
show a • r • f m = r • a • f m, from sorry } }

Strengthening [has_scalar α N] to [module α N] closes the map_add' goal.

instance {α R M N : Type*}
[module α 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$
smul_add a (f m₁) (f m₂),
map_smul' := λ r m, (congr_arg _ $f.map_smul _ _).trans$
show a • r • f m = r • a • f m, from sorry } }

Strengthening our existing assumptions doesn't help here.

instance {α R M N : Type*}
[module α N] [module R M] [module R N] [smul_comm_class α 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$
smul_add a (f m₁) (f m₂),
map_smul' := λ r m, (congr_arg _ $f.map_smul _ _).trans$
smul_comm a r (f m) } }

We need a new typeclass:

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)

Yury Kudryashovmathlib PR #4770: introduce smul_comm_class

### Derived actions Compatibility constraints


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)


Another similar typeclass:


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))


For example:


-- the action of ℝ on ℂ³ factors through the action of ℂ on ℂ³
instance : is_scalar_tower ℝ ℂ (fin 3 → ℂ) := by apply_instance


Valuable for working with field extensions*.

Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. NuccioA formalization of Dedekind domains and class groups of global fields

## Algebras


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))


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))

One way to construct an algebra instance in mathlib:

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


x * y = x • y, so h₁ is is_scalar_tower R A A, and h₂ is smul_comm_class R A A!

## Algebras


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


x * y = x • y, so h₁ is is_scalar_tower R A A, and h₂ is smul_comm_class R A A!

Relaxing requirements of algebras:


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]


An equivalent choice to above


variables
[comm_semiring R] [non_unital_non_assoc_semiring A] [module R A]
[is_scalar_tower R A A] [smul_comm_class R A A]


Useful* when A behaves as a Lie algebra

Oliver Nash mathlib PR #7932: adjointness for the functor G ↦ monoid algebra k G when G carries only has_mul

variables
[comm_semiring R] [semiring A] [module R A]
[is_scalar_tower R A A] [smul_comm_class R A A]


An equivalent choice to above


variables
[monoid R] [semiring A] [distrib_mul_action R A]
[is_scalar_tower R A A] [smul_comm_class R A A]


Useful for actions by units, when R = units S.

Kexing Ying mathlib PR #7416: complex version of Sylvester’s law of inertia

## Diamonds

### Diamonds How typeclass diamonds originate

What does • in the following mean?


variables (R : Type*) {ι A B : Type*}
def double_nat (f : ι → A →+ B) := (2 : ℕ) • f


variables [semiring R] [module R B]
def double_any (f : ι → A →+ B) := (2 : R) • f

Is double_any ℕ = double_nat?
Paths taken: double_nat, double_any ℕ

### DiamondsTypes of equality

• Propositional
• All $\mathbb{N}$-module structures must be equal, subsingleton (module ℕ α)
• Sufficient to satisfy the user that a • in the goal is one they meant.
• Definitional
• Sufficient to satisfy Lean that a • in the goal is the • in other lemmas.

double_any ℕ = double_nat: propositional ✔, definitional ✘

Controlling definitional equality:*


class add_comm_monoid (M : Type*) :=
(zero : M) (add : M → M → M)
(nsmul : ℕ → M → M)  -- mathematically redundant
(various_monoid_axioms : sorry)

Sébastien Gouëzelmathlib PR #7084: kill nat multiplication diamonds

## Future work

### Future workRight actions

LeftRight
(m₁ * m₂) • a = m₁ • m₂ • a
a • b = a * b
a <• (m₁ * m₂) = a <• m₁ <• m₂
a <• b = b * a
Requirements and examples of actions

Choose op a • b = b <• a such that:

 (op m₂ * op m₁) • a = op m₂ • op m₁ • a  a <• (m₁ * m₂) = a <• m₁ <• m₂ 

instance op_mul_action [monoid α] : mul_action (opposite α) α :=
{ smul := λ oa b, b * unop oa,  -- as opposed to a * b
one_smul := mul_one,
mul_smul := λ oa ob r, (mul_assoc _ _ _).symm }

Eric Wiesermathlib PR #7630: add has_scalar (opposite α) α instances.

### Future workCompatibility of right actions

Bi-module require:

r • (m <• s) = (r • m) <• s

r • (op s • m) = op s • (r • m)

Lean assumptions:


variables [module R M] [module (opposite S) M]
[smul_comm_class R (opposite S) M]


Enables work on sub-bimodules, two-sided ideals, …

No current typeclass: (a <• b) • c = a • (b •> c)
Needed for (a b c : α), {S : submonoid α} (a c : α) (b : S), (a b : α) (c : ι → α), …

### Future workScalar actions in Lean 4

• Lean 4* generalizes has_mul.mul : α → α → α to HMul.hMul : α → β → γ
• Possible replacements:
• notation: •*
• left actions: has_scalar R MHMul R M M
• right actions: has_scalar (opposite R) MHMul M R M
• compatibility: is_scalar_tower R S MHMulAssoc R S M
• compatibility: smul_comm_class R S MHMulLeftComm R S M
• It's likely best to wait for an initial port of Mathlib to Lean 4 before attempting this.
Leonardo de Moura and Sebastian UllrichThe lean 4 theorem prover and programming language

### Future workMore diamonds

Non definitionally-equal diamonds remain in the algebra_map fields of:

Diamond instance Possible solution algebra ℕ R algebra ℤ R algebra ℚ R semiring.of_nat ring.of_int division_ring.of_rat (and corresponding proof fields)

A recently discovered diamond:

Agrees definitionally on ↑(u₁ • u₂) but not ↑(u₁ • u₂)⁻¹.
can be corrected with right actions!