mathlib3 documentation

group_theory.commensurable

Commensurability for subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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, refl]
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} :
@[symm]
theorem commensurable.symm {G : Type u_1} [group G] {H K : subgroup G} :
@[trans]
theorem commensurable.trans {G : Type u_1} [group G] {H K L : subgroup G} (hhk : commensurable H K) (hkl : commensurable K L) :
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) :
theorem commensurable.commensurable_inv {G : Type u_1} [group G] (H : subgroup G) (g : conj_act 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