# Additively-graded multiplicative action structures #

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure
over the sigma type `GradedMonoid A`

such that `(•) : A i → M j → M (i + j)`

; that is to say, `A`

has an additively-graded multiplicative action on `M`

. The typeclasses are:

With the `SigmaGraded`

locale open, these respectively imbue:

For now, these typeclasses are primarily used in the construction of `DirectSum.GModule.Module`

and
the rest of that file.

## Internally graded multiplicative actions #

In addition to the above typeclasses, in the most frequent case when `A`

is an indexed collection of
`SetLike`

subobjects (such as `AddSubmonoid`

s, `AddSubgroup`

s, or `Submodule`

s), this file
provides the `Prop`

typeclasses:

`SetLike.GradedSmul A M`

(which provides the obvious`GradedMonoid.GSmul A`

instance)

which provides the API lemma

`SetLike.graded_smul_mem_graded`

Note that there is no need for `SetLike.graded_mul_action`

or similar, as all the information it
would contain is already supplied by `GradedSmul`

when the objects within `A`

and `M`

have
a `MulAction`

instance.

## tags #

graded action

### Typeclasses #

A graded version of `Mul.toSMul`

- smul : {i j : ι} → A i → M j → M (i + j)
- one_smul : ∀ (b : GradedMonoid M), 1 • b = b
One is the neutral element for

`•`

- mul_smul : ∀ (a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b
Associativity of

`•`

and`*`

A graded version of `MulAction`

.

## Instances

The graded version of `Monoid.toMulAction`

.

### Shorthands for creating instance of the above typeclasses for collections of subobjects #

Internally graded version of `Mul.toSMul`

.