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.

theorem AddSemiconjBy.addUnits_neg_right {M : Type u_1} [AddMonoid M] {a : M} {x : AddUnits M} {y : AddUnits M} (h : AddSemiconjBy a ↑x ↑y) : AddSemiconjBy a ↑(-x) ↑(-y)

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

theorem SemiconjBy.units_inv_right {M : Type u_1} [Monoid M] {a : M} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a ↑x ↑y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹

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

@[simp]

theorem AddSemiconjBy.addUnits_neg_right_iff {M : Type u_1} [AddMonoid M] {a : M} {x : AddUnits M} {y : AddUnits M} : AddSemiconjBy a ↑(-x) ↑(-y) ↔ AddSemiconjBy a ↑x ↑y

@[simp]

theorem SemiconjBy.units_inv_right_iff {M : Type u_1} [Monoid M] {a : M} {x : Mˣ} {y : Mˣ} : SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y

theorem AddSemiconjBy.addUnits_neg_symm_left {M : Type u_1} [AddMonoid M] {a : AddUnits M} {x : M} {y : M} (h : AddSemiconjBy (↑a) x y) : AddSemiconjBy (↑(-a)) y x

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

theorem SemiconjBy.units_inv_symm_left {M : Type u_1} [Monoid M] {a : Mˣ} {x : M} {y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x

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

@[simp]

theorem AddSemiconjBy.addUnits_neg_symm_left_iff {M : Type u_1} [AddMonoid M] {a : AddUnits M} {x : M} {y : M} : AddSemiconjBy (↑(-a)) y x ↔ AddSemiconjBy (↑a) x y

@[simp]

theorem SemiconjBy.units_inv_symm_left_iff {M : Type u_1} [Monoid M] {a : Mˣ} {x : M} {y : M} : SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y

theorem AddSemiconjBy.addUnits_val {M : Type u_1} [AddMonoid M] {a : AddUnits M} {x : AddUnits M} {y : AddUnits M} (h : AddSemiconjBy a x y) : AddSemiconjBy ↑a ↑x ↑y

theorem SemiconjBy.units_val {M : Type u_1} [Monoid M] {a : Mˣ} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy ↑a ↑x ↑y

theorem AddSemiconjBy.addUnits_of_val {M : Type u_1} [AddMonoid M] {a : AddUnits M} {x : AddUnits M} {y : AddUnits M} (h : AddSemiconjBy ↑a ↑x ↑y) : AddSemiconjBy a x y

theorem SemiconjBy.units_of_val {M : Type u_1} [Monoid M] {a : Mˣ} {x : Mˣ} {y : Mˣ} (h : SemiconjBy ↑a ↑x ↑y) : SemiconjBy a x y

@[simp]

theorem AddSemiconjBy.addUnits_val_iff {M : Type u_1} [AddMonoid M] {a : AddUnits M} {x : AddUnits M} {y : AddUnits M} : AddSemiconjBy ↑a ↑x ↑y ↔ AddSemiconjBy a x y

@[simp]

theorem SemiconjBy.units_val_iff {M : Type u_1} [Monoid M] {a : Mˣ} {x : Mˣ} {y : Mˣ} : SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y

@[simp]

theorem AddSemiconjBy.neg_right_iff {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} : AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y

@[simp]

theorem SemiconjBy.inv_right_iff {G : Type u_1} [Group G] {a : G} {x : G} {y : G} : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

theorem AddSemiconjBy.neg_right {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} : AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)

theorem SemiconjBy.inv_right {G : Type u_1} [Group G] {a : G} {x : G} {y : G} : SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹

@[simp]

theorem AddSemiconjBy.neg_symm_left_iff {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} : AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y

@[simp]

theorem SemiconjBy.inv_symm_left_iff {G : Type u_1} [Group G] {a : G} {x : G} {y : G} : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

theorem AddSemiconjBy.neg_symm_left {G : Type u_1} [AddGroup G] {a : G} {x : G} {y : G} : AddSemiconjBy a x y → AddSemiconjBy (-a) y x

theorem SemiconjBy.inv_symm_left {G : Type u_1} [Group G] {a : G} {x : G} {y : G} : SemiconjBy a x y → SemiconjBy a⁻¹ y x

theorem AddUnits.mk_addSemiconjBy {M : Type u_1} [AddMonoid M] (u : AddUnits M) (x : M) : AddSemiconjBy (↑u) x (↑u + x + ↑(-u))

a semiconjugates x to a + x + -a.

theorem Units.mk_semiconjBy {M : Type u_1} [Monoid M] (u : Mˣ) (x : M) : SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)

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