FdRep.char_iso
theorem FdRep.char_iso :
∀ {k : Type u} [inst : Field k] {G : Type u} [inst_1 : Monoid G] {V W : FdRep k G},
(V ≅ W) → V.character = W.character
This theorem states that for any field 'k' and any monoid 'G', if two finite-dimensional 'k'-linear representations of 'G', denoted as 'V' and 'W', are isomorphic, then their characters are the same. In other words, the character of a representation is invariant under isomorphism. This means that if we can find an isomorphism between two such representations, their characters, which capture certain fundamental features of these representations, must be identical.
More concisely: For any field 'k' and monoid 'G', if two finite-dimensional 'k'-linear representations 'V' and 'W' of 'G' are isomorphic, then their characters are equal.
|
FdRep.char_tensor
theorem FdRep.char_tensor :
∀ {k : Type u} [inst : Field k] {G : Type u} [inst_1 : Monoid G] (V W : FdRep k G),
(CategoryTheory.MonoidalCategory.tensorObj V W).character = V.character * W.character
This theorem states that the character of the tensor product of two finite dimensional `k`-linear representations `V` and `W` of a monoid `G` is multiplicative. That is to say that the character of the tensor product is equal to the product of the characters of `V` and `W`. Here, `k` is a field and `G` is a monoid. This property is fundamental to the study of representation theory, as it shows how combining representations (via the tensor product) affects their characters.
More concisely: The character of the tensor product of two finite dimensional `k`-linear representations of a monoid `G`, `V` and `W`, is equal to the product of their characters.
|
FdRep.char_conj
theorem FdRep.char_conj :
∀ {k : Type u} [inst : Field k] {G : Type u} [inst_1 : Group G] (V : FdRep k G) (g h : G),
V.character (h * g * h⁻¹) = V.character g
The theorem `FdRep.char_conj` states that for any field `k`, any group `G`, and any finite-dimensional `k`-linear representation `V` of `G`, the character of the representation `V` is invariant under conjugation. More specifically, for any group elements `g` and `h` in `G`, the character of `V` at the conjugate of `g` by `h` (i.e., `h * g * h⁻¹`) is equal to the character of `V` at `g`. This result is fundamental in the theory of group representations, as it shows that the character, which encapsulates key information about the representation, only depends on the conjugacy class of `g`, not on `g` itself.
More concisely: For any finite-dimensional representation of a group over a field, the character is constant on conjugate group elements.
|
FdRep.char_orthonormal
theorem FdRep.char_orthonormal :
∀ {k : Type u} [inst : Field k] {G : GroupCat} [inst_1 : IsAlgClosed k] [inst_2 : Fintype ↑G]
[inst_3 : Invertible ↑(Fintype.card ↑G)] (V W : FdRep k ↑G) [inst_4 : CategoryTheory.Simple V]
[inst_5 : CategoryTheory.Simple W],
(⅟↑(Fintype.card ↑G) • Finset.univ.sum fun g => V.character g * W.character g⁻¹) =
if Nonempty (V ≅ W) then 1 else 0
This theorem states that for a finite group `G` and an algebraically closed field `k`, if the characteristic of the field doesn't divide the order of the group, then the characters for the irreducible representations `V` and `W` of this group over this field are orthogonal. More precisely, the sum, over all elements in the group, of the product of the character of `V` at an element and the character of `W` at the inverse of that element, scaled by the reciprocal of the order of the group, equals `1` if `V` and `W` are isomorphic as representations and `0` otherwise. This is a formalization of the orthogonality relations for characters in the representation theory of finite groups.
More concisely: For a finite group `G` over an algebraically closed field `k` of characteristic not dividing the group order, the sum of product of characters of irreducible representations `V` and `W` scaled by the reciprocal of the group order is 1 if `V` and `W` are isomorphic, and 0 otherwise.
|