OAI/GroupTheory/PolycyclicRecognition/Algebra/UnitaryCentralFixed.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The central fixed subspace in a unitary representation

The central fixed subspace is closed and invariant under the whole group. Its orthogonal projection therefore commutes with the representation. These are the concrete splitting facts for the nilpotent cohomology induction.

  1. def OAI.PolycyclicRecognition.unitaryCentralFixed line 23
  2. theorem OAI.PolycyclicRecognition.isClosed_unitaryCentralFixed line 29
  3. theorem OAI.PolycyclicRecognition.unitaryCentralFixed_map line 36
  4. theorem OAI.PolycyclicRecognition.unitaryCentralFixed_map_eq line 46
  5. theorem OAI.PolycyclicRecognition.unitaryCentralFixed_orthogonal_map line 58
  6. theorem OAI.PolycyclicRecognition.unitaryCentralFixed_orthogonal_no_fixed line 65
  7. instance OAI.PolycyclicRecognition.unitaryCentralFixed_complete line 72
  8. theorem OAI.PolycyclicRecognition.unitaryCentralFixed_projection_commutes line 75