Commensurability for subgroups

Two subgroups H and K of a group G are commensurable if H ∩ K has finite index in both H and K.

This file defines commensurability for subgroups of a group G. It goes on to prove that commensurability defines an equivalence relation on subgroups of G and finally defines the commensurator of a subgroup H of G, which is the elements g of G such that gHg⁻¹ is commensurable with H.

Main definitions

• Commensurable H K: the statement that the subgroups H and K of G are commensurable.
• commensurator H: 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.

We define Commensurable both for additive and multiplicative groups (in the AddSubgroup and Subgroup namespaces respectively); but Commensurator is not additivized, since it is not an interesting concept for abelian groups, and it would be unusual to write a non-abelian group additively.

@[deprecated "This technical lemma is no longer necessary for the proof of `commensurable_conj`." (since := "2026-06-25")]

def Subgroup.quotConjEquiv {G : Type u_1} [Group G] (H K : Subgroup G) (g : ConjAct G) : ↥K ⧸ H.subgroupOf K ≃ ↥(g • K) ⧸ (g • H).subgroupOf (g • K)

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

Equations

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

def Subgroup.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

• H.Commensurable K = (H.IsFiniteRelIndex K ∧ K.IsFiniteRelIndex H)

def AddSubgroup.Commensurable {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : Prop

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

Equations

• H.Commensurable K = (H.IsFiniteRelIndex K ∧ K.IsFiniteRelIndex H)

theorem Subgroup.Commensurable.refl {G : Type u_1} [Group G] (H : Subgroup G) : H.Commensurable H

theorem AddSubgroup.Commensurable.refl {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.Commensurable H

theorem Subgroup.Commensurable.comm {G : Type u_1} [Group G] {H K : Subgroup G} : H.Commensurable K ↔ K.Commensurable H

theorem AddSubgroup.Commensurable.comm {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.Commensurable K ↔ K.Commensurable H

theorem Subgroup.Commensurable.symm {G : Type u_1} [Group G] {H K : Subgroup G} : H.Commensurable K → K.Commensurable H

theorem AddSubgroup.Commensurable.symm {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.Commensurable K → K.Commensurable H

theorem Subgroup.Commensurable.trans {G : Type u_1} [Group G] {H K L : Subgroup G} (hhk : H.Commensurable K) (hkl : K.Commensurable L) : H.Commensurable L

theorem AddSubgroup.Commensurable.trans {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hhk : H.Commensurable K) (hkl : K.Commensurable L) : H.Commensurable L

theorem Subgroup.Commensurable.equivalence {G : Type u_1} [Group G] : Equivalence Commensurable

theorem AddSubgroup.Commensurable.equivalence {G : Type u_1} [AddGroup G] : Equivalence Commensurable

@[simp]

theorem Subgroup.Commensurable.top_left_iff {G : Type u_1} [Group G] {H : Subgroup G} : ⊤.Commensurable H ↔ H.FiniteIndex

@[simp]

theorem AddSubgroup.Commensurable.top_left_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⊤.Commensurable H ↔ H.FiniteIndex

@[simp]

theorem Subgroup.Commensurable.top_right_iff {G : Type u_1} [Group G] {H : Subgroup G} : H.Commensurable ⊤ ↔ H.FiniteIndex

@[simp]

theorem AddSubgroup.Commensurable.top_right_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Commensurable ⊤ ↔ H.FiniteIndex

@[simp]

theorem Subgroup.Commensurable.bot_left_iff {G : Type u_1} [Group G] {H : Subgroup G} : ⊥.Commensurable H ↔ Finite ↥H

@[simp]

theorem AddSubgroup.Commensurable.bot_left_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⊥.Commensurable H ↔ Finite ↥H

@[simp]

theorem Subgroup.Commensurable.bot_right_iff {G : Type u_1} [Group G] {H : Subgroup G} : H.Commensurable ⊥ ↔ Finite ↥H

@[simp]

theorem AddSubgroup.Commensurable.bot_right_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Commensurable ⊥ ↔ Finite ↥H

theorem Subgroup.Commensurable.inf_left {G : Type u_1} [Group G] {H K L : Subgroup G} (hHL : H.Commensurable L) (hKL : K.Commensurable L) : (H ⊓ K).Commensurable L

theorem Subgroup.Commensurable.inf_right {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H.Commensurable K) (hHL : H.Commensurable L) : H.Commensurable (K ⊓ L)

theorem Subgroup.Commensurable.map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H K : Subgroup G} (f : G →* G') (h : H.Commensurable K) : (map f H).Commensurable (map f K)

theorem Subgroup.Commensurable.comap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H K : Subgroup G} (f : G' →* G) (h : H.Commensurable K) : (comap f H).Commensurable (comap f K)

theorem Subgroup.Commensurable.map_injective_iff {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H K : Subgroup G} {f : G →* G'} (hf : Function.Injective ⇑f) : (map f H).Commensurable (map f K) ↔ H.Commensurable K

theorem Subgroup.Commensurable.comap_surjective_iff {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H K : Subgroup G} {f : G' →* G} (hf : Function.Surjective ⇑f) : (comap f H).Commensurable (comap f K) ↔ H.Commensurable K

theorem Subgroup.Commensurable.smul {G : Type u_1} [Group G] {H K : Subgroup G} {Φ : Type u_3} [Group Φ] [MulDistribMulAction Φ G] (φ : Φ) (h : H.Commensurable K) : (φ • H).Commensurable (φ • K)

@[deprecated Subgroup.Commensurable.smul (since := "2026-06-25")]

theorem Subgroup.Commensurable.conj {G : Type u_1} [Group G] {H K : Subgroup G} {Φ : Type u_3} [Group Φ] [MulDistribMulAction Φ G] (φ : Φ) (h : H.Commensurable K) : (φ • H).Commensurable (φ • K)

Alias of Subgroup.Commensurable.smul.

theorem Subgroup.Commensurable.smul_iff {G : Type u_1} [Group G] {H K : Subgroup G} {Φ : Type u_3} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} : (φ • H).Commensurable (φ • K) ↔ H.Commensurable K

@[deprecated Subgroup.Commensurable.smul_iff (since := "2026-06-25")]

theorem Subgroup.Commensurable.commensurable_conj {G : Type u_1} [Group G] {H K : Subgroup G} {Φ : Type u_3} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} : (φ • H).Commensurable (φ • K) ↔ H.Commensurable K

Alias of Subgroup.Commensurable.smul_iff.

theorem Subgroup.Commensurable.inv_smul_iff {G : Type u_1} [Group G] {H K : Subgroup G} {Φ : Type u_3} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} : (φ⁻¹ • H).Commensurable K ↔ H.Commensurable (φ • K)

@[deprecated Subgroup.Commensurable.inv_smul_iff (since := "2026-06-25")]

theorem Subgroup.Commensurable.commensurable_inv {G : Type u_1} [Group G] {H K : Subgroup G} {Φ : Type u_3} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} : (φ⁻¹ • H).Commensurable K ↔ H.Commensurable (φ • K)

Alias of Subgroup.Commensurable.inv_smul_iff.

def Subgroup.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

• Subgroup.Commensurable.commensurator H = { carrier := {g : G | (MulAut.conj g • H).Commensurable H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[deprecated "Use `Subgroup.Commensurable.commensurator` instead." (since := "2026-06-25")]

def Subgroup.Commensurable.commensurator' {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup (ConjAct G)

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

Equations

• Subgroup.Commensurable.commensurator' H = Subgroup.map ConjAct.toConjAct.toMonoidHom (Subgroup.Commensurable.commensurator H)

@[simp]

theorem Subgroup.Commensurable.commensurator_mem_iff {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : g ∈ commensurator H ↔ (MulAut.conj g • H).Commensurable H

@[deprecated "Use `commensurator_mem_iff` instead." (since := "2026-06-25")]

theorem Subgroup.Commensurable.commensurator'_mem_iff {G : Type u_1} [Group G] (H : Subgroup G) (g : ConjAct G) : g ∈ commensurator' H ↔ (g • H).Commensurable H

theorem Subgroup.Commensurable.eq {G : Type u_1} [Group G] {H K : Subgroup G} (hk : H.Commensurable K) : commensurator H = commensurator K