Documentation

Mathlib.GroupTheory.Submonoid.Center

Centers of monoids #

Main definitions #

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

theorem AddSubmonoid.center.proof_1 (M : Type u_1) [AddZeroClass M] :
∀ {a b : M}, a Set.addCenter Mb Set.addCenter Ma + b Set.addCenter M

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

Equations
Instances For

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

    Equations
    Instances For
      theorem AddSubmonoid.center.addCommMonoid'.proof_5 {M : Type u_1} [AddZeroClass M] :
      ∀ (n : ) (x : (AddSubmonoid.center M)), nsmulRec (n + 1) x = nsmulRec (n + 1) x
      theorem AddSubmonoid.center.addCommMonoid'.proof_4 {M : Type u_1} [AddZeroClass M] :
      ∀ (x : (AddSubmonoid.center M)), nsmulRec 0 x = nsmulRec 0 x
      @[reducible, inline]

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

      Equations
      Instances For
        @[reducible, inline]

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

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

        Equations
        Instances For
          Equations

          The center of a monoid is commutative.

          Equations
          theorem AddSubmonoid.mem_center_iff {M : Type u_1} [AddMonoid M] {z : M} :
          z AddSubmonoid.center M ∀ (g : M), g + z = z + g
          theorem Submonoid.mem_center_iff {M : Type u_1} [Monoid M] {z : M} :
          z Submonoid.center M ∀ (g : M), g * z = z * g
          instance AddSubmonoid.decidableMemCenter {M : Type u_1} [AddMonoid M] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
          Equations
          instance Submonoid.decidableMemCenter {M : Type u_1} [Monoid M] (a : M) [Decidable (∀ (b : M), b * a = a * b)] :
          Equations

          The center of a monoid acts commutatively on that monoid.

          Equations
          • =

          The center of a monoid acts commutatively on that monoid.

          Equations
          • =

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

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

          Equations
          Instances For
            @[simp]
            theorem val_unitsCenterToCenterUnits_apply_coe (M : Type u_1) [Monoid M] (n : (↥(Submonoid.center M))ˣ) :
            ((unitsCenterToCenterUnits M) n) = n

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

            Equations
            Instances For