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
(conj_act G)
, which we call commensurator' and then taking the pre-image under
the map G → (conj_act G)
to obtain our commensurator as a subgroup of G
.
@[protected, refl]
theorem
commensurable.comm
{G : Type u_1}
[group G]
{H K : subgroup G} :
commensurable H K ↔ commensurable K H
@[symm]
theorem
commensurable.symm
{G : Type u_1}
[group G]
{H K : subgroup G} :
commensurable H K → commensurable K H
@[trans]
theorem
commensurable.trans
{G : Type u_1}
[group G]
{H K L : subgroup G}
(hhk : commensurable H K)
(hkl : commensurable K L) :
commensurable H L
Equivalence of K/H ⊓ K
with gKg⁻¹/gHg⁻¹ ⊓ gKg⁻¹
Equations
- commensurable.quot_conj_equiv H K g = quotient.congr (subgroup.equiv_smul g K).to_equiv _
theorem
commensurable.commensurable_conj
{G : Type u_1}
[group G]
{H K : subgroup G}
(g : conj_act G) :
commensurable H K ↔ commensurable (g • H) (g • K)
theorem
commensurable.commensurable_inv
{G : Type u_1}
[group G]
(H : subgroup G)
(g : conj_act G) :
commensurable (g • H) H ↔ commensurable H (g⁻¹ • H)
For H
a subgroup of G
, this is the subgroup of all elements g : conj_aut G
such that commensurable (g • H) H
Equations
- commensurable.commensurator' H = {carrier := {g : conj_act G | commensurable (g • H) H}, mul_mem' := _, one_mem' := _, inv_mem' := _}
For H
a subgroup of G
, this is the subgroup of all elements g : G
such that commensurable (g H g⁻¹) H
@[simp]
theorem
commensurable.commensurator'_mem_iff
{G : Type u_1}
[group G]
(H : subgroup G)
(g : conj_act 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 (⇑conj_act.to_conj_act g • H) H