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.