OAI/Algebra/Finitistic/Selection/CharacterModule.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.CharacterModule.projector line 20

   Source documentation

   The unnormalized character projector. Its identity coefficient is one, so normalization is unnecessary for constructing the nonzero test module.

   noncomputable def projector : MonoidAlgebra ℂ F :=
   …

2. theorem OAI.LittleFinitistic.CharacterModule.projector_coeff_one line 23
3. theorem OAI.LittleFinitistic.CharacterModule.projector_ne_zero line 31
4. theorem OAI.LittleFinitistic.CharacterModule.projector_eigen line 37
5. def OAI.LittleFinitistic.CharacterModule.eigenspace line 57

   Source documentation

   All vectors on which the central subgroup acts by the selected character.

   noncomputable def eigenspace : Submodule (MonoidAlgebra ℂ F) (MonoidAlgebra ℂ F) where
   …

6. theorem OAI.LittleFinitistic.CharacterModule.projector_mem line 69
7. theorem OAI.LittleFinitistic.CharacterModule.eigenspace_nontrivial line 72
8. theorem OAI.LittleFinitistic.CharacterModule.eigenspace_finiteDimensional line 79