# mathlibdocumentation

group_theory.commensurable

# 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 subgroups H, K of G
• commensurator: defines the commensurator of a subgroup H of G.

## 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.

def commensurable {G : Type u_1} [group G] (H K : subgroup G) :
Prop

Two subgroups H K of G are commensurable if H ⊓ K has finite index in both H and K

Equations
@[protected]
theorem commensurable.refl {G : Type u_1} [group G] (H : subgroup G) :
theorem commensurable.comm {G : Type u_1} [group G] {H K : subgroup G} :
theorem commensurable.symm {G : Type u_1} [group G] {H K : subgroup G} :
theorem commensurable.trans {G : Type u_1} [group G] {H K L : subgroup G} (hhk : K) (hkl : L) :
theorem commensurable.equivalence {G : Type u_1} [group G] :
def commensurable.quot_conj_equiv {G : Type u_1} [group G] (H K : subgroup G) (g : conj_act G) :

Equivalence of K/H ⊓ K with gKg⁻¹/gHg⁻¹ ⊓ gKg⁻¹

Equations
theorem commensurable.commensurable_conj {G : Type u_1} [group G] {H K : subgroup G} (g : conj_act G) :
commensurable (g H) (g K)
theorem commensurable.commensurable_inv {G : Type u_1} [group G] (H : subgroup G) (g : conj_act G) :
def commensurable.commensurator' {G : Type u_1} [group G] (H : subgroup G) :

For H a subgroup of G, this is the subgroup of all elements g : conj_aut G such that commensurable (g • H) H

Equations
def commensurable.commensurator {G : Type u_1} [group G] (H : subgroup G) :

For H a subgroup of G, this is the subgroup of all elements g : G such that commensurable (g H g⁻¹) H

Equations
@[simp]
theorem commensurable.commensurator'_mem_iff {G : Type u_1} [group G] (H : subgroup G) (g : conj_act G) :
@[simp]
theorem commensurable.commensurator_mem_iff {G : Type u_1} [group G] (H : subgroup G) (g : G) :
theorem commensurable.eq {G : Type u_1} [group G] {H K : subgroup G} (hk : K) :