Documentation

Mathlib.GroupTheory.Commensurable

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 #

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) :

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

Equations
Instances For
    theorem Commensurable.refl {G : Type u_1} [Group G] (H : Subgroup G) :
    theorem Commensurable.comm {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
    theorem Commensurable.symm {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
    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) :
    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
    Instances For
      theorem Commensurable.commensurable_conj {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (g : 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
      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
        Instances For
          @[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