ActualRotationalModification.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual compact rotational modification of the original group

def OAI.PolycyclicRecognition.ComplexWeightFactorModel.compactRotationAction line 22
Source documentation
The compact action on the original group, now with its invariant character.
```
def compactRotationAction : realRotationTorus (GroupLieAlgebra (𝓘(ℝ,E)) G) H →* MulAut G :=
…
```
Mentions: OAI.PolycyclicRecognition.realRotationTorus
theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.continuous_compactRotationAction line 25
theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.compactRotationAction_invariant line 30
abbrev OAI.PolycyclicRecognition.ComplexWeightFactorModel.RotationalModification line 37
Source documentation
The concrete graph subgroup that removes the compact rotations.
```
abbrev RotationalModification :=
…
```
def OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationalModificationHomeomorph line 42
Source documentation
The modification preserves the original underlying topology.
```
def rotationalModificationHomeomorph : F.RotationalModification hExp ≃ₜ G :=
…
```
instance OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationalExtensionTopologicalGroup line 46
instance OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationalModificationTopologicalGroup line 52
def OAI.PolycyclicRecognition.ComplexWeightFactorModel.originalToRotationalExtension line 56
Source documentation
The original group is properly and cocompactly included in the compact extension.
```
def originalToRotationalExtension :
    ProperCocompactHom G (G ⋊[F.compactRotationAction hExp]
      realRotationTorus (GroupLieAlgebra (𝓘(ℝ,E)) G) H) := by
…
```
Mentions: OAI.PolycyclicRecognition.ProperCocompactHom, OAI.PolycyclicRecognition.realRotationTorus
def OAI.PolycyclicRecognition.ComplexWeightFactorModel.modificationToRotationalExtension line 63
Source documentation
The actual modification has the other proper cocompact inclusion.
```
def modificationToRotationalExtension :
    ProperCocompactHom (F.RotationalModification hExp)
      (G ⋊[F.compactRotationAction hExp] realRotationTorus (GroupLieAlgebra (𝓘(ℝ,E)) G) H) := by
…
```
Mentions: OAI.PolycyclicRecognition.ProperCocompactHom, OAI.PolycyclicRecognition.realRotationTorus