Documentation

Mathlib.Algebra.Group.Semiconj.Defs

Semiconjugate elements of a semigroup #

Main definitions #

We say that x is semiconjugate to y by a (SemiconjBy a x y), if a * x = y * a. In this file we provide operations on SemiconjBy _ _ _.

In the names of these operations, we treat a as the “left” argument, and both x and y as “right” arguments. This way most names in this file agree with the names of the corresponding lemmas for Commute a b = SemiconjBy a b b. As a side effect, some lemmas have only _right version.

Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like rw [(h.pow_right 5).eq] rather than just rw [h.pow_right 5].

This file provides only basic operations (mul_left, mul_right, inv_right etc). Other operations (pow_right, field inverse etc) are in the files that define corresponding notions.

def AddSemiconjBy {M : Type u_2} [Add M] (a : M) (x : M) (y : M) :

x is additive semiconjugate to y by a if a + x = y + a

Equations
Instances For
    def SemiconjBy {M : Type u_2} [Mul M] (a : M) (x : M) (y : M) :

    x is semiconjugate to y by a, if a * x = y * a.

    Equations
    Instances For
      theorem AddSemiconjBy.eq {S : Type u_1} [Add S] {a : S} {x : S} {y : S} (h : AddSemiconjBy a x y) :
      a + x = y + a

      Equality behind AddSemiconjBy a x y; useful for rewriting.

      theorem SemiconjBy.eq {S : Type u_1} [Mul S] {a : S} {x : S} {y : S} (h : SemiconjBy a x y) :
      a * x = y * a

      Equality behind SemiconjBy a x y; useful for rewriting.

      @[simp]
      theorem AddSemiconjBy.add_right {S : Type u_1} [AddSemigroup S] {a : S} {x : S} {y : S} {x' : S} {y' : S} (h : AddSemiconjBy a x y) (h' : AddSemiconjBy a x' y') :
      AddSemiconjBy a (x + x') (y + y')

      If a semiconjugates x to y and x' to y', then it semiconjugates x + x' to y + y'.

      @[simp]
      theorem SemiconjBy.mul_right {S : Type u_1} [Semigroup S] {a : S} {x : S} {y : S} {x' : S} {y' : S} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
      SemiconjBy a (x * x') (y * y')

      If a semiconjugates x to y and x' to y', then it semiconjugates x * x' to y * y'.

      theorem AddSemiconjBy.add_left {S : Type u_1} [AddSemigroup S] {a : S} {b : S} {x : S} {y : S} {z : S} (ha : AddSemiconjBy a y z) (hb : AddSemiconjBy b x y) :
      AddSemiconjBy (a + b) x z

      If b semiconjugates x to y and a semiconjugates y to z, then a + b semiconjugates x to z.

      theorem SemiconjBy.mul_left {S : Type u_1} [Semigroup S] {a : S} {b : S} {x : S} {y : S} {z : S} (ha : SemiconjBy a y z) (hb : SemiconjBy b x y) :
      SemiconjBy (a * b) x z

      If b semiconjugates x to y and a semiconjugates y to z, then a * b semiconjugates x to z.

      theorem AddSemiconjBy.transitive {S : Type u_1} [AddSemigroup S] :
      Transitive fun (a b : S) => ∃ (c : S), AddSemiconjBy c a b

      The relation “there exists an element that semiconjugates a to b” on an additive semigroup is transitive.

      theorem SemiconjBy.transitive {S : Type u_1} [Semigroup S] :
      Transitive fun (a b : S) => ∃ (c : S), SemiconjBy c a b

      The relation “there exists an element that semiconjugates a to b” on a semigroup is transitive.

      @[simp]
      theorem AddSemiconjBy.zero_right {M : Type u_2} [AddZeroClass M] (a : M) :

      Any element semiconjugates 0 to 0.

      @[simp]
      theorem SemiconjBy.one_right {M : Type u_2} [MulOneClass M] (a : M) :

      Any element semiconjugates 1 to 1.

      @[simp]
      theorem AddSemiconjBy.zero_left {M : Type u_2} [AddZeroClass M] (x : M) :

      Zero semiconjugates any element to itself.

      @[simp]
      theorem SemiconjBy.one_left {M : Type u_2} [MulOneClass M] (x : M) :

      One semiconjugates any element to itself.

      theorem AddSemiconjBy.reflexive {M : Type u_2} [AddZeroClass M] :
      Reflexive fun (a b : M) => ∃ (c : M), AddSemiconjBy c a b

      The relation “there exists an element that semiconjugates a to b” on an additive monoid (or, more generally, on an AddZeroClass type) is reflexive.

      theorem SemiconjBy.reflexive {M : Type u_2} [MulOneClass M] :
      Reflexive fun (a b : M) => ∃ (c : M), SemiconjBy c a b

      The relation “there exists an element that semiconjugates a to b” on a monoid (or, more generally, on MulOneClass type) is reflexive.

      @[simp]
      theorem AddSemiconjBy.nsmul_right {M : Type u_2} [AddMonoid M] {a : M} {x : M} {y : M} (h : AddSemiconjBy a x y) (n : ) :
      AddSemiconjBy a (n x) (n y)
      @[simp]
      theorem SemiconjBy.pow_right {M : Type u_2} [Monoid M] {a : M} {x : M} {y : M} (h : SemiconjBy a x y) (n : ) :
      SemiconjBy a (x ^ n) (y ^ n)
      theorem AddSemiconjBy.conj_mk {G : Type u_3} [AddGroup G] (a : G) (x : G) :
      AddSemiconjBy a x (a + x + -a)

      a semiconjugates x to a + x + -a.

      theorem SemiconjBy.conj_mk {G : Type u_3} [Group G] (a : G) (x : G) :
      SemiconjBy a x (a * x * a⁻¹)

      a semiconjugates x to a * x * a⁻¹.

      @[simp]
      theorem AddSemiconjBy.conj_iff {G : Type u_3} [AddGroup G] {a : G} {x : G} {y : G} {b : G} :
      AddSemiconjBy (b + a + -b) (b + x + -b) (b + y + -b) AddSemiconjBy a x y
      @[simp]
      theorem SemiconjBy.conj_iff {G : Type u_3} [Group G] {a : G} {x : G} {y : G} {b : G} :
      SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) SemiconjBy a x y
      @[simp]
      theorem addSemiconjBy_iff_eq {M : Type u_2} [AddCancelCommMonoid M] {a : M} {x : M} {y : M} :
      AddSemiconjBy a x y x = y
      @[simp]
      theorem semiconjBy_iff_eq {M : Type u_2} [CancelCommMonoid M] {a : M} {x : M} {y : M} :
      SemiconjBy a x y x = y