Representation.apply_eq_self
theorem Representation.apply_eq_self :
∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G]
[inst_2 : AddCommMonoid V] [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (x : V) [h : ρ.IsTrivial],
(ρ g) x = x
The `Representation.apply_eq_self` theorem states that for any types `k`, `G`, and `V`, where `k` is a commutative semiring, `G` is a monoid, `V` is an additive commutative monoid and a `k`-module, and given a representation `ρ` of `G` on the `k`-module `V` and any element `g` from `G` and `x` from `V`, if `ρ` is a trivial representation (i.e., every group element is represented by the identity on `V`), then the result of applying the group element `g` to `x` via the representation `ρ` is equal to `x` itself. This theorem essentially says that in a trivial representation, the action of any group element leaves every vector in the `V` space unchanged.
More concisely: In a trivial representation of a monoid `G` on an additive commutative `k`-module `V`, where `k` is a commutative semiring, the action of any group element `g` on any vector `x` in `V` is equal to `x`.
|
Representation.asAlgebraHom_single
theorem Representation.asAlgebraHom_single :
∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G]
[inst_2 : AddCommMonoid V] [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (r : k),
(ρ.asAlgebraHom fun₀ | g => r) = r • ρ g
The theorem `Representation.asAlgebraHom_single` states that for any commutative semiring `k`, monoid `G`, and additively commutative monoid `V` that forms a `k`-module, and for any representation `ρ` of `G` on `V` over `k`, and any element `g` of `G` and `r` of `k`, applying the algebra homomorphism corresponding to the representation `ρ` to the monoid algebra element that maps `g` to `r` (and everything else to zero) results in the same as scaling the linear transformation corresponding to `g` under the representation `ρ` by `r`. In terms of linear algebra, this is asserting an interaction between the scalar multiplication in the module and the action of the group on the module via the representation.
More concisely: For any commutative semiring `k`, monoid `G`, additively commutative `k`-module `V`, representation `ρ` of `G` on `V`, and `g` in `G` and `r` in `k`, the algebra homomorphism `ρ` applied to the monoid algebra element `r * ∑ (x : G) (ρ(x) * x)` equals the scalar multiplication `r * (ρ(g))` in `V` where `ρ(g)` is the linear transformation corresponding to `g` under the representation `ρ`.
|
Representation.dualTensorHom_comm
theorem Representation.dualTensorHom_comm :
∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring k] [inst_1 : Group G]
[inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
(ρV : Representation k G V) (ρW : Representation k G W) (g : G),
dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W
The theorem `Representation.dualTensorHom_comm` states that given commutative semiring `k`, a group `G`, and `k`-modules `V` and `W`, if we have representations of `G` on `V` and `W` (denoted `ρV` and `ρW` respectively), and an element `g` from `G`, then the composition of the function `dualTensorHom` (which maps the tensor product of the dual of `V` and `W` to the set of `k`-linear maps from `V` to `W`) with the tensor product of the dual of the representation of `g` on `V` and the representation of `g` on `W` is equal to the composition of the `k`-linear map induced by the action of `g` on the tensor product of `V` and `W` and the `dualTensorHom` function. In simpler words, this theorem claims that the `dualTensorHom` function is `G`-linear, i.e., it preserves the action of `G`.
More concisely: Given commutative semirings `k`, groups `G`, and `k`-modules `V` and `W` with representations `ρV` and `ρW`, the composition of `dualTensorHom` with the tensor product of `ρV(g)`, `ρW(g)`, and the identity maps is equal to the `k`-linear map induced by the action of `g` on the tensor product of `V` and `W` when applying `dualTensorHom`.
|