Commensurability for subgroups #
Two subgroups H
and K
of a group G
are commensurable if H ∩ K
has finite index in both H
and K
.
This file defines commensurability for subgroups of a group G
. It goes on to prove that
commensurability defines an equivalence relation on subgroups of G
and finally defines the
commensurator of a subgroup H
of G
, which is the elements g
of G
such that gHg⁻¹
is
commensurable with H
.
Main definitions #
Commensurable H K
: the statement that the subgroupsH
andK
ofG
are commensurable.commensurator H
: the commensurator of a subgroupH
ofG
.
Implementation details #
We define the commensurator of a subgroup H
of G
by first defining it as a subgroup of
(conjAct G)
, which we call commensurator'
and then taking the pre-image under
the map G → (conjAct G)
to obtain our commensurator as a subgroup of G
.
We define Commensurable
both for additive and multiplicative groups (in the AddSubgroup
and
Subgroup
namespaces respectively); but Commensurator
is not additivized, since it is not an
interesting concept for abelian groups, and it would be unusual to write a non-abelian group
additively.
Equivalence of K / (H ⊓ K)
with gKg⁻¹/ (gHg⁻¹ ⊓ gKg⁻¹)
Equations
- H.quotConjEquiv K g = Quotient.congr (Subgroup.equivSMul g K).toEquiv ⋯
Instances For
Alias of Subgroup.quotConjEquiv
.
Equivalence of K / (H ⊓ K)
with gKg⁻¹/ (gHg⁻¹ ⊓ gKg⁻¹)
Equations
Instances For
Two subgroups H K
of G
are commensurable if H ⊓ K
has finite index in both
H
and K
.
Instances For
Alias of Subgroup.Commensurable
.
Two subgroups H K
of G
are commensurable if H ⊓ K
has finite index in both H
and K
.
Equations
Instances For
Alias for the forward direction of commensurable_conj
to allow dot-notation
For H
a subgroup of G
, this is the subgroup of all elements g : conjAut G
such that Commensurable (g • H) H
Equations
Instances For
For H
a subgroup of G
, this is the subgroup of all elements g : G
such that Commensurable (g H g⁻¹) H