Documentation

Mathlib.Algebra.Group.Center

Centers of magmas and semigroups #

Main definitions #

See also #

See Mathlib.GroupTheory.Subsemigroup.Center for the definition of the center as a subsemigroup:

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

See Mathlib.GroupTheory.Subsemigroup.Centralizer for the definition of the centralizer as a subsemigroup:

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files.

structure IsAddCentral {M : Type u_1} [Add M] (z : M) :

Conditions for an element to be additively central

  • comm : ∀ (a : M), z + a = a + z

    addition commutes

  • left_assoc : ∀ (b c : M), z + (b + c) = z + b + c

    associative property for left addition

  • mid_assoc : ∀ (a c : M), a + z + c = a + (z + c)

    middle associative addition property

  • right_assoc : ∀ (a b : M), a + b + z = a + (b + z)

    associative property for right addition

Instances For
    theorem IsAddCentral.comm {M : Type u_1} [Add M] {z : M} (self : IsAddCentral z) (a : M) :
    z + a = a + z

    addition commutes

    theorem IsAddCentral.left_assoc {M : Type u_1} [Add M] {z : M} (self : IsAddCentral z) (b : M) (c : M) :
    z + (b + c) = z + b + c

    associative property for left addition

    theorem IsAddCentral.mid_assoc {M : Type u_1} [Add M] {z : M} (self : IsAddCentral z) (a : M) (c : M) :
    a + z + c = a + (z + c)

    middle associative addition property

    theorem IsAddCentral.right_assoc {M : Type u_1} [Add M] {z : M} (self : IsAddCentral z) (a : M) (b : M) :
    a + b + z = a + (b + z)

    associative property for right addition

    structure IsMulCentral {M : Type u_1} [Mul M] (z : M) :

    Conditions for an element to be multiplicatively central

    • comm : ∀ (a : M), z * a = a * z

      multiplication commutes

    • left_assoc : ∀ (b c : M), z * (b * c) = z * b * c

      associative property for left multiplication

    • mid_assoc : ∀ (a c : M), a * z * c = a * (z * c)

      middle associative multiplication property

    • right_assoc : ∀ (a b : M), a * b * z = a * (b * z)

      associative property for right multiplication

    Instances For
      theorem IsMulCentral.comm {M : Type u_1} [Mul M] {z : M} (self : IsMulCentral z) (a : M) :
      z * a = a * z

      multiplication commutes

      theorem IsMulCentral.left_assoc {M : Type u_1} [Mul M] {z : M} (self : IsMulCentral z) (b : M) (c : M) :
      z * (b * c) = z * b * c

      associative property for left multiplication

      theorem IsMulCentral.mid_assoc {M : Type u_1} [Mul M] {z : M} (self : IsMulCentral z) (a : M) (c : M) :
      a * z * c = a * (z * c)

      middle associative multiplication property

      theorem IsMulCentral.right_assoc {M : Type u_1} [Mul M] {z : M} (self : IsMulCentral z) (a : M) (b : M) :
      a * b * z = a * (b * z)

      associative property for right multiplication

      theorem isMulCentral_iff {M : Type u_1} [Mul M] (z : M) :
      IsMulCentral z (∀ (a : M), z * a = a * z) (∀ (b c : M), z * (b * c) = z * b * c) (∀ (a c : M), a * z * c = a * (z * c)) ∀ (a b : M), a * b * z = a * (b * z)
      theorem isAddCentral_iff {M : Type u_1} [Add M] (z : M) :
      IsAddCentral z (∀ (a : M), z + a = a + z) (∀ (b c : M), z + (b + c) = z + b + c) (∀ (a c : M), a + z + c = a + (z + c)) ∀ (a b : M), a + b + z = a + (b + z)
      theorem IsAddCentral.left_comm {M : Type u_1} {a : M} [Add M] (h : IsAddCentral a) (b : M) (c : M) :
      a + (b + c) = b + (a + c)
      theorem IsMulCentral.left_comm {M : Type u_1} {a : M} [Mul M] (h : IsMulCentral a) (b : M) (c : M) :
      a * (b * c) = b * (a * c)
      theorem IsAddCentral.right_comm {M : Type u_1} {c : M} [Add M] (h : IsAddCentral c) (a : M) (b : M) :
      a + b + c = a + c + b
      theorem IsMulCentral.right_comm {M : Type u_1} {c : M} [Mul M] (h : IsMulCentral c) (a : M) (b : M) :
      a * b * c = a * c * b

      Center #

      def Set.addCenter (M : Type u_1) [Add M] :
      Set M

      The center of an additive magma.

      Equations
      Instances For
        def Set.center (M : Type u_1) [Mul M] :
        Set M

        The center of a magma.

        Equations
        Instances For
          def Set.addCentralizer {M : Type u_1} (S : Set M) [Add M] :
          Set M

          The centralizer of a subset of an additive magma.

          Equations
          • S.addCentralizer = {c : M | mS, m + c = c + m}
          Instances For
            def Set.centralizer {M : Type u_1} (S : Set M) [Mul M] :
            Set M

            The centralizer of a subset of a magma.

            Equations
            • S.centralizer = {c : M | mS, m * c = c * m}
            Instances For
              theorem Set.mem_center_iff {M : Type u_1} [Mul M] {z : M} :
              theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} :
              c S.addCentralizer mS, m + c = c + m
              theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} :
              c S.centralizer mS, m * c = c * m
              @[simp]
              theorem Set.add_mem_addCenter {M : Type u_1} [Add M] {z₁ : M} {z₂ : M} (hz₁ : z₁ Set.addCenter M) (hz₂ : z₂ Set.addCenter M) :
              z₁ + z₂ Set.addCenter M
              @[simp]
              theorem Set.mul_mem_center {M : Type u_1} [Mul M] {z₁ : M} {z₂ : M} (hz₁ : z₁ Set.center M) (hz₂ : z₂ Set.center M) :
              z₁ * z₂ Set.center M
              theorem Set.addCenter_subset_addCentralizer {M : Type u_1} [Add M] (S : Set M) :
              Set.addCenter M S.addCentralizer
              theorem Set.center_subset_centralizer {M : Type u_1} [Mul M] (S : Set M) :
              Set.center M S.centralizer
              theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S T) :
              T.addCentralizer S.addCentralizer
              theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Mul M] (h : S T) :
              T.centralizer S.centralizer
              theorem Set.subset_addCentralizer_addCentralizer {M : Type u_1} {S : Set M} [Add M] :
              S S.addCentralizer.addCentralizer
              theorem Set.subset_centralizer_centralizer {M : Type u_1} {S : Set M} [Mul M] :
              S S.centralizer.centralizer
              @[simp]
              theorem Set.addCentralizer_addCentralizer_addCentralizer {M : Type u_1} [Add M] (S : Set M) :
              S.addCentralizer.addCentralizer.addCentralizer = S.addCentralizer
              @[simp]
              theorem Set.centralizer_centralizer_centralizer {M : Type u_1} [Mul M] (S : Set M) :
              S.centralizer.centralizer.centralizer = S.centralizer
              instance Set.decidableMemAddCentralizer {M : Type u_1} {S : Set M} [Add M] [(a : M) → Decidable (bS, b + a = a + b)] :
              DecidablePred fun (x : M) => x S.addCentralizer
              Equations
              instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [Mul M] [(a : M) → Decidable (bS, b * a = a * b)] :
              DecidablePred fun (x : M) => x S.centralizer
              Equations
              theorem AddSemigroup.mem_center_iff {M : Type u_1} [AddSemigroup M] {z : M} :
              z Set.addCenter M ∀ (g : M), g + z = z + g
              theorem Semigroup.mem_center_iff {M : Type u_1} [Semigroup M] {z : M} :
              z Set.center M ∀ (g : M), g * z = z * g
              @[simp]
              theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] {a : M} {b : M} (ha : a S.addCentralizer) (hb : b S.addCentralizer) :
              a + b S.addCentralizer
              @[simp]
              theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} [Semigroup M] {a : M} {b : M} (ha : a S.centralizer) (hb : b S.centralizer) :
              a * b S.centralizer
              @[simp]
              theorem Set.addCentralizer_eq_top_iff_subset {M : Type u_1} {S : Set M} [AddSemigroup M] :
              S.addCentralizer = Set.univ S Set.addCenter M
              @[simp]
              theorem Set.centralizer_eq_top_iff_subset {M : Type u_1} {S : Set M} [Semigroup M] :
              S.centralizer = Set.univ S Set.center M
              @[simp]
              theorem Set.addCentralizer_univ (M : Type u_1) [AddSemigroup M] :
              Set.univ.addCentralizer = Set.addCenter M
              @[simp]
              theorem Set.centralizer_univ (M : Type u_1) [Semigroup M] :
              Set.univ.centralizer = Set.center M
              instance Set.decidableMemAddCenter {M : Type u_1} [AddSemigroup M] [(a : M) → Decidable (∀ (b : M), b + a = a + b)] :
              DecidablePred fun (x : M) => x Set.addCenter M
              Equations
              instance Set.decidableMemCenter {M : Type u_1} [Semigroup M] [(a : M) → Decidable (∀ (b : M), b * a = a * b)] :
              DecidablePred fun (x : M) => x Set.center M
              Equations
              @[simp]
              theorem Set.addCenter_eq_univ (M : Type u_1) [AddCommSemigroup M] :
              Set.addCenter M = Set.univ
              @[simp]
              theorem Set.center_eq_univ (M : Type u_1) [CommSemigroup M] :
              Set.center M = Set.univ
              @[simp]
              theorem Set.addCentralizer_eq_univ (M : Type u_1) {S : Set M} [AddCommSemigroup M] :
              S.addCentralizer = Set.univ
              @[simp]
              theorem Set.centralizer_eq_univ (M : Type u_1) {S : Set M} [CommSemigroup M] :
              S.centralizer = Set.univ
              @[simp]
              theorem Set.one_mem_center {M : Type u_1} [MulOneClass M] :
              @[simp]
              theorem Set.zero_mem_addCentralizer {M : Type u_1} {S : Set M} [AddZeroClass M] :
              0 S.addCentralizer
              @[simp]
              theorem Set.one_mem_centralizer {M : Type u_1} {S : Set M} [MulOneClass M] :
              1 S.centralizer
              @[simp]
              theorem Set.addUnits_neg_mem_center {M : Type u_1} [AddMonoid M] {a : AddUnits M} (ha : a Set.addCenter M) :
              @[simp]
              theorem Set.units_inv_mem_center {M : Type u_1} [Monoid M] {a : Mˣ} (ha : a Set.center M) :
              @[simp]
              theorem Set.invOf_mem_center {M : Type u_1} [Monoid M] {a : M} [Invertible a] (ha : a Set.center M) :
              @[simp]
              theorem Set.neg_mem_addCenter {M : Type u_1} [SubtractionMonoid M] {a : M} (ha : a Set.addCenter M) :
              @[simp]
              theorem Set.inv_mem_center {M : Type u_1} [DivisionMonoid M] {a : M} (ha : a Set.center M) :
              @[simp]
              theorem Set.sub_mem_addCenter {M : Type u_1} [SubtractionMonoid M] {a : M} {b : M} (ha : a Set.addCenter M) (hb : b Set.addCenter M) :
              @[simp]
              theorem Set.div_mem_center {M : Type u_1} [DivisionMonoid M] {a : M} {b : M} (ha : a Set.center M) (hb : b Set.center M) :
              @[simp]
              theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} [AddGroup M] {a : M} (ha : a S.addCentralizer) :
              -a S.addCentralizer
              @[simp]
              theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} [Group M] {a : M} (ha : a S.centralizer) :
              a⁻¹ S.centralizer
              @[simp]
              theorem Set.sub_mem_addCentralizer {M : Type u_1} {S : Set M} [AddGroup M] {a : M} {b : M} (ha : a S.addCentralizer) (hb : b S.addCentralizer) :
              a - b S.addCentralizer
              @[simp]
              theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} [Group M] {a : M} {b : M} (ha : a S.centralizer) (hb : b S.centralizer) :
              a / b S.centralizer