Documentation

Mathlib.Algebra.Group.Semiconj

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_1} [inst : Add M] (a : M) (x : M) (y : M) :

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

Equations

AddSemiconjBy a x y = (a + x = y + a)

def SemiconjBy {M : Type u_1} [inst : Mul M] (a : M) (x : M) (y : M) :

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

Equations

SemiconjBy a x y = (a * x = y * a)

theorem AddSemiconjBy.eq {S : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : AddSemigroup S] :

Transitive fun a b => ∃ c, AddSemiconjBy c a b

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

abbrev AddSemiconjBy.transitive.match_1 {S : Type u_1} [inst : AddSemigroup S] (motive : (x x_1 x_2 : S) → (∃ c, AddSemiconjBy c x x_1) → (∃ c, AddSemiconjBy c x_1 x_2) → Prop) :

(x x_1 x_2 : S) → (x_3 : ∃ c, AddSemiconjBy c x x_1) → (x_4 : ∃ c, AddSemiconjBy c x_1 x_2) → ((x x_5 x_6 x_7 : S) → (hx : AddSemiconjBy x_7 x x_5) → (y : S) → (hy : AddSemiconjBy y x_5 x_6) → motive x x_5 x_6 (_ : ∃ c, AddSemiconjBy c x x_5) (_ : ∃ c, AddSemiconjBy c x_5 x_6)) → motive x x_1 x_2 x_3 x_4

Equations

AddSemiconjBy.transitive.match_1 motive x x x x x h_1 = Exists.casesOn x fun w h => Exists.casesOn x fun w_1 h_1 => h_1 x x x w h w_1 h_1

theorem SemiconjBy.transitive {S : Type u_1} [inst : Semigroup S] :

Transitive fun a b => ∃ c, 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_1} [inst : AddZeroClass M] (a : M) :

AddSemiconjBy a 0 0

Any element semiconjugates 0 to 0.

@[simp]

theorem SemiconjBy.one_right {M : Type u_1} [inst : MulOneClass M] (a : M) :

SemiconjBy a 1 1

Any element semiconjugates 1 to 1.

@[simp]

theorem AddSemiconjBy.zero_left {M : Type u_1} [inst : AddZeroClass M] (x : M) :

AddSemiconjBy 0 x x

Zero semiconjugates any element to itself.

@[simp]

theorem SemiconjBy.one_left {M : Type u_1} [inst : MulOneClass M] (x : M) :

SemiconjBy 1 x x

One semiconjugates any element to itself.

theorem AddSemiconjBy.reflexive {M : Type u_1} [inst : AddZeroClass M] :

Reflexive fun a b => ∃ c, AddSemiconjBy c a b

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

theorem SemiconjBy.reflexive {M : Type u_1} [inst : MulOneClass M] :

Reflexive fun a b => ∃ c, 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.

theorem AddSemiconjBy.addUnits_neg_right {M : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Monoid M] {a : Mˣ} {x : M} {y : M} :

SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y

theorem AddSemiconjBy.addUnits_val {M : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Monoid M] {a : Mˣ} {x : Mˣ} {y : Mˣ} :

SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y

@[simp]

theorem AddSemiconjBy.nsmul_right {M : Type u_1} [inst : 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_1} [inst : Monoid M] {a : M} {x : M} {y : M} (h : SemiconjBy a x y) (n : ℕ) :

SemiconjBy a (x ^ n) (y ^ n)

@[simp]

theorem AddSemiconjBy.neg_neg_symm_iff {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {x : G} {y : G} :

AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x

@[simp]

theorem SemiconjBy.inv_inv_symm_iff {G : Type u_1} [inst : DivisionMonoid G] {a : G} {x : G} {y : G} :

SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

theorem AddSemiconjBy.neg_neg_symm {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {x : G} {y : G} :

AddSemiconjBy a x y → AddSemiconjBy (-a) (-y) (-x)

theorem SemiconjBy.inv_inv_symm {G : Type u_1} [inst : DivisionMonoid G] {a : G} {x : G} {y : G} :

SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹

@[simp]

theorem AddSemiconjBy.neg_right_iff {G : Type u_1} [inst : 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} [inst : Group G] {a : G} {x : G} {y : G} :

SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

theorem AddSemiconjBy.neg_right {G : Type u_1} [inst : AddGroup G] {a : G} {x : G} {y : G} :

AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)

theorem SemiconjBy.inv_right {G : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Group G] {a : G} {x : G} {y : G} :

SemiconjBy a x y → SemiconjBy a⁻¹ y x

theorem AddSemiconjBy.conj_mk {G : Type u_1} [inst : 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_1} [inst : Group G] (a : G) (x : G) :

SemiconjBy a x (a * x * a⁻¹)

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

@[simp]

theorem addSemiconjBy_iff_eq {M : Type u_1} [inst : AddCancelCommMonoid M] {a : M} {x : M} {y : M} :

AddSemiconjBy a x y ↔ x = y

@[simp]

theorem semiconjBy_iff_eq {M : Type u_1} [inst : CancelCommMonoid M] {a : M} {x : M} {y : M} :

SemiconjBy a x y ↔ x = y

theorem AddUnits.mk_addSemiconjBy {M : Type u_1} [inst : 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} [inst : Monoid M] (u : Mˣ) (x : M) :

SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)

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