CompactRotationalTwist.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Compact rotational modifications

An invariant character into a compact abelian automorphism group has a closed graph inside the semidirect extension. The original group and this graph both have proper cocompact inclusions.

def OAI.PolycyclicRecognition.rotationalTwist line 28
Source documentation
The inverse-character graph, with the multiplication inherited from the semidirect extension. The character is invariant under the compact action.
```
def rotationalTwist : Subgroup (G ⋊[α] K) where
…
```
def OAI.PolycyclicRecognition.rotationalTwistHomeomorph line 42
Source documentation
Removing a rotation changes multiplication, while preserving the underlying topological space.
```
def rotationalTwistHomeomorph [IsTopologicalGroup K] (hτ : Continuous τ) :
    rotationalTwist α τ hinv ≃ₜ G where
…
```
Mentions: OAI.PolycyclicRecognition.rotationalTwist
theorem OAI.PolycyclicRecognition.rotationalTwist_isClosed line 61
theorem OAI.PolycyclicRecognition.semidirect_inl_isProperMap line 68
Source documentation
The original group has a proper inclusion into its semidirect extension.
```
theorem semidirect_inl_isProperMap :
    IsProperMap (SemidirectProduct.inl : G → G ⋊[α] K) := by
…
```
theorem OAI.PolycyclicRecognition.rotationalTwist_subtype_isProperMap line 81
Source documentation
The modified group is likewise properly included.
```
theorem rotationalTwist_subtype_isProperMap (hτ : Continuous τ) :
    IsProperMap (rotationalTwist α τ hinv).subtype :=
…
```
Mentions: OAI.PolycyclicRecognition.rotationalTwist
def OAI.PolycyclicRecognition.semidirect_inl_properCocompact line 88
Source documentation
The rotation subgroup is one fixed compact right-coset cover.
```
def semidirect_inl_properCocompact : ProperCocompactHom G (G ⋊[α] K) where
…
```
Mentions: OAI.PolycyclicRecognition.ProperCocompactHom
def OAI.PolycyclicRecognition.rotationalTwist_properCocompact line 98
Source documentation
The same compact subgroup covers the inverse-character graph, so no metric estimate or triangulability assertion is hidden in this arrow.
```
def rotationalTwist_properCocompact (hτ : Continuous τ) :
    ProperCocompactHom (rotationalTwist α τ hinv) (G ⋊[α] K) where
…
```
Mentions: OAI.PolycyclicRecognition.ProperCocompactHom, OAI.PolycyclicRecognition.rotationalTwist
theorem OAI.PolycyclicRecognition.rotationalTwist_nonempty_metricQuasiEquivalence line 112
Source documentation
Compatible proper chain metrics turn a compact rotational modification into an actual quasi-isometry by composing the two proved arrows.
```
theorem rotationalTwist_nonempty_metricQuasiEquivalence
    (hτ : Continuous τ) (dG : ProperChainMetric G)
    (dT : ProperChainMetric (rotationalTwist α τ hinv))
    (dS : ProperChainMetric (G ⋊[α] K)) :
    letI := dG.compatibleMetric
…
```
Mentions: OAI.PolycyclicRecognition.ProperChainMetric, OAI.PolycyclicRecognition.rotationalTwist