Eric Wieser
Cambridge University Engineering Department
has_scalar
typeclass in Mathlib, and difficulties arising around compatibility of actions and around instance diamonds.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 }
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)
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 }
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 α α :=
{ zero_sfmul := zero_mul, add_smul := add_mul,
smul_zero := mul_zero, smul_add := mul_add }
Another simple action, assuming [add_comm_monoid α]
:
(3 : ℕ) • a = a + a + a
def repeated_add [add_comm_monoid α] : ℕ → α → α
 0 a := 0
 (n + 1) a := a + repeated_add n a
instance nat_scalar [add_comm_monoid α] : has_scalar ℕ α :=
{ smul := repeated_add }
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*}
[semiring R] [add_comm_monoid M] [add_comm_group N]
[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
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]
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 α]
, …
has_scalar M (ι → α)
was easy. has_scalar α (M →ₗ[R] N)
is harder.
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 } }
Now we have proof fields to fill out.
instance {α R M N : Type*}
[semiring R] [add_comm_monoid M] [add_comm_monoid N]
[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*}
[semiring R] [add_comm_monoid M] [add_comm_monoid N]
[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*}
[semiring R] [add_comm_monoid M] [add_comm_monoid N]
[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
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
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))
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
!
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
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
.
What does •
in the following mean?
variables (R : Type*) {ι A B : Type*}
variables [add_comm_monoid A] [add_comm_monoid B]
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
?
double_nat
, double_any ℕ
subsingleton (module ℕ α)
•
in the goal is one they meant.•
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)
Left  Right 

(m₁ * m₂) • a = m₁ • m₂ • a a • b = a * b

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

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 }
has_scalar (opposite α) α
instances.
Bimodule 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 subbimodules, twosided ideals, …
No current typeclass: (a <• b) • c = a • (b •> c)
Needed for (a b c : α)
, {S : submonoid α} (a c : α) (b : S)
, (a b : α) (c : ι → α)
, …
has_mul.mul : α → α → α
to HMul.hMul : α → β → γ
•
→ *
has_scalar R M
→ HMul R M M
has_scalar (opposite R) M
→ HMul M R M
is_scalar_tower R S M
→ HMulAssoc R S M
smul_comm_class R S M
→ HMulLeftComm R S M
Non definitionallyequal diamonds remain in the algebra_map
fields of:
Diamond instance  algebra ℕ R 
algebra ℤ R 
algebra ℚ R 

Possible solution  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₂)⁻¹
.More about mathlib:
leanprovercommunity.github.io
Slides for this presentation:
ericwieser.github.io/fmm2021