Documentation

Mathlib.GroupTheory.Subgroup.Center

Centers of subgroups #

source
๐Ÿ”ธ coverage
def Subgroup.center (G : Type u_1) [Group G] :
Subgroup G

The center of a group G is the set of elements that commute with everything in G

Instances For
    source
    ๐Ÿ”ธ coverage
    def AddSubgroup.center (G : Type u_1) [AddGroup G] :
    AddSubgroup G

    The center of an additive group G is the set of elements that commute with everything in G

    Instances For
      source
      ๐Ÿ“ coverage
      theorem Subgroup.coe_center (G : Type u_1) [Group G] :
      โ†‘(center G) = Set.center G
      source
      ๐Ÿ“ coverage
      theorem AddSubgroup.coe_center (G : Type u_1) [AddGroup G] :
      โ†‘(center G) = Set.addCenter G
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subgroup.center_toSubmonoid (G : Type u_1) [Group G] :
      (center G).toSubmonoid = Submonoid.center G
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem AddSubgroup.center_toAddSubmonoid (G : Type u_1) [AddGroup G] :
      (center G).toAddSubmonoid = AddSubmonoid.center G
      source
      ๐Ÿ“ coverage
      instance Subgroup.center.isMulCommutative (G : Type u_1) [Group G] :
      IsMulCommutative โ†ฅ(center G)
      source
      ๐Ÿ”ธ coverage
      def Subgroup.centerCongr {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G โ‰ƒ* H) :
      โ†ฅ(center G) โ‰ƒ* โ†ฅ(center H)

      The center of isomorphic groups are isomorphic.

      Instances For
        source
        ๐Ÿ”ธ coverage
        def AddSubgroup.centerCongr {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (e : G โ‰ƒ+ H) :
        โ†ฅ(center G) โ‰ƒ+ โ†ฅ(center H)

        The center of isomorphic additive groups are isomorphic.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Subgroup.centerCongr_symm_apply_coe {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G โ‰ƒ* H) (s : โ†ฅ(Subsemigroup.center H)) :
          โ†‘((centerCongr e).symm s) = e.symm โ†‘s
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddSubgroup.centerCongr_apply_coe {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (e : G โ‰ƒ+ H) (r : โ†ฅ(AddSubsemigroup.center G)) :
          โ†‘((centerCongr e) r) = e โ†‘r
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Subgroup.centerCongr_apply_coe {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G โ‰ƒ* H) (r : โ†ฅ(Subsemigroup.center G)) :
          โ†‘((centerCongr e) r) = e โ†‘r
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddSubgroup.centerCongr_symm_apply_coe {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (e : G โ‰ƒ+ H) (s : โ†ฅ(AddSubsemigroup.center H)) :
          โ†‘((centerCongr e).symm s) = e.symm โ†‘s
          source
          ๐Ÿ”ธ coverage
          def Subgroup.centerToMulOpposite (G : Type u_1) [Group G] :
          โ†ฅ(center G) โ‰ƒ* โ†ฅ(center Gแตแต’แต–)

          The center of a group is isomorphic to the center of its opposite.

          Instances For
            source
            ๐Ÿ”ธ coverage
            def AddSubgroup.centerToAddOpposite (G : Type u_1) [AddGroup G] :
            โ†ฅ(center G) โ‰ƒ+ โ†ฅ(center Gแตƒแต’แต–)

            The center of an additive group is isomorphic to the center of its opposite.

            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem Subgroup.centerToMulOpposite_apply_coe (G : Type u_1) [Group G] (r : โ†ฅ(Subsemigroup.center G)) :
              โ†‘((centerToMulOpposite G) r) = MulOpposite.op โ†‘r
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem Subgroup.centerToMulOpposite_symm_apply_coe (G : Type u_1) [Group G] (r : โ†ฅ(Subsemigroup.center Gแตแต’แต–)) :
              โ†‘((centerToMulOpposite G).symm r) = MulOpposite.unop โ†‘r
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem AddSubgroup.centerToAddOpposite_apply_coe (G : Type u_1) [AddGroup G] (r : โ†ฅ(AddSubsemigroup.center G)) :
              โ†‘((centerToAddOpposite G) r) = AddOpposite.op โ†‘r
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem AddSubgroup.centerToAddOpposite_symm_apply_coe (G : Type u_1) [AddGroup G] (r : โ†ฅ(AddSubsemigroup.center Gแตƒแต’แต–)) :
              โ†‘((centerToAddOpposite G).symm r) = AddOpposite.unop โ†‘r
              source
              ๐Ÿ“ coverage
              theorem Subgroup.mem_center_iff {G : Type u_1} [Group G] {z : G} :
              z โˆˆ center G โ†” โˆ€ (g : G), g * z = z * g
              source
              ๐Ÿ“ coverage
              theorem AddSubgroup.mem_center_iff {G : Type u_1} [AddGroup G] {z : G} :
              z โˆˆ center G โ†” โˆ€ (g : G), g + z = z + g
              source
              ๐Ÿ”ธ coverage
              @[implicit_reducible]
              instance Subgroup.decidableMemCenter {G : Type u_1} [Group G] (z : G) [Decidable (โˆ€ (g : G), g * z = z * g)] :
              Decidable (z โˆˆ center G)
              source
              ๐Ÿ“ coverage
              instance Subgroup.centerCharacteristic {G : Type u_1} [Group G] :
              (center G).Characteristic
              source
              ๐Ÿ“ coverage
              instance AddSubgroup.centerCharacteristic {G : Type u_1} [AddGroup G] :
              (center G).Characteristic
              source
              ๐Ÿ“ coverage
              theorem CommGroup.center_eq_top {G : Type u_2} [CommGroup G] :
              Subgroup.center G = โŠค
              source
              ๐Ÿ”ธ coverage
              @[implicit_reducible]
              def Group.commGroupOfCenterEqTop {G : Type u_1} [Group G] (h : Subgroup.center G = โŠค) :
              CommGroup G

              A group is commutative if the center is the whole group

              Instances For
                source
                ๐Ÿ“ coverage
                instance Subgroup.instNormalCenter {G : Type u_1} [Group G] :
                (center G).Normal
                source
                ๐Ÿ“ coverage
                instance AddSubgroup.instNormalCenter {G : Type u_1} [AddGroup G] :
                (center G).Normal
                source
                ๐Ÿ“ coverage
                theorem Subgroup.center_le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} :
                center G โ‰ค normalizer โ†‘H
                source
                ๐Ÿ“ coverage
                theorem AddSubgroup.center_le_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                center G โ‰ค normalizer โ†‘H
                source
                theorem IsConj.eq_of_left_mem_center {M : Type u_2} [Monoid M] {g h : M} (H : IsConj g h) (Hg : g โˆˆ Set.center M) :
                g = h
                source
                theorem IsConj.eq_of_right_mem_center {M : Type u_2} [Monoid M] {g h : M} (H : IsConj g h) (Hh : h โˆˆ Set.center M) :
                g = h
                source
                ๐Ÿ“ coverage
                theorem ConjClasses.mk_bijOn (G : Type u_2) [Group G] :
                Set.BijOn ConjClasses.mk (โ†‘(Subgroup.center G)) (noncenter G)แถœ