Documentation

Mathlib.Algebra.Group.Conj

Conjugacy of group elements #

See also MulAut.conj and Quandle.conj.

def IsConj {α : Type u} [Monoid α] (a : α) (b : α) :

We say that a is conjugate to b if for some unit c we have c * a * c⁻¹ = b.

Equations
Instances For
    theorem IsConj.refl {α : Type u} [Monoid α] (a : α) :
    IsConj a a
    theorem IsConj.symm {α : Type u} [Monoid α] {a : α} {b : α} :
    IsConj a bIsConj b a
    theorem isConj_comm {α : Type u} [Monoid α] {g : α} {h : α} :
    IsConj g h IsConj h g
    theorem IsConj.trans {α : Type u} [Monoid α] {a : α} {b : α} {c : α} :
    IsConj a bIsConj b cIsConj a c
    @[simp]
    theorem isConj_iff_eq {α : Type u_1} [CommMonoid α] {a : α} {b : α} :
    IsConj a b a = b
    theorem MonoidHom.map_isConj {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) {a : α} {b : α} :
    IsConj a bIsConj (f a) (f b)
    @[simp]
    theorem isConj_one_right {α : Type u} [CancelMonoid α] {a : α} :
    IsConj 1 a a = 1
    @[simp]
    theorem isConj_one_left {α : Type u} [CancelMonoid α] {a : α} :
    IsConj a 1 a = 1
    @[simp]
    theorem isConj_iff {α : Type u} [Group α] {a : α} {b : α} :
    IsConj a b ∃ (c : α), c * a * c⁻¹ = b
    theorem conj_inv {α : Type u} [Group α] {a : α} {b : α} :
    (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
    @[simp]
    theorem conj_mul {α : Type u} [Group α] {a : α} {b : α} {c : α} :
    b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹
    @[simp]
    theorem conj_pow {α : Type u} [Group α] {i : } {a : α} {b : α} :
    (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
    @[simp]
    theorem conj_zpow {α : Type u} [Group α] {i : } {a : α} {b : α} :
    (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
    theorem conj_injective {α : Type u} [Group α] {x : α} :
    Function.Injective fun (g : α) => x * g * x⁻¹
    @[simp]
    theorem isConj_iff₀ {α : Type u} [GroupWithZero α] {a : α} {b : α} :
    IsConj a b ∃ (c : α), c 0 c * a * c⁻¹ = b
    def IsConj.setoid (α : Type u_1) [Monoid α] :

    The setoid of the relation IsConj iff there is a unit u such that u * x = y * u

    Equations
    Instances For
      def ConjClasses (α : Type u_1) [Monoid α] :
      Type u_1

      The quotient type of conjugacy classes of a group.

      Equations
      Instances For
        def ConjClasses.mk {α : Type u_1} [Monoid α] (a : α) :

        The canonical quotient map from a monoid α into the ConjClasses of α

        Equations
        Instances For
          Equations
          • ConjClasses.instInhabitedConjClasses = { default := 1 }
          theorem ConjClasses.quotient_mk_eq_mk {α : Type u} [Monoid α] (a : α) :
          a = ConjClasses.mk a
          theorem ConjClasses.quot_mk_eq_mk {α : Type u} [Monoid α] (a : α) :
          Quot.mk Setoid.r a = ConjClasses.mk a
          theorem ConjClasses.forall_isConj {α : Type u} [Monoid α] {p : ConjClasses αProp} :
          (∀ (a : ConjClasses α), p a) ∀ (a : α), p (ConjClasses.mk a)
          theorem ConjClasses.mk_surjective {α : Type u} [Monoid α] :
          Function.Surjective ConjClasses.mk
          Equations
          • ConjClasses.instOneConjClasses = { one := 1 }
          theorem ConjClasses.exists_rep {α : Type u} [Monoid α] (a : ConjClasses α) :
          ∃ (a0 : α), ConjClasses.mk a0 = a
          def ConjClasses.map {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) :

          A MonoidHom maps conjugacy classes of one group to conjugacy classes of another.

          Equations
          Instances For
            theorem ConjClasses.map_surjective {α : Type u} {β : Type v} [Monoid α] [Monoid β] {f : α →* β} (hf : Function.Surjective f) :
            Equations
            • ConjClasses.instDecidableEqConjClasses = instDecidableEqQuotient

            The bijection between a CommGroup and its ConjClasses.

            Equations
            • ConjClasses.mkEquiv = { toFun := ConjClasses.mk, invFun := Quotient.lift id , left_inv := , right_inv := }
            Instances For
              def conjugatesOf {α : Type u} [Monoid α] (a : α) :
              Set α

              Given an element a, conjugatesOf a is the set of conjugates.

              Equations
              Instances For
                theorem mem_conjugatesOf_self {α : Type u} [Monoid α] {a : α} :
                theorem IsConj.conjugatesOf_eq {α : Type u} [Monoid α] {a : α} {b : α} (ab : IsConj a b) :
                theorem isConj_iff_conjugatesOf_eq {α : Type u} [Monoid α] {a : α} {b : α} :
                def ConjClasses.carrier {α : Type u} [Monoid α] :
                ConjClasses αSet α

                Given a conjugacy class a, carrier a is the set it represents.

                Equations
                Instances For
                  theorem ConjClasses.carrier_eq_preimage_mk {α : Type u} [Monoid α] {a : ConjClasses α} :
                  ConjClasses.carrier a = ConjClasses.mk ⁻¹' {a}