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

.

Two subgroups `H K`

of `G`

are commensurable if `H ⊓ K`

has finite index in both `H`

and `K`

## Equations

- Commensurable H K = (Subgroup.relindex H K ≠ 0 ∧ Subgroup.relindex K H ≠ 0)

## Instances For

Equivalence of `K/H ⊓ K`

with `gKg⁻¹/gHg⁻¹ ⊓ gKg⁻¹`

## Equations

- Commensurable.quotConjEquiv H K g = Quotient.congr (Subgroup.equivSMul g K).toEquiv ⋯

## Instances For

For `H`

a subgroup of `G`

, this is the subgroup of all elements `g : conjAut G`

such that `Commensurable (g • H) H`

## Equations

- Commensurable.commensurator' H = { toSubmonoid := { toSubsemigroup := { carrier := {g : ConjAct G | Commensurable (g • H) H}, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }

## Instances For

For `H`

a subgroup of `G`

, this is the subgroup of all elements `g : G`

such that `Commensurable (g H g⁻¹) H`

## Equations

- Commensurable.commensurator H = Subgroup.comap (MulEquiv.toMonoidHom ConjAct.toConjAct) (Commensurable.commensurator' H)