Documentation

Mathlib.GroupTheory.Subgroup.Center

Centers of subgroups #

source
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

Equations
    Instances For
      source
      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

      Equations
        Instances For
          source
          theorem Subgroup.coe_center (G : Type u_1) [Group G] :
          ↑(center G) = Set.center G
          source
          theorem AddSubgroup.coe_center (G : Type u_1) [AddGroup G] :
          ↑(center G) = Set.addCenter G
          source
          @[simp]
          theorem Subgroup.center_toSubmonoid (G : Type u_1) [Group G] :
          (center G).toSubmonoid = Submonoid.center G
          source
          @[simp]
          theorem AddSubgroup.center_toAddSubmonoid (G : Type u_1) [AddGroup G] :
          (center G).toAddSubmonoid = AddSubmonoid.center G
          source
          instance Subgroup.center.isMulCommutative (G : Type u_1) [Group G] :
          IsMulCommutative ↥(center G)
          source
          @[deprecated Subgroup.center.isMulCommutative (since := "2025-04-09")]
          theorem Subgroup.center.isCommutative (G : Type u_1) [Group G] :
          IsMulCommutative ↥(center G)

          Alias of Subgroup.center.isMulCommutative.

          source
          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.

          Equations
            Instances For
              source
              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.

              Equations
                Instances For
                  source
                  @[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
                  @[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
                  @[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
                  @[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
                  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.

                  Equations
                    Instances For
                      source
                      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.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem AddSubgroup.centerToAddOpposite_apply_coe (G : Type u_1) [AddGroup G] (r : ↥(AddSubsemigroup.center G)) :
                          ↑((centerToAddOpposite G) r) = AddOpposite.op ↑r
                          source
                          @[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
                          @[simp]
                          theorem Subgroup.centerToMulOpposite_apply_coe (G : Type u_1) [Group G] (r : ↥(Subsemigroup.center G)) :
                          ↑((centerToMulOpposite G) r) = MulOpposite.op ↑r
                          source
                          @[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
                          theorem Subgroup.mem_center_iff {G : Type u_1} [Group G] {z : G} :
                          z ∈ center G ↔ ∀ (g : G), g * z = z * g
                          source
                          theorem AddSubgroup.mem_center_iff {G : Type u_1} [AddGroup G] {z : G} :
                          z ∈ center G ↔ ∀ (g : G), g + z = z + g
                          source
                          instance Subgroup.decidableMemCenter {G : Type u_1} [Group G] (z : G) [Decidable (∀ (g : G), g * z = z * g)] :
                          Decidable (z ∈ center G)
                          Equations
                            source
                            instance Subgroup.centerCharacteristic {G : Type u_1} [Group G] :
                            (center G).Characteristic
                            source
                            instance AddSubgroup.centerCharacteristic {G : Type u_1} [AddGroup G] :
                            (center G).Characteristic
                            source
                            theorem CommGroup.center_eq_top {G : Type u_2} [CommGroup G] :
                            Subgroup.center G = ⊤
                            source
                            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

                            Equations
                              Instances For
                                source
                                instance Subgroup.instNormalCenter {G : Type u_1} [Group G] :
                                (center G).Normal
                                source
                                instance AddSubgroup.instNormalCenter {G : Type u_1} [AddGroup G] :
                                (center G).Normal
                                source
                                theorem Subgroup.center_le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} :
                                center G ≤ H.normalizer
                                source
                                theorem AddSubgroup.center_le_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                center G ≤ H.normalizer
                                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
                                theorem ConjClasses.mk_bijOn (G : Type u_2) [Group G] :
                                Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ