actions on hom spaces

Stream: maths

[Johan Commelin]

We have in https://github.com/leanprover-community/mathlib4/commit/d3038070bcab78ca09317951523576e264e9cf84

variable [Semiring R] [Semiring R₂]
variable [AddCommMonoid M] [AddCommMonoid M₂]
variable [Module R M] [Module R₂ M₂]
variable {σ₁₂ : R →+* R₂}
variable [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂]
variable [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂]

instance : SMul S (M →ₛₗ[σ₁₂] M₂) :=
  ⟨fun a f ↦
    { toFun := a • (f : M → M₂)
      map_add' := fun x y ↦ by simp only [Pi.smul_apply, f.map_add, smul_add]
      map_smul' := fun c x ↦ by simp [Pi.smul_apply, smul_comm] }⟩

but I'm a bit concerned. If S is not just a monoid, but actually a group, then it is also common to define

$$g \bullet f = \left(v \mapsto g \bullet (f (g^{-1} \bullet v))\right)$$

Which coincides propositionally with the existing instance, if the action on the domain M is trivial. But we seem to have a fork in the road here:

• on the one hand we want the existing instance in the generality of monoids
• on the other hand, the equation above is going to show up in representation theory, and probably elsewhere

[Eric Wieser]

I think we have very strongly gone down the line of "SMul always acts on the pieces", where "pieces" means "parts of a product", "coefficients of a polynomial", "codomain of a map", etc

[Johan Commelin]

I guess you mean "codomain of a map"?

[Eric Wieser]

Edited, thanks

[Johan Commelin]

But for maps, that is quite strongly breaking symmetry :sad:

[Eric Wieser]

Symmetry with what?

[Eric Wieser]

Maybe a simpler description of the rule is "SMul commutes with the projections" (eg docs#Prod.smul_fst, docs#LinearMap.coe_smul, docs#Pi.smul_apply, etc)

[Eric Wieser]

This is a good idea because + almost always behaves in the same way, and so we don't end up with asymmetry between scaling and addition in a module

[Richard Hill]

Johan's suggestion agrees with the action in Rep.ihom, although this is not a SMul action.

[Johan Commelin]

This is already an issue with group actions. If we have $G$ acting on $X$ and $Y$, then you get an action on $X \to Y$, but it is not the one that is in Mathlib.

I'm starting to think that we should pull apart SMul and Act (the latter does not exist yet).

[Kevin Buzzard]

Yeah we have now run into the situation where we want two G-actions on X -> Ydepending on whether X has a G-action or not. The advantage of $(gf)(x):=g(f(g^{-1}x)))$ is that then the G-equivariant homs are precisely the $G$-fixed points.

Do we have $G$-action on a tensor product of $G$-modules? Here we surely want $g(x\otimes y)=gx\otimes gy$ (modules over a ring, tensor product over the same ring). In fact the canonial map $V^*\otimes_RW\to Hom_R(V,W)$ (here $G$ is acting on $V$ and $W$ $R$-linearly) presumably won't be equivariant for mathlib's conventions, because the group surely acts diagonally on the tensor product but will act only on the target in the hom set.

[Johan Commelin]

Luckily, $G$ acts trivially on $V^*$ because that is $\text{Hom}(V, K)$... :see_no_evil:

[Eric Wieser]

Johan Commelin said:

I'm starting to think that we should pull apart SMul and Act (the latter does not exist yet).

This certainly solves problems relating to interactions with SMul, but I suspect the intended behavior is still quite hard to specify. To me it sounds very diamond prone.

[Eric Wieser]

In my thesis I outlined a possible alternative for being very precise about how any given action acts

[Yaël Dillies]

In that case, can we create a new type synonym DomConjAct or something like that, and put the action on it instead of o' G itself

[Eric Wieser]

Ultimately this falls apart too unless we also make the standard SMul action need a type synonym

[Eric Wieser]

But indeed we already have a set of (likely diamond creating) type synonyms that create the actions Johan describes

[Antoine Chambert-Loir]

Johan Commelin said:

This is already an issue with group actions. If we have $G$ acting on $X$ and $Y$, then you get an action on $X \to Y$, but it is not the one that is in Mathlib.

I'm starting to think that we should pull apart SMul and Act (the latter does not exist yet).

You have three actions on $X\to Y$ (of course, you know that), the action on the target and the action on the source, and since they commute, you can combine them to Kevin's action.

[Junyan Xu]

I'm inclined to introduce a type synonyms called AsGroupRep X. When X is V →ₗ[R] W you can introduce the desired G-action on AsGroupRep (V →ₗ[R] W), for example.

[Antoine Chambert-Loir]

The question is how one would formulate the above sentence, that Kevin's action is the combination of the left and right commuting actions on $X \to Y$?

[Antoine Chambert-Loir]

Should the type synonym machinery be used for the group that acts, or the things that are acted upon?

[Anatole Dedecker]

From a mathematical/categorical point of view, I think the answer is clearly "the thing which is acted upon": each type synonym will then correspond to one object in the category of representations of G.

Of course practicality is more important, so maybe putting the type alias on the group side (which is what we currently do) is better.

But really I believe the long term solution might be allowing naming actions.

[Anatole Dedecker]

(Note that, for example, docs#Flow is essentially a domain-specific version of named actions)

[Yaël Dillies]

Is representation theory to docs#SMul the same as what a filtration is to docs#MeasurableSpace ?

[Yaël Dillies]

It would be a sweeping change to make mathlib compatible, but it would certainly be doable if well-motivated

[Eric Wieser]

But really I believe the long term solution might be allowing naming actions.

This is one of the things I briefly discuss in my thesis:

A possible redesign of the SMul typeclass could be

def SMul.Discr := Type class SMul (M : Type*) (α : Type*) (discr : SMul.Discr) where
  smul : M → α → α
notation3:72 a:72 " •[" discr "] " b:72 => @SMul.smul _ _ discr _ a b

where the discr parameter acts as a discriminator to implement “tag dispatching” (to borrow the term from C++) and contains information relevant only at typeclass-search-time about _which_ action to use; information that was previously tracked by attaching it to type synonyms wrapping M and α.
[...]
With this infrastructure in place, the diamonds in fig. 4.7 are avoided by forcing the user to spell which action they want:

variable {G H} (discr) [SMul G H discr] (g : G) (f : H → H → H) (a b : H)
example : (g •[discr.domAct] f) a b = f (g •[discr] a) b := rfl
example : (g •[discr.domAct.codAct] f) a b = f a (g •[discr] b) := rfl

This strategy is not without its downsides. It makes cases where the typeclass diamonds do commute (such as fig. 4.3) more awkward to work with, requiring an additional compatibility typeclass that states that two discriminators describe the same action; Additionally, bundled linear maps would now need to take two extra arguments to specify the discriminator for their source and domain. Determining whether these trade-offs are acceptable would require an attempt at refactoring large pieces of mathlib, which the author will leave to a particularly interested reader.

[Anatole Dedecker]

Yaël Dillies said:

Is representation theory to docs#SMul the same as what a filtration is to docs#MeasurableSpace ?

I'm not sure I get the comparison. In representation theory, you also change the underlying vector space a lot, but there are definitely some spaces where it would be nice being able to write down the action. A typical example is Fell's absorption principle, which says that if $\lambda$ is the left-regular representation of a discrete group $\Gamma$, and $\pi : \Gamma \curvearrowright \mathcal{H}$ is any unitary representaton, then the tensor product $\lambda\otimes\pi$ is unitarily equivalent to $\lambda\otimes 1_{\mathcal{H}}$, where $1_{\mathcal{H}}$ is the trivial representation on $\mathcal{H}$. Note that these two are naturally representations on the same Hilbert space, although of course we could make type aliases.

[Anatole Dedecker]

Oh but maybe what you meant is that the group shouldn't change ? If so, yes that is the case. I don't think we want all of our morphisms of representations to be equivariant over a map between type aliases of the group.

[Anatole Dedecker]

Thanks for the pointer Eric! Is there any reason we couldn't have a "canonical" discriminator which would give us the current behaviour with the usual notations?

[Eric Wieser]

In practice almost every theorem about SMul would take a discriminator as a free variable, rather than using a canonical one.

[Eric Wieser]

"if X acts on Y with discriminator discr, then F X acts on F Y with disciminator discr.f", etc

[Anatole Dedecker]

Ah yes sure, otherwise it won't be applicable. So this doesn't bring much except for downstream projects maybe.

[Scott Carnahan]

If monoids G and H act on X and Y respectively, then we get a canonical action of Gᵒᵖ × H on X → Y, and the H-action on the target is the only H-action guaranteed to exist. However, if G is a group and G = H, then the choice of homomorphism G →* Gᵒᵖ × G is no longer canonical.

Is it reasonable to make the various possible SMul instances scoped in a way that makes them unlikely to collide, e.g., we have to open DiagonalActionOnHom to get the diagonal?

[Lenny Taelman]

This is perhaps only tangentially related, but wouldn't it be much cleaner to have explicit notations of Left, Right, and Bi-actions? With instances such that e.g. a right action on X induces a left action on X → Y, or left actions on X and Y inducing a bi-action on X → Y?

I had been thinking a bit about this in terms of tensor products and Homs between modules over non-commutative rings. I would love to be able to write bi-actions in their natural notation (with the acting operators written on the right and left), rather than via an action of Gᵒᵖ × H.

So as a user, I would love to be able to do sth like:

variable (G H X Y : Type) [Monoid G] [Monoid H] [LMulAction G X] [LMulAction H Y]
#synth RMulAction G (X → Y)
#synth LMulAction H (X → Y)
#synth BiMulAction H G (X → Y)

variable (s : G) (t : H) (x : X) (f : X → Y)
example : (t • f • s) x = t • (f ( s • x )) := rfl

"Commuting" symbols unnecessary is in my experience opinion bad practice (at least informally...).

[Michael Stoll]

See perhaps also #mathlib4 > Too many 'Smul's @ 💬

[Eric Wieser]

Lenny, unfortunately that isn't enough, because you need to distinguish (left actions arising from a left action) from (left actions arising from a right action)

[Lenny Taelman]

Eric Wieser said:

Lenny, unfortunately that isn't enough, because you need to distinguish (left actions arising from a left action) from (left actions arising from a right action)

Meaning e.g. a left action of Gᵒᵖ coming from a right action of G? Not quite sure I understand the point (although I can see there may be many many conflicting actions around in some situations)...

[Eric Wieser]

An example I'm thinking of is distinguishing the four actions on the domain / codomain of a map corresponding to left / right actions on those parts

[Lenny Taelman]

Absolutely. I would love to have sth like...

instance [LMulAction G X] : RMulAction G X → Y := sorry
instance [RMulAction G X] : LMulAction G X → Y := sorry
instance [LMulAction G Y] : LMulAction G X → Y := sorry
instance [RMulAction G Y] : RMulAction G X → Y := sorry

I'm sure this would lead to many conflicts, but mathematically it feels like these are more fundamental then the various (possibly conflicting) less canonical variations...

[Kevin Buzzard]

[RMulAction G X] is spelt [MulAction G^{op} X] right?