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
      theorem IsConj.pow {α : Type u} [Monoid α] {a b : α} (n : ) :
      IsConj a bIsConj (a ^ n) (b ^ n)
      @[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} [Monoid α] {a : α} :
      IsConj 1 a a = 1
      @[simp]
      theorem isConj_one_left {α : Type u} [Monoid α] {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⁻¹
      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
                    theorem ConjClasses.quot_mk_eq_mk {α : Type u} [Monoid α] (a : α) :
                    theorem ConjClasses.forall_isConj {α : Type u} [Monoid α] {p : ConjClasses αProp} :
                    (∀ (a : ConjClasses α), p a) ∀ (a : α), p (ConjClasses.mk a)
                    instance ConjClasses.instOne {α : Type u} [Monoid α] :
                    Equations
                      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) :

                          The bijection between a CommGroup and its ConjClasses.

                          Equations
                            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) :
                                  def ConjClasses.carrier {α : Type u} [Monoid α] :
                                  ConjClasses αSet α

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

                                  Equations
                                    Instances For