Documentation

Mathlib.GroupTheory.Subgroup.Centralizer

Centralizers of subgroups #

def Subgroup.centralizer {G : Type u_1} [Group G] (s : Set G) :

The centralizer of s is the subgroup of g : G commuting with every h : s.

Equations
    Instances For
      def AddSubgroup.centralizer {G : Type u_1} [AddGroup G] (s : Set G) :

      The centralizer of s is the additive subgroup of g : G commuting with every h : s.

      Equations
        Instances For
          theorem Subgroup.mem_centralizer_iff {G : Type u_1} [Group G] {g : G} {s : Set G} :
          g centralizer s hs, h * g = g * h
          theorem AddSubgroup.mem_centralizer_iff {G : Type u_1} [AddGroup G] {g : G} {s : Set G} :
          g centralizer s hs, h + g = g + h
          theorem Subgroup.mem_centralizer_iff_commutator_eq_one {G : Type u_1} [Group G] {g : G} {s : Set G} :
          g centralizer s hs, h * g * h⁻¹ * g⁻¹ = 1
          theorem AddSubgroup.mem_centralizer_iff_commutator_eq_zero {G : Type u_1} [AddGroup G] {g : G} {s : Set G} :
          g centralizer s hs, h + g + -h + -g = 0
          theorem Subgroup.mem_centralizer_singleton_iff {G : Type u_1} [Group G] {g k : G} :
          k centralizer {g} k * g = g * k
          theorem Subgroup.le_centralizer_iff {G : Type u_1} [Group G] {H K : Subgroup G} :
          theorem Subgroup.centralizer_le {G : Type u_1} [Group G] {s t : Set G} (h : s t) :
          theorem AddSubgroup.centralizer_le {G : Type u_1} [AddGroup G] {s t : Set G} (h : s t) :
          @[simp]
          theorem Subgroup.map_centralizer_le_centralizer_image {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (s : Set G) (f : G →* G') :
          theorem AddSubgroup.map_centralizer_le_centralizer_image {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (s : Set G) (f : G →+ G') :
          @[deprecated Subgroup.le_centralizer_iff_isMulCommutative (since := "2025-04-09")]

          Alias of Subgroup.le_centralizer_iff_isMulCommutative.

          @[deprecated AddSubgroup.le_centralizer_iff_isAddCommutative (since := "2025-04-09")]

          Alias of AddSubgroup.le_centralizer_iff_isAddCommutative.

          theorem Subgroup.le_centralizer {G : Type u_1} [Group G] (H : Subgroup G) [h : IsMulCommutative H] :
          @[reducible, inline]
          abbrev Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : xk, yk, x * y = y * x) :

          If all the elements of a set s commute, then closure s is a commutative group.

          Equations
            Instances For
              @[reducible, inline]
              abbrev AddSubgroup.closureAddCommGroupOfComm {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : xk, yk, x + y = y + x) :

              If all the elements of a set s commute, then closure s is an additive commutative group.

              Equations
                Instances For

                  The conjugation action of N(H) on H.

                  Equations
                    @[simp]
                    theorem Subgroup.smul_coe {G : Type u_1} [Group G] (H : Subgroup G) (g : H.normalizer) (h : H) :
                    (SMul.smul g h) = g * h * g⁻¹

                    The homomorphism N(H) → Aut(H) with kernel C(H).

                    Equations
                      Instances For
                        @[simp]
                        theorem Subgroup.normalizerMonoidHom_apply_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (x : H.normalizer) (a✝ : H) :
                        ((H.normalizerMonoidHom x) a✝) = x * a✝ * (↑x)⁻¹
                        @[simp]
                        theorem Subgroup.normalizerMonoidHom_apply_symm_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (x : H.normalizer) (a✝ : H) :
                        ((MulEquiv.symm (H.normalizerMonoidHom x)) a✝) = (↑x)⁻¹ * a✝ * x