OAI/RepresentationTheory/FiniteUnitary/Characters.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.FiniteCharacters.classRep line 11
2. lemma OAI.CubeShuffle.FiniteCharacters.classRep_spec line 13
3. def OAI.CubeShuffle.FiniteCharacters.characterClass line 18
4. lemma OAI.CubeShuffle.FiniteCharacters.characterClass_mk line 22
5. def OAI.CubeShuffle.FiniteCharacters.characterDual line 29
6. lemma OAI.CubeShuffle.FiniteCharacters.characterDual_characterClass line 39
7. theorem OAI.CubeShuffle.FiniteCharacters.complete_of_card_conjugacy_le line 54

   Source documentation

   A finite family of pairwise inequivalent irreducibles whose size is at least the number of conjugacy classes is complete. This avoids assuming any symmetric-group classification theorem.

   theorem complete_of_card_conjugacy_le
       {G ι : Type*} [Group G] [Fintype G] [Fintype ι]
       (V : ι → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module ℂ (V i)]
       [∀ i, FiniteDimensional ℂ (V i)]
       (ρ : ∀ i, Representation ℂ G (V i)) [∀ i, Representation.IsIrreducible (ρ i)]
       (hneq : ∀ i j, i ≠ j → ¬Nonempty (Representation.Equiv (ρ i) (ρ j)))
       (hcard : Nat.card (ConjClasses G) ≤ Fintype.card ι)
       {W : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
       (σ : Representation ℂ G W) [Representation.IsIrreducible σ] :
       ∃ i, Nonempty (Representation.Equiv (ρ i) σ) := by
   …

8. lemma OAI.CubeShuffle.FiniteCharacters.character_expansion line 112
9. theorem OAI.CubeShuffle.FiniteCharacters.sum_dimension_sq line 141

   Source documentation

   The sum of squared dimensions is derived from the actual character basis, without a regular-module decomposition assumption.

   theorem sum_dimension_sq : ∑ i, (Module.finrank ℂ (V i))^2=Fintype.card G := by
   …