Monoid representations #
This file introduces monoid representations and their characters and defines a few ways to construct representations.
Main definitions #
- Representation.Representation
- Representation.character
- Representation.tprod
- Representation.linHom
- Representation.dual
Implementation notes #
Representations of a monoid G
on a k
-module V
are implemented as
homomorphisms G →* (V →ₗ[k] V)
.
A representation of G
on the k
-module V
is a homomorphism G →* (V →ₗ[k] V)
.
Instances For
The trivial representation of G
on a k
-module V.
Instances For
A k
-linear representation of G
on V
can be thought of as
an algebra map from MonoidAlgebra k G
into the k
-linear endomorphisms of V
.
Instances For
If ρ : Representation k G V
, then ρ.asModule
is a type synonym for V
,
which we equip with an instance Module (MonoidAlgebra k G) ρ.asModule
.
You should use asModuleEquiv : ρ.asModule ≃+ V
to translate terms.
Instances For
A k
-linear representation of G
on V
can be thought of as
a module over MonoidAlgebra k G
.
The additive equivalence from the Module (MonoidAlgebra k G)
to the original vector space
of the representative.
This is just the identity, but it is helpful for typechecking and keeping track of instances.
Instances For
Build a Representation k G M
from a [Module (MonoidAlgebra k G) M]
.
This version is not always what we want, as it relies on an existing [Module k M]
instance, along with a [IsScalarTower k (MonoidAlgebra k G) M]
instance.
We remedy this below in ofModule
(with the tradeoff that the representation is defined
only on a type synonym of the original module.)
Instances For
Build a Representation
from a [Module (MonoidAlgebra k G) M]
.
Note that the representation is built on restrictScalars k (MonoidAlgebra k G) M
,
rather than on M
itself.
Instances For
ofModule
and asModule
are inverses. #
This requires a little care in both directions: this is a categorical equivalence, not an isomorphism.
See Rep.equivalenceModuleMonoidAlgebra
for the full statement.
Starting with ρ : Representation k G V
, converting to a module and back again
we have a Representation k G (restrictScalars k (MonoidAlgebra k G) ρ.asModule)
.
To compare these, we use the composition of restrictScalarsAddEquiv
and ρ.asModuleEquiv
.
Similarly, starting with Module (MonoidAlgebra k G) M
,
after we convert to a representation and back to a module,
we have Module (MonoidAlgebra k G) (restrictScalars k (MonoidAlgebra k G) M)
.
A G
-action on H
induces a representation G →* End(k[H])
in the natural way.
Instances For
If we equip k[G]
with the k
-linear G
-representation induced by the left regular action of
G
on itself, the resulting object is isomorphic as a k[G]
-module to k[G]
with its natural
k[G]
-module structure.
Instances For
When G
is a group, a k
-linear representation of G
on V
can be thought of as
a group homomorphism from G
into the invertible k
-linear endomorphisms of V
.
Instances For
Given representations of G
on V
and W
, there is a natural representation of G
on their
tensor product V ⊗[k] W
.
Instances For
Given representations of G
on V
and W
, there is a natural representation of G
on the
module V →ₗ[k] W
, where G
acts by conjugation.
Instances For
The dual of a representation ρ
of G
on a module V
, given by (dual ρ) g f = f ∘ₗ (ρ g⁻¹)
,
where f : Module.Dual k V
.
Instances For
Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$
(implemented by LinearAlgebra.Contraction.dualTensorHom
).
Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on
$Hom_k(V, W)$.
This lemma says that $φ$ is $G$-linear.