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 #

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.

source

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

commensurable H K = (H.relindex K ≠ 0 ∧ K.relindex H ≠ 0)

source

@[protected, refl]

theorem commensurable.refl {G : Type u_1} [group G] (H : subgroup G) :

commensurable H H

source

theorem commensurable.comm {G : Type u_1} [group G] {H K : subgroup G} :

commensurable H K ↔ commensurable K H

source

@[symm]

theorem commensurable.symm {G : Type u_1} [group G] {H K : subgroup G} :

commensurable H K → commensurable K H

source

@[trans]

theorem commensurable.trans {G : Type u_1} [group G] {H K L : subgroup G} (hhk : commensurable H K) (hkl : commensurable K L) :

commensurable H L

source

theorem commensurable.equivalence {G : Type u_1} [group G] :

equivalence commensurable

source

def commensurable.quot_conj_equiv {G : Type u_1} [group G] (H K : subgroup G) (g : conj_act G) :

↥K ⧸ H.subgroup_of K ≃ ↥((g • K).carrier) ⧸ (g • H).subgroup_of (g • K)

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

Equations

commensurable.quot_conj_equiv H K g = quotient.congr (subgroup.equiv_smul g K).to_equiv _

source

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

commensurable H K ↔ commensurable (g • H) (g • K)

source

theorem commensurable.commensurable_inv {G : Type u_1} [group G] (H : subgroup G) (g : conj_act G) :

commensurable (g • H) H ↔ commensurable H (g⁻¹ • H)

source

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

subgroup (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

commensurable.commensurator' H = {carrier := {g : conj_act G | commensurable (g • H) H}, mul_mem' := _, one_mem' := _, inv_mem' := _}

source

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

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

commensurable.commensurator H = subgroup.comap conj_act.to_conj_act.to_monoid_hom (commensurable.commensurator' H)

source

@[simp]

theorem commensurable.commensurator'_mem_iff {G : Type u_1} [group G] (H : subgroup G) (g : conj_act G) :

g ∈ commensurable.commensurator' H ↔ commensurable (g • H) H

source

@[simp]

theorem commensurable.commensurator_mem_iff {G : Type u_1} [group G] (H : subgroup G) (g : G) :

g ∈ commensurable.commensurator H ↔ commensurable (⇑conj_act.to_conj_act g • H) H

source

theorem commensurable.eq {G : Type u_1} [group G] {H K : subgroup G} (hk : commensurable H K) :

commensurable.commensurator H = commensurable.commensurator K