Commensurability for subgroups #
This file defines commensurability for subgroups of a group G
. It then goes on to prove that
commensurability defines an equivalence relation and finally defines the commensurator of a subgroup
of G
.
Main definitions #
Commensurable
: defines commensurability for two subgroupsH
,K
ofG
commensurator
: defines 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
.
theorem
Commensurable.comm
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
:
Commensurable H K ↔ Commensurable K H
theorem
Commensurable.symm
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
:
Commensurable H K → Commensurable K H
theorem
Commensurable.trans
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
{L : Subgroup G}
(hhk : Commensurable H K)
(hkl : Commensurable K L)
:
Commensurable H L
theorem
Commensurable.commensurable_conj
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
(g : ConjAct G)
:
Commensurable H K ↔ Commensurable (g • H) (g • K)
theorem
Commensurable.commensurable_inv
{G : Type u_1}
[Group G]
(H : Subgroup G)
(g : ConjAct G)
:
Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)
For H
a subgroup of G
, this is the subgroup of all elements g : conjAut G
such that Commensurable (g • H) H
Instances For
For H
a subgroup of G
, this is the subgroup of all elements g : G
such that Commensurable (g H g⁻¹) H
Instances For
@[simp]
theorem
Commensurable.commensurator'_mem_iff
{G : Type u_1}
[Group G]
(H : Subgroup G)
(g : ConjAct G)
:
g ∈ Commensurable.commensurator' H ↔ Commensurable (g • H) H
@[simp]
theorem
Commensurable.commensurator_mem_iff
{G : Type u_1}
[Group G]
(H : Subgroup G)
(g : G)
:
g ∈ Commensurable.commensurator H ↔ Commensurable (↑ConjAct.toConjAct g • H) H
theorem
Commensurable.eq
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
(hk : Commensurable H K)
: