OAI/GroupTheory/PolycyclicRecognition/Algebra/UnitaryMautner.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed vectors and contracted elements

The fixed-vector case of Cornulier--Tessera, Lemma 5.2. The proof uses only strong continuity and the isometry identity, with explicit contracting sequences. The closed subgroup generated by these elements then has the same fixed vectors as the contracting subgroup.

  1. def OAI.PolycyclicRecognition.unitaryStabilizer line 25
  2. theorem OAI.PolycyclicRecognition.isClosed_unitaryStabilizer line 42
  3. def OAI.PolycyclicRecognition.contractedBy line 46
  4. theorem OAI.PolycyclicRecognition.unitary_fixed_of_contracted line 49
  5. theorem OAI.PolycyclicRecognition.unitary_fixed_of_contracted_generation line 76
  6. theorem OAI.PolycyclicRecognition.unitary_no_fixed_on_contracting_subgroup line 91