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.

def Commensurable {G : Type u_1} [Group G] (H : Subgroup G) (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)

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

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

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

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

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

Equations

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

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)

def 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

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

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

@[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) : Commensurable.commensurator H = Commensurable.commensurator K