Documentation

Mathlib.GroupTheory.Commensurable

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 #

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.

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
Instances For
    @[deprecated Subgroup.quotConjEquiv (since := "2025-09-17")]
    def Commensurable.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)

    Alias of Subgroup.quotConjEquiv.


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

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

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

        Equations
        Instances For
          @[deprecated Subgroup.Commensurable (since := "2025-09-17")]
          def Commensurable {G : Type u_1} [Group G] (H K : Subgroup G) :

          Alias of Subgroup.Commensurable.


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

          Equations
          Instances For
            theorem Subgroup.Commensurable.trans {G : Type u_1} [Group G] {H K L : Subgroup G} (hhk : H.Commensurable K) (hkl : K.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) :
            theorem Subgroup.Commensurable.conj {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.Commensurable K) (g : ConjAct G) :
            (g H).Commensurable (g K)

            Alias for the forward direction of commensurable_conj to allow dot-notation

            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