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

.

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

def
Commensurable.quotConjEquiv
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(g : ConjAct G)
:

Equivalence of `K/H ⊓ K`

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

## Equations

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

## Instances For

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`

## Equations

- Commensurable.commensurator' H = { 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 ConjAct.toConjAct.toMonoidHom (Commensurable.commensurator' 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)
: