mathlib documentation

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
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
@[protected]
theorem semiconj_by.eq {S : Type u} [has_mul S] {a x y : S} (h : semiconj_by a 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 : add_semiconj_by a x 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 : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by 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 add_semiconj_by.add_right {S : Type u} [add_semigroup S] {a x y x' y' : S} (h : add_semiconj_by a x y) (h' : add_semiconj_by a x' y') :
add_semiconj_by a (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 : semiconj_by a y z) (hb : semiconj_by b 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} [add_semigroup S] {a b x y z : S} (ha : add_semiconj_by a y z) (hb : add_semiconj_by b x 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), semiconj_by c 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} [add_semigroup S] :
transitive (λ (a b : S), ∃ (c : S), add_semiconj_by c a 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} [add_zero_class M] (a : M) :

Any element additively semiconjugates 0 to 0.

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

Any element semiconjugates 1 to 1.

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

Zero additively semiconjugates any element to itself.

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

One semiconjugates any element to itself.

@[protected]
theorem semiconj_by.reflexive {M : Type u} [mul_one_class M] :
reflexive (λ (a b : M), ∃ (c : M), semiconj_by c 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} [add_zero_class M] :
reflexive (λ (a b : M), ∃ (c : M), add_semiconj_by c a 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.

theorem add_semiconj_by.add_units_neg_right {M : Type u} [add_monoid M] {a : M} {x y : add_units M} (h : add_semiconj_by a 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 : semiconj_by a x y) :

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

@[simp]
@[simp]
theorem semiconj_by.units_inv_right_iff {M : Type u} [monoid M] {a : M} {x y : Mˣ} :
theorem add_semiconj_by.add_units_neg_symm_left {M : Type u} [add_monoid M] {a : add_units M} {x y : M} (h : add_semiconj_by a x y) :

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 : semiconj_by a x y) :

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

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

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

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

a semiconjugates x to a + x + -a.

@[simp]
theorem semiconj_by_iff_eq {M : Type u} [cancel_comm_monoid M] {a x y : M} :
semiconj_by a x y x = y
@[simp]
theorem add_semiconj_by_iff_eq {M : Type u} [add_cancel_comm_monoid M] {a x y : M} :
theorem add_units.mk_semiconj_by {M : Type u} [add_monoid M] (u : add_units M) (x : M) :

a semiconjugates x to a + x + -a.

theorem units.mk_semiconj_by {M : Type u} [monoid M] (u : Mˣ) (x : M) :
semiconj_by u x (((u) * x) * u⁻¹)

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