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

def Commensurable {G : Type u_1} [] (H : ) (K : ) :

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

Equations
Instances For
theorem Commensurable.refl {G : Type u_1} [] (H : ) :
theorem Commensurable.comm {G : Type u_1} [] {H : } {K : } :
theorem Commensurable.symm {G : Type u_1} [] {H : } {K : } :
theorem Commensurable.trans {G : Type u_1} [] {H : } {K : } {L : } (hhk : ) (hkl : ) :
theorem Commensurable.equivalence {G : Type u_1} [] :
Equivalence Commensurable
def Commensurable.quotConjEquiv {G : Type u_1} [] (H : ) (K : ) (g : ) :
K (g K).toSubmonoid Subgroup.subgroupOf (g H) (g K)

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

Equations
Instances For
theorem Commensurable.commensurable_conj {G : Type u_1} [] {H : } {K : } (g : ) :
Commensurable (g H) (g K)
theorem Commensurable.commensurable_inv {G : Type u_1} [] (H : ) (g : ) :
def Commensurable.commensurator' {G : Type u_1} [] (H : ) :

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

Equations
• = { toSubmonoid := { toSubsemigroup := { carrier := {g : | Commensurable (g H) H}, mul_mem' := }, one_mem' := }, inv_mem' := }
Instances For
def Commensurable.commensurator {G : Type u_1} [] (H : ) :

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

Equations
Instances For
@[simp]
theorem Commensurable.commensurator'_mem_iff {G : Type u_1} [] (H : ) (g : ) :
@[simp]
theorem Commensurable.commensurator_mem_iff {G : Type u_1} [] (H : ) (g : G) :
Commensurable (ConjAct.toConjAct g H) H
theorem Commensurable.eq {G : Type u_1} [] {H : } {K : } (hk : ) :