Documentation

Mathlib.GroupTheory.Submonoid.Center

Centers of monoids #

Main definitions #

We provide Subgroup.center, AddSubgroup.center, Subsemiring.center, and Subring.center in other files.

source
๐Ÿ”ธ coverage
def Submonoid.center (M : Type u_1) [MulOneClass M] :
Submonoid M

The center of a multiplication with unit M is the set of elements that commute with everything in M

Instances For
    source
    ๐Ÿ”ธ coverage
    def AddSubmonoid.center (M : Type u_1) [AddZeroClass M] :
    AddSubmonoid M

    The center of an addition with zero M is the set of elements that commute with everything in M

    Instances For
      source
      ๐Ÿ“ coverage
      theorem Submonoid.coe_center (M : Type u_1) [MulOneClass M] :
      โ†‘(center M) = Set.center M
      source
      ๐Ÿ“ coverage
      theorem AddSubmonoid.coe_center (M : Type u_1) [AddZeroClass M] :
      โ†‘(center M) = Set.addCenter M
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Submonoid.center_toSubsemigroup (M : Type u_1) [MulOneClass M] :
      (center M).toSubsemigroup = Subsemigroup.center M
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem AddSubmonoid.center_toAddSubsemigroup (M : Type u_1) [AddZeroClass M] :
      (center M).toAddSubsemigroup = AddSubsemigroup.center M
      source
      ๐Ÿ“ coverage
      instance Submonoid.instSMulCommClassSubtypeMemCenter {M : Type u_2} {ฮฑ : Type u_3} [Monoid M] [MulAction M ฮฑ] :
      SMulCommClass (โ†ฅ(center M)) M ฮฑ
      source
      ๐Ÿ“ coverage
      instance Submonoid.instSMulCommClassSubtypeMemCenter_1 {M : Type u_2} {ฮฑ : Type u_3} [Monoid M] [MulAction M ฮฑ] :
      SMulCommClass M (โ†ฅ(center M)) ฮฑ
      source
      ๐Ÿ”ธ coverage
      @[reducible, inline]
      abbrev Submonoid.center.commMonoid' {M : Type u_1} [MulOneClass M] :
      CommMonoid โ†ฅ(center M)

      The center of a multiplication with unit is commutative and associative.

      This is not an instance as it forms a non-defeq diamond with Submonoid.toMonoid in the npow field.

      Instances For
        source
        ๐Ÿ”ธ coverage
        @[reducible, inline]
        abbrev AddSubmonoid.center.addCommMonoid' {M : Type u_1} [AddZeroClass M] :
        AddCommMonoid โ†ฅ(center M)

        The center of an addition with zero is commutative and associative.

        Instances For
          source
          ๐Ÿ”ธ coverage
          @[implicit_reducible]
          instance Submonoid.center.commMonoid {M : Type u_1} [Monoid M] :
          CommMonoid โ†ฅ(center M)

          The center of a monoid is commutative.

          source
          ๐Ÿ”ธ coverage
          @[implicit_reducible]
          instance AddSubmonoid.center.addCommMonoid {M : Type u_1} [AddMonoid M] :
          AddCommMonoid โ†ฅ(center M)
          source
          ๐Ÿ“ coverage
          theorem Submonoid.mem_center_iff {M : Type u_1} [Monoid M] {z : M} :
          z โˆˆ center M โ†” โˆ€ (g : M), g * z = z * g
          source
          ๐Ÿ“ coverage
          theorem AddSubmonoid.mem_center_iff {M : Type u_1} [AddMonoid M] {z : M} :
          z โˆˆ center M โ†” โˆ€ (g : M), g + z = z + g
          source
          ๐Ÿ”ธ coverage
          @[implicit_reducible]
          instance Submonoid.decidableMemCenter {M : Type u_1} [Monoid M] (a : M) [Decidable (โˆ€ (b : M), b * a = a * b)] :
          Decidable (a โˆˆ center M)
          source
          ๐Ÿ”ธ coverage
          @[implicit_reducible]
          instance AddSubmonoid.decidableMemCenter {M : Type u_1} [AddMonoid M] (a : M) [Decidable (โˆ€ (b : M), b + a = a + b)] :
          Decidable (a โˆˆ center M)
          source
          ๐Ÿ“ coverage
          instance Submonoid.center.smulCommClass_left {M : Type u_1} [Monoid M] :
          SMulCommClass (โ†ฅ(center M)) M M

          The center of a monoid acts commutatively on that monoid.

          source
          ๐Ÿ“ coverage
          instance Submonoid.center.smulCommClass_right {M : Type u_1} [Monoid M] :
          SMulCommClass M (โ†ฅ(center M)) M

          The center of a monoid acts commutatively on that monoid.

          Note that smulCommClass (center M) (center M) M is already implied by Submonoid.smulCommClass_right

          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Submonoid.center_eq_top (M : Type u_1) [CommMonoid M] :
          center M = โŠค
          source
          ๐Ÿ”ธ coverage
          def unitsCenterToCenterUnits (M : Type u_1) [Monoid M] :
          (โ†ฅ(Submonoid.center M))หฃ โ†’* โ†ฅ(Submonoid.center Mหฃ)

          For a monoid, the units of the center inject into the center of the units. This is not an equivalence in general; one case where this holds is for groups with zero, which is covered in centerUnitsEquivUnitsCenter.

          Instances For
            source
            ๐Ÿ”ธ coverage
            def addUnitsCenterToCenterAddUnits (M : Type u_1) [AddMonoid M] :
            AddUnits โ†ฅ(AddSubmonoid.center M) โ†’+ โ†ฅ(AddSubmonoid.center (AddUnits M))

            For an additive monoid, the units of the center inject into the center of the units.

            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem val_unitsCenterToCenterUnits_apply_coe (M : Type u_1) [Monoid M] (n : (โ†ฅ(Submonoid.center M))หฃ) :
              โ†‘โ†‘((unitsCenterToCenterUnits M) n) = โ†‘โ†‘n
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem val_addUnitsCenterToCenterAddUnits_apply_coe (M : Type u_1) [AddMonoid M] (n : AddUnits โ†ฅ(AddSubmonoid.center M)) :
              โ†‘โ†‘((addUnitsCenterToCenterAddUnits M) n) = โ†‘โ†‘n
              source
              ๐Ÿ“ coverage
              theorem unitsCenterToCenterUnits_injective (M : Type u_1) [Monoid M] :
              Function.Injective โ‡‘(unitsCenterToCenterUnits M)
              source
              ๐Ÿ“ coverage
              theorem addUnitsCenterToCenterAddUnits_injective (M : Type u_1) [AddMonoid M] :
              Function.Injective โ‡‘(addUnitsCenterToCenterAddUnits M)
              source
              ๐Ÿ“ coverage
              theorem MulEquivClass.apply_mem_center {M : Type u_3} {N : Type u_1} {F : Type u_2} [EquivLike F M N] [Mul M] [Mul N] [MulEquivClass F M N] (e : F) {x : M} (hx : x โˆˆ Set.center M) :
              e x โˆˆ Set.center N
              source
              ๐Ÿ“ coverage
              theorem AddEquivClass.apply_mem_center {M : Type u_3} {N : Type u_1} {F : Type u_2} [EquivLike F M N] [Add M] [Add N] [AddEquivClass F M N] (e : F) {x : M} (hx : x โˆˆ Set.addCenter M) :
              e x โˆˆ Set.addCenter N
              source
              ๐Ÿ“ coverage
              theorem MulEquivClass.apply_mem_center_iff {M : Type u_3} {N : Type u_1} {F : Type u_2} [EquivLike F M N] [Mul M] [Mul N] [MulEquivClass F M N] (e : F) {x : M} :
              e x โˆˆ Set.center N โ†” x โˆˆ Set.center M
              source
              ๐Ÿ“ coverage
              theorem AddEquivClass.apply_mem_center_iff {M : Type u_3} {N : Type u_1} {F : Type u_2} [EquivLike F M N] [Add M] [Add N] [AddEquivClass F M N] (e : F) {x : M} :
              e x โˆˆ Set.addCenter N โ†” x โˆˆ Set.addCenter M
              source
              ๐Ÿ”ธ coverage
              def Subsemigroup.centerCongr {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M โ‰ƒ* N) :
              โ†ฅ(center M) โ‰ƒ* โ†ฅ(center N)

              The center of isomorphic magmas are isomorphic.

              Instances For
                source
                ๐Ÿ”ธ coverage
                def AddSubsemigroup.centerCongr {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M โ‰ƒ+ N) :
                โ†ฅ(center M) โ‰ƒ+ โ†ฅ(center N)

                The center of isomorphic additive magmas are isomorphic.

                Instances For
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AddSubsemigroup.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M โ‰ƒ+ N) (r : โ†ฅ(center M)) :
                  โ†‘((centerCongr e) r) = e โ†‘r
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem Subsemigroup.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M โ‰ƒ* N) (r : โ†ฅ(center M)) :
                  โ†‘((centerCongr e) r) = e โ†‘r
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem Subsemigroup.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M โ‰ƒ* N) (s : โ†ฅ(center N)) :
                  โ†‘((centerCongr e).symm s) = e.symm โ†‘s
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AddSubsemigroup.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M โ‰ƒ+ N) (s : โ†ฅ(center N)) :
                  โ†‘((centerCongr e).symm s) = e.symm โ†‘s
                  source
                  ๐Ÿ”ธ coverage
                  def Submonoid.centerCongr {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M โ‰ƒ* N) :
                  โ†ฅ(center M) โ‰ƒ* โ†ฅ(center N)

                  The center of isomorphic monoids are isomorphic.

                  Instances For
                    source
                    ๐Ÿ”ธ coverage
                    def AddSubmonoid.centerCongr {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M โ‰ƒ+ N) :
                    โ†ฅ(center M) โ‰ƒ+ โ†ฅ(center N)

                    The center of isomorphic additive monoids are isomorphic.

                    Instances For
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem Submonoid.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M โ‰ƒ* N) (r : โ†ฅ(Subsemigroup.center M)) :
                      โ†‘((centerCongr e) r) = e โ†‘r
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem Submonoid.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M โ‰ƒ* N) (s : โ†ฅ(Subsemigroup.center N)) :
                      โ†‘((centerCongr e).symm s) = e.symm โ†‘s
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem AddSubmonoid.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M โ‰ƒ+ N) (r : โ†ฅ(AddSubsemigroup.center M)) :
                      โ†‘((centerCongr e) r) = e โ†‘r
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem AddSubmonoid.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M โ‰ƒ+ N) (s : โ†ฅ(AddSubsemigroup.center N)) :
                      โ†‘((centerCongr e).symm s) = e.symm โ†‘s
                      source
                      ๐Ÿ“ coverage
                      theorem MulOpposite.op_mem_center_iff {M : Type u_2} [Mul M] {x : M} :
                      op x โˆˆ Set.center Mแตแต’แต– โ†” x โˆˆ Set.center M
                      source
                      ๐Ÿ“ coverage
                      theorem AddOpposite.op_mem_center_iff {M : Type u_2} [Add M] {x : M} :
                      op x โˆˆ Set.addCenter Mแตƒแต’แต– โ†” x โˆˆ Set.addCenter M
                      source
                      ๐Ÿ“ coverage
                      theorem MulOpposite.unop_mem_center_iff {M : Type u_2} [Mul M] {x : Mแตแต’แต–} :
                      unop x โˆˆ Set.center M โ†” x โˆˆ Set.center Mแตแต’แต–
                      source
                      ๐Ÿ“ coverage
                      theorem AddOpposite.unop_mem_center_iff {M : Type u_2} [Add M] {x : Mแตƒแต’แต–} :
                      unop x โˆˆ Set.addCenter M โ†” x โˆˆ Set.addCenter Mแตƒแต’แต–
                      source
                      ๐Ÿ”ธ coverage
                      def Subsemigroup.centerToMulOpposite {M : Type u_2} [Mul M] :
                      โ†ฅ(center M) โ‰ƒ* โ†ฅ(center Mแตแต’แต–)

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

                      Instances For
                        source
                        ๐Ÿ”ธ coverage
                        def AddSubsemigroup.centerToAddOpposite {M : Type u_2} [Add M] :
                        โ†ฅ(center M) โ‰ƒ+ โ†ฅ(center Mแตƒแต’แต–)

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

                        Instances For
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem Subsemigroup.centerToMulOpposite_apply_coe {M : Type u_2} [Mul M] (r : โ†ฅ(center M)) :
                          โ†‘(centerToMulOpposite r) = MulOpposite.op โ†‘r
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem AddSubsemigroup.centerToAddOpposite_symm_apply_coe {M : Type u_2} [Add M] (r : โ†ฅ(center Mแตƒแต’แต–)) :
                          โ†‘(centerToAddOpposite.symm r) = AddOpposite.unop โ†‘r
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem Subsemigroup.centerToMulOpposite_symm_apply_coe {M : Type u_2} [Mul M] (r : โ†ฅ(center Mแตแต’แต–)) :
                          โ†‘(centerToMulOpposite.symm r) = MulOpposite.unop โ†‘r
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem AddSubsemigroup.centerToAddOpposite_apply_coe {M : Type u_2} [Add M] (r : โ†ฅ(center M)) :
                          โ†‘(centerToAddOpposite r) = AddOpposite.op โ†‘r
                          source
                          ๐Ÿ”ธ coverage
                          def Submonoid.centerToMulOpposite {M : Type u_2} [MulOneClass M] :
                          โ†ฅ(center M) โ‰ƒ* โ†ฅ(center Mแตแต’แต–)

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

                          Instances For
                            source
                            ๐Ÿ”ธ coverage
                            def AddSubmonoid.centerToAddOpposite {M : Type u_2} [AddZeroClass M] :
                            โ†ฅ(center M) โ‰ƒ+ โ†ฅ(center Mแตƒแต’แต–)

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

                            Instances For
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem Submonoid.centerToMulOpposite_symm_apply_coe {M : Type u_2} [MulOneClass M] (r : โ†ฅ(Subsemigroup.center Mแตแต’แต–)) :
                              โ†‘(centerToMulOpposite.symm r) = MulOpposite.unop โ†‘r
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem AddSubmonoid.centerToAddOpposite_apply_coe {M : Type u_2} [AddZeroClass M] (r : โ†ฅ(AddSubsemigroup.center M)) :
                              โ†‘(centerToAddOpposite r) = AddOpposite.op โ†‘r
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem AddSubmonoid.centerToAddOpposite_symm_apply_coe {M : Type u_2} [AddZeroClass M] (r : โ†ฅ(AddSubsemigroup.center Mแตƒแต’แต–)) :
                              โ†‘(centerToAddOpposite.symm r) = AddOpposite.unop โ†‘r
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem Submonoid.centerToMulOpposite_apply_coe {M : Type u_2} [MulOneClass M] (r : โ†ฅ(Subsemigroup.center M)) :
                              โ†‘(centerToMulOpposite r) = MulOpposite.op โ†‘r