RationalConjugation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Rational conjugation on an abelian normal subgroup

Conjugation extends to the rationalization. When the subgroup is torsion free, the extended action has exactly the same kernel, namely its centralizer. Together with the rank bound this is a finite-dimensional representation of the centralizer quotient, without a finite-generation assumption on the abelian subgroup.

def OAI.PolycyclicRecognition.rationalAbelianAut line 24
theorem OAI.PolycyclicRecognition.rationalAbelianAut_map line 35
theorem OAI.PolycyclicRecognition.rationalAbelianAut_injective line 39
def OAI.PolycyclicRecognition.rationalConjugation line 49
theorem OAI.PolycyclicRecognition.rationalConjugation_ker line 53
theorem OAI.PolycyclicRecognition.rationalConjugation_ker_of_finiteDimension line 70
def OAI.PolycyclicRecognition.rationalConjugationQuotient line 76
Source documentation
The centralizer quotient acts faithfully on the rationalization.
```
def rationalConjugationQuotient (hH : HasNoNontrivialTorsion H) :
    (G ⧸ Subgroup.centralizer (H : Set G)) →*
      (RationalAbelianSpace H ≃ₗ[ℚ] RationalAbelianSpace H) :=
…
```
Mentions: OAI.PolycyclicRecognition.HasNoNontrivialTorsion, OAI.PolycyclicRecognition.RationalAbelianSpace
theorem OAI.PolycyclicRecognition.rationalConjugationQuotient_injective line 82