An algebra representation as a module over scalars?

Stream: mathlib4

[Kalle Kytölä]

If $V$ is a representation of a $\mathbb{K}$-algebra $A$, then for any $a \in A$, the map $v \mapsto a \cdot v$ is a $\mathbb{K}$-linear map --- in math. How about in Mathlib?

[Kalle Kytölä]

First for comparison something that works in Mathlib. If I have commuting (SMulCommClass) module actions of two (semi)rings on a space, then I can at least state (and prove) the linearity over one ring of SMul by the other ring.

import Mathlib.Algebra.Algebra.Defs
import Mathlib.GroupTheory.GroupAction.Ring
import Mathlib.LinearAlgebra.Span.Defs

variable (R S : Type*) [Semiring R] [Semiring S]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M]

/-- Works. (Generalizes `IsLinearMap.isLinearMap_smul`, but I did not find this in Mathlib.) -/
lemma IsLinearMap.isLinearMap_smul_of_smulCommClass (s : S) :
    IsLinearMap R (fun (v : M) ↦ s • v) :=
  ⟨fun m n ↦ by simp, fun r m ↦ (smul_comm r s m).symm⟩

[Kalle Kytölä]

The issue I am facing is that I cannot even make an algebra representation a module over the scalars!

docs#algebraMap does provide a way to see scalars as a part of the algebra and one can use this to define moduleScalarOfModule below, but I cannot make it an instance ("cannot find synthesization order"). What am I doing wrong? What is the intended solution?

import Mathlib.Algebra.Algebra.Defs
import Mathlib.GroupTheory.GroupAction.Ring
import Mathlib.LinearAlgebra.Span.Defs

variable (𝕜 : Type*) [CommRing 𝕜]
variable (A : Type*) [Semiring A] [Algebra 𝕜 A]
variable (V : Type*) [AddCommMonoid V] [Module A V]

/-- Any module over an algebra is a module over the scalars. -/
def moduleScalarOfModule :
    Module 𝕜 V where
  smul c v := (algebraMap 𝕜 A c) • v
  one_smul v := by
    change (algebraMap 𝕜 A 1) • v = v
    simp
  mul_smul c₁ c₂ v := by
    change (algebraMap 𝕜 A (c₁ * c₂)) • v = (algebraMap 𝕜 A c₁) • (algebraMap 𝕜 A c₂ • v)
    simp [← mul_smul]
  smul_zero c := by
    change (algebraMap 𝕜 A c) • (0 : V) = 0
    simp
  smul_add c v₁ v₂ := by
    change (algebraMap 𝕜 A c) • (v₁ + v₂) = (algebraMap 𝕜 A c) • v₁ + (algebraMap 𝕜 A c) • v₂
    simp
  add_smul c₁ c₂ v := by
    change (algebraMap 𝕜 A (c₁ + c₂)) • v = (algebraMap 𝕜 A c₁) • v + (algebraMap 𝕜 A c₂) • v
    simp [add_smul]
  zero_smul v := by
    change (algebraMap 𝕜 A 0) • v = 0
    simp

instance instSMulOfAlgebraOfModule :
    SMul 𝕜 V where
  smul c v := (algebraMap 𝕜 A c) • v
/- *Error message:*
cannot find synthesization order for instance instSMulOfAlgebraOfModule with type
  (𝕜 : Type u_1) →
    [inst : CommRing 𝕜] →
      (A : Type u_2) →
        [inst_1 : Semiring A] → [Algebra 𝕜 A] → (V : Type u_3) → [inst : AddCommMonoid V] → [Module A V] → SMul 𝕜 V
all remaining arguments have metavariables:
  Semiring ?A
  @Algebra 𝕜 ?A CommRing.toCommSemiring ?inst✝
  @Module ?A V ?inst✝ inst✝¹
-/

[Kalle Kytölä]

Why do I want the above instance?

• to be able to state that action of algebra elements is linear over scalars
• to be able to use linearity results of the action of algebra elements
• palatable notation for scalar multiplication (without algebraMap inserted every time you want scalar multiples)
• to be able to talk about both vector subspaces (Subodule 𝕜 V) and subrepresentations (Submodule A V) of a representation V (Module A V) over a noncommutative 𝕜-algebra A
  • I have admittedly picked the design choice "representation of an algebra = module over the algebra", which might not be the only one or the optimal spelling for group representations, but the case for this spelling is stronger with algebra representations

[Kenny Lau]

@Kalle Kytölä The canonical spelling is [Module k V] [Module A V] [IsScalarTower k A V]

[Eric Wieser]

Note that your code can be golfed to

def moduleScalarOfModule : Module 𝕜 V := Module.compHom _ (algebraMap 𝕜 A)

[Kalle Kytölä]

Thanks a lot!

I think it just feels funny to essentially assume that a module over a $\mathbb{K}$-algebra has a compatible $\mathbb{K}$ action (in the hypotheses [Module k V] [IsScalarTower k A V]), although this action could very well just be constructed from the already existing data (which I thought the type class system could be made to do automatically, but the "cannot find synthesization order" prevents this) and I sure hope this is the unique $\mathbb{K}$-module structure one would ever have on the $A$-module.

But I believe the canonical solution will work. (I guess at least for unital algebras it follows from the canonically spelled hypotheses that the assumed action must be what one would construct it to be.) Thanks!

[Kenny Lau]

this is just part of the lean/mathlib philosophy when you use classes

[Kenny Lau]

because of diamonds

[Kalle Kytölä]

Yes. And I must say that I really like the IsScalarTower design. (Just that I naively hoped that one of the two Module instances and their joint IsScalarTower instance could have been synthesized and not assumed in the algebra representation case.)

[Kenny Lau]

they can, we've explicitly disabled that to avoid diamonds

[Kenny Lau]

it's a design choice

[Kenny Lau]

Kenny Lau said:

they can, we've explicitly disabled that to avoid diamonds

(they also kind of can't, you're asking for an instance of Module k V to be derived from an instance of Module A V and Algebra k A, which is a dangerous instance

[Kenny Lau]

remember that Lean makes instances backwards from how mathematicians think

[Kenny Lau]

this is also why the canonical spelling is [AddCommMonoid M] [Module R M] rather than the Module just subsuming the AddCommMonoid

[Kenny Lau]

because an instance Module R M -> AddCommMonoid M is a dangerous decreasing instance rule

[Kalle Kytölä]

I think I can imagine some ways the instance search could go really badly. But is this explained somewhere in detail if I'd like to study and get a better understanding of what is dangerous and what is not?

[Kenny Lau]

@Kalle Kytölä basically it's dangerous because now every time Lean wants to search for AddCommMonoid M, Lean has to invent some R and check that there's an instance of Module R M. In other words, the R cannot be inferred from the goal.

[Kenny Lau]

Lean basically always only starts from the goal and apply instance inferring rules