mathlib3 documentation

algebra.group.semiconj

Semiconjugate elements of a semigroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

add_semiconj_by a x 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

semiconj_by a x y = (a * x = y * a)

@[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) :

add_semiconj_by a 0 0

Any element additively semiconjugates 0 to 0.

@[simp]

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

semiconj_by a 1 1

Any element semiconjugates 1 to 1.

@[simp]

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

add_semiconj_by 0 x x

Zero additively semiconjugates any element to itself.

@[simp]

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

semiconj_by 1 x x

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) :

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) :

semiconj_by a ↑x⁻¹ ↑y⁻¹

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

@[simp]

theorem add_semiconj_by.add_units_neg_right_iff {M : Type u} [add_monoid M] {a : M} {x y : add_units M} :

add_semiconj_by a (↑-x) (↑-y) ↔ add_semiconj_by a ↑x ↑y

@[simp]

theorem semiconj_by.units_inv_right_iff {M : Type u} [monoid M] {a : M} {x y : Mˣ} :

semiconj_by a ↑x⁻¹ ↑y⁻¹ ↔ semiconj_by a ↑x ↑y

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) :

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

semiconj_by ↑a⁻¹ y x

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

@[simp]

theorem add_semiconj_by.add_units_neg_symm_left_iff {M : Type u} [add_monoid M] {a : add_units M} {x y : M} :

add_semiconj_by (↑-a) y x ↔ add_semiconj_by ↑a x y

@[simp]

theorem semiconj_by.units_inv_symm_left_iff {M : Type u} [monoid M] {a : Mˣ} {x y : M} :

semiconj_by ↑a⁻¹ y x ↔ semiconj_by ↑a x y

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

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) :

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) :

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) :

add_semiconj_by a x y

@[simp]

theorem add_semiconj_by.add_units_coe_iff {M : Type u} [add_monoid M] {a x y : add_units M} :

add_semiconj_by ↑a ↑x ↑y ↔ add_semiconj_by a x y

@[simp]

theorem semiconj_by.units_coe_iff {M : Type u} [monoid M] {a x y : Mˣ} :

semiconj_by ↑a ↑x ↑y ↔ semiconj_by a x y

@[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 semiconj_by.inv_inv_symm_iff {G : Type u_1} [division_monoid G] {a x y : G} :

semiconj_by a⁻¹ x⁻¹ y⁻¹ ↔ semiconj_by a y x

@[simp]

theorem add_semiconj_by.neg_neg_symm_iff {G : Type u_1} [subtraction_monoid G] {a x y : G} :

add_semiconj_by (-a) (-x) (-y) ↔ add_semiconj_by a y x

theorem add_semiconj_by.neg_neg_symm {G : Type u_1} [subtraction_monoid G] {a x y : G} :

add_semiconj_by a x y → add_semiconj_by (-a) (-y) (-x)

theorem semiconj_by.inv_inv_symm {G : Type u_1} [division_monoid G] {a x y : G} :

semiconj_by a x y → semiconj_by a⁻¹ y⁻¹ x⁻¹

@[simp]

theorem add_semiconj_by.neg_right_iff {G : Type u_1} [add_group G] {a x y : G} :

add_semiconj_by a (-x) (-y) ↔ add_semiconj_by a x y

@[simp]

theorem semiconj_by.inv_right_iff {G : Type u_1} [group G] {a x y : G} :

semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y

theorem add_semiconj_by.neg_right {G : Type u_1} [add_group G] {a x y : G} :

add_semiconj_by a x y → add_semiconj_by a (-x) (-y)

theorem semiconj_by.inv_right {G : Type u_1} [group G] {a x y : G} :

semiconj_by a x y → semiconj_by a x⁻¹ y⁻¹

@[simp]

theorem semiconj_by.inv_symm_left_iff {G : Type u_1} [group G] {a x y : G} :

semiconj_by a⁻¹ y x ↔ semiconj_by a x y

@[simp]

theorem add_semiconj_by.neg_symm_left_iff {G : Type u_1} [add_group G] {a x y : G} :

add_semiconj_by (-a) y x ↔ add_semiconj_by a x y

theorem add_semiconj_by.neg_symm_left {G : Type u_1} [add_group G] {a x y : G} :

add_semiconj_by a x y → add_semiconj_by (-a) y x

theorem semiconj_by.inv_symm_left {G : Type u_1} [group G] {a x y : G} :

semiconj_by a x y → semiconj_by a⁻¹ y x

theorem semiconj_by.conj_mk {G : Type u_1} [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_1} [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} :

add_semiconj_by a x y ↔ x = y

theorem add_units.mk_semiconj_by {M : Type u} [add_monoid M] (u : add_units M) (x : M) :

add_semiconj_by ↑u x (↑u + x + ↑-u)

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⁻¹.