# mathlibdocumentation

algebra.group.semiconj

# Semiconjugate elements of a semigroup #

## Main definitions #

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

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 = semiconj_by 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 add_semiconj_by {M : Type u} [has_add M] (a x y : M) :
Prop

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

Equations
• y = (a + x = y + a)
def semiconj_by {M : Type u} [has_mul M] (a x y : M) :
Prop

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

Equations
• x y = (a * x = y * a)
@[protected]
theorem semiconj_by.eq {S : Type u} [has_mul S] {a x y : S} (h : x y) :
a * x = y * a

Equality behind semiconj_by a x y; useful for rewriting.

@[protected]
theorem add_semiconj_by.eq {S : Type u} [has_add S] {a x y : S} (h : y) :
a + x = y + a

Equality behind add_semiconj_by a x y; useful for rewriting.

@[simp]
theorem semiconj_by.mul_right {S : Type u} [semigroup S] {a x y x' y' : S} (h : x y) (h' : x' y') :
(x * x') (y * y')

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

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

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

theorem semiconj_by.mul_left {S : Type u} [semigroup S] {a b x y z : S} (ha : y z) (hb : x y) :
semiconj_by (a * b) x z

If both a and b semiconjugate x to y, then so does a * b.

theorem add_semiconj_by.add_left {S : Type u} {a b x y z : S} (ha : z) (hb : y) :
add_semiconj_by (a + b) x z

If both a and b semiconjugate x to y, then so does a + b.

@[protected]
theorem semiconj_by.transitive {S : Type u} [semigroup S] :
transitive (λ (a b : S), ∃ (c : S), a b)

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

@[protected]
theorem add_semiconj_by.transitive {S : Type u}  :
transitive (λ (a b : S), ∃ (c : S), b)

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

@[simp]
theorem add_semiconj_by.zero_right {M : Type u} (a : M) :
0

Any element additively semiconjugates 0 to 0.

@[simp]
theorem semiconj_by.one_right {M : Type u} (a : M) :
1 1

Any element semiconjugates 1 to 1.

@[simp]
theorem add_semiconj_by.zero_left {M : Type u} (x : M) :
x

Zero additively semiconjugates any element to itself.

@[simp]
theorem semiconj_by.one_left {M : Type u} (x : M) :
x x

One semiconjugates any element to itself.

@[protected]
theorem semiconj_by.reflexive {M : Type u}  :
reflexive (λ (a b : M), ∃ (c : M), a b)

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

@[protected]
theorem add_semiconj_by.reflexive {M : Type u}  :
reflexive (λ (a b : M), ∃ (c : M), b)

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

(-x) (-y)

If a semiconjugates an additive unit x to an additive unit y, then it semiconjugates -x to -y.

theorem semiconj_by.units_inv_right {M : Type u} [monoid M] {a : M} {x y : Mˣ} (h : x y) :

If a semiconjugates a unit x to a unit y, then it semiconjugates x⁻¹ to y⁻¹.

@[simp]
(-x) (-y) y
@[simp]
theorem semiconj_by.units_inv_right_iff {M : Type u} [monoid M] {a : M} {x y : Mˣ} :
y x

If an additive unit a semiconjugates x to y, then -a semiconjugates y to x.

theorem semiconj_by.units_inv_symm_left {M : Type u} [monoid M] {a : Mˣ} {x y : M} (h : x y) :
x

If a unit a semiconjugates x to y, then a⁻¹ semiconjugates y to x.

@[simp]
y x y
@[simp]
theorem semiconj_by.units_inv_symm_left_iff {M : Type u} [monoid M] {a : Mˣ} {x y : M} :
x x y
theorem semiconj_by.units_coe {M : Type u} [monoid M] {a x y : Mˣ} (h : x y) :
y
y
theorem semiconj_by.units_of_coe {M : Type u} [monoid M] {a x y : Mˣ} (h : y) :
x y
y
@[simp]
y y
@[simp]
theorem semiconj_by.units_coe_iff {M : Type u} [monoid M] {a x y : Mˣ} :
y x y
@[simp]
theorem add_semiconj_by.nsmul_right {M : Type u} [add_monoid M] {a x y : M} (h : y) (n : ) :
(n x) (n y)
@[simp]
theorem semiconj_by.pow_right {M : Type u} [monoid M] {a x y : M} (h : x y) (n : ) :
(x ^ n) (y ^ n)
@[simp]
theorem semiconj_by.inv_inv_symm_iff {G : Type u_1} {a x y : G} :
y⁻¹ y x
@[simp]
theorem add_semiconj_by.neg_neg_symm_iff {G : Type u_1} {a x y : G} :
(-x) (-y) x
theorem add_semiconj_by.neg_neg_symm {G : Type u_1} {a x y : G} :
y (-y) (-x)
theorem semiconj_by.inv_inv_symm {G : Type u_1} {a x y : G} :
x y x⁻¹
@[simp]
theorem add_semiconj_by.neg_right_iff {G : Type u_1} [add_group G] {a x y : G} :
(-x) (-y) y
@[simp]
theorem semiconj_by.inv_right_iff {G : Type u_1} [group G] {a x y : G} :
y⁻¹ x y
theorem add_semiconj_by.neg_right {G : Type u_1} [add_group G] {a x y : G} :
y (-x) (-y)
theorem semiconj_by.inv_right {G : Type u_1} [group G] {a x y : G} :
x y y⁻¹
@[simp]
theorem semiconj_by.inv_symm_left_iff {G : Type u_1} [group G] {a x y : G} :
x x y
@[simp]
theorem add_semiconj_by.neg_symm_left_iff {G : Type u_1} [add_group G] {a x y : G} :
y x y
theorem add_semiconj_by.neg_symm_left {G : Type u_1} [add_group G] {a x y : G} :
y y x
theorem semiconj_by.inv_symm_left {G : Type u_1} [group G] {a x y : G} :
x y x
theorem semiconj_by.conj_mk {G : Type u_1} [group G] (a x : G) :
x (a * x * a⁻¹)

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

theorem add_semiconj_by.conj_mk {G : Type u_1} [add_group G] (a x : G) :
(a + x + -a)

a semiconjugates x to a + x + -a.

@[simp]
theorem semiconj_by_iff_eq {M : Type u} {a x y : M} :
x y x = y
@[simp]
theorem add_semiconj_by_iff_eq {M : Type u} {a x y : M} :
y x = y
a semiconjugates x to a + x + -a.
a semiconjugates x to a * x * a⁻¹.