GroupAlgebra.mul_average_left
theorem GroupAlgebra.mul_average_left :
∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G]
[inst_3 : Invertible ↑(Fintype.card G)] (g : G),
(fun₀ | g => 1) * GroupAlgebra.average k G = GroupAlgebra.average k G
The theorem `GroupAlgebra.mul_average_left` states that for any commutative semiring `k`, group `G` which is finite and for any element `g` in `G`, the "average" of the group algebra is invariant under left multiplication by elements of `G`. This means that if we multiply each element of the group by an arbitrary element `g` and then compute the average, the result is the same as if we had computed the average directly. In mathematical terms, for a given `g` in `G`, the operation `(fun₀ | g => 1) * GroupAlgebra.average k G` is equal to `GroupAlgebra.average k G`. Here, `(fun₀ | g => 1)` represents multiplication by `g` in the group algebra, and `GroupAlgebra.average k G` is the average of all elements in the group algebra.
More concisely: For any commutative semiring `k`, finite group `G`, and `g` in `G`, the average of the group algebra is invariant under left multiplication by `g`, that is, `(fun₀ | g => 1) * GroupAlgebra.average k G = GroupAlgebra.average k G`.
|
GroupAlgebra.mul_average_right
theorem GroupAlgebra.mul_average_right :
∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G]
[inst_3 : Invertible ↑(Fintype.card G)] (g : G),
(GroupAlgebra.average k G * fun₀ | g => 1) = GroupAlgebra.average k G
The theorem `GroupAlgebra.mul_average_right` asserts that the average of all elements of a group `G` (when the group is considered as an element of the MonoidAlgebra `k G`), is invariant under right multiplication by elements of `G`. In more mathematical terms, given a commutative semiring `k`, a group `G`, and an element `g` of `G`, the product of the average of `G` and the function that maps `g` to 1 is equal to the average of `G`. This invariance property implies that the average acts as a sort of "center of mass" in the algebra of the group.
More concisely: Given a commutative semiring `k`, a group `G`, and an element `g` in `G`, the average of `G` commutes with right multiplication by `g`, that is, the average of `G` is equal to the average of `G` multiplied by the constant function mapping `g` to 1.
|
Representation.averageMap_id
theorem Representation.averageMap_id :
∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
[inst_3 : Module k V] (ρ : Representation k G V) [inst_4 : Fintype G] [inst_5 : Invertible ↑(Fintype.card G)],
∀ v ∈ ρ.invariants, ρ.averageMap v = v
The theorem `Representation.averageMap_id` states that for any type `k` with a commutative semiring structure, any type `G` with a group structure, and any type `V` with an additive commutative monoid structure and a `k`-module structure, given a representation `ρ` of `G` on the `k`-module `V`, if `G` is a finite type and the cardinality of `G` is invertible, then for any element `v` in the invariants of the representation `ρ`, the action of the `averageMap` of the representation `ρ` on `v` is equal to `v` itself. In other words, the `averageMap` acts as the identity on the subspace of invariants of `ρ`.
More concisely: For any finite commutative semigroup `G`, group `G`, additive commutative monoid `V` with a `G`-module structure over a commutative semiring `k` where the cardinality of `G` is invertible, and representation `ρ` of `G` on `V`, the average map of `ρ` acts as the identity on the subspace of invariants of `ρ`.
|
Representation.averageMap_invariant
theorem Representation.averageMap_invariant :
∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
[inst_3 : Module k V] (ρ : Representation k G V) [inst_4 : Fintype G] [inst_5 : Invertible ↑(Fintype.card G)]
(v : V), ρ.averageMap v ∈ ρ.invariants
The theorem `Representation.averageMap_invariant` states that for any commutative semiring `k`, any group `G`, any additive commutative monoid `V` which has a `k`-module structure, any representation `ρ` of `G` on `V`, and any finite set `G` with an invertible cardinality, the average map sends any element `v` from `V` to the subspace of invariants in `ρ`. In other words, the average map takes an element from `V` and maps it to an invariant in the `ρ` representation.
More concisely: For any commutative semiring `k`, group `G`, additive commutative monoid `V` with a `k`-module structure, finite subgroup `S` of `G` with invertible cardinality, and representation `ρ` of `G` on `V`, the average map `Average ρ` sends any `v` in `V` to the subspace of invariants `Inv(ρ)`.
|