Mathlib.Algebra.Group.Commute.Units

Commute.units_inv_right theorem

: Commute a u → Commute a ↑u⁻¹

Full source

@[to_additive]
theorem units_inv_right : Commute a u → Commute a ↑u⁻¹ :=
  SemiconjBy.units_inv_right

Commutation with Unit Implies Commutation with Unit Inverse: $a \cdot u = u \cdot a \to a \cdot u^{-1} = u^{-1} \cdot a$

Informal description

For any element $a$ in a monoid $M$ and any unit $u \in M^\times$, if $a$ commutes with $u$, then $a$ also commutes with the inverse $u^{-1}$. That is, if $a \cdot u = u \cdot a$, then $a \cdot u^{-1} = u^{-1} \cdot a$.

Commute.units_inv_right_iff theorem

: Commute a ↑u⁻¹ ↔ Commute a u

Full source

@[to_additive (attr := simp)]
theorem units_inv_right_iff : CommuteCommute a ↑u⁻¹ ↔ Commute a u :=
  SemiconjBy.units_inv_right_iff

Commutation with Unit Inverse iff Commutation with Unit: $a \cdot u^{-1} = u^{-1} \cdot a \leftrightarrow a \cdot u = u \cdot a$

Informal description

For any element $a$ in a monoid $M$ and any unit $u \in M^\times$, the element $a$ commutes with the inverse $u^{-1}$ if and only if $a$ commutes with $u$. That is, $a \cdot u^{-1} = u^{-1} \cdot a$ if and only if $a \cdot u = u \cdot a$.

Commute.units_inv_left theorem

: Commute (↑u) a → Commute (↑u⁻¹) a

Full source

@[to_additive]
theorem units_inv_left : Commute (↑u) a → Commute (↑u⁻¹) a :=
  SemiconjBy.units_inv_symm_left

Commutation with Unit Implies Commutation with Unit Inverse: $u \cdot a = a \cdot u \to u^{-1} \cdot a = a \cdot u^{-1}$

Informal description

For any element $a$ in a monoid $M$ and any unit $u \in M^\times$, if $u$ commutes with $a$, then the inverse $u^{-1}$ also commutes with $a$. That is, if $u \cdot a = a \cdot u$, then $u^{-1} \cdot a = a \cdot u^{-1}$.

Commute.units_inv_left_iff theorem

: Commute (↑u⁻¹) a ↔ Commute (↑u) a

Full source

@[to_additive (attr := simp)]
theorem units_inv_left_iff : CommuteCommute (↑u⁻¹) a ↔ Commute (↑u) a :=
  SemiconjBy.units_inv_symm_left_iff

Commutation with Unit Inverse iff Commutation with Unit: $a \cdot u^{-1} = u^{-1} \cdot a \leftrightarrow a \cdot u = u \cdot a$

Informal description

For any element $a$ in a monoid $M$ and any unit $u \in M^\times$, the element $a$ commutes with the inverse $u^{-1}$ if and only if $a$ commutes with $u$. In other words, $a \cdot u^{-1} = u^{-1} \cdot a$ holds if and only if $a \cdot u = u \cdot a$ holds.

Commute.units_val theorem

: Commute u₁ u₂ → Commute (u₁ : M) u₂

Full source

@[to_additive]
theorem units_val : Commute u₁ u₂ → Commute (u₁ : M) u₂ :=
  SemiconjBy.units_val

Commutation of Units in Monoid Implies Commutation of Their Underlying Elements

Informal description

For any two units $u_1$ and $u_2$ in a monoid $M$, if $u_1$ and $u_2$ commute as elements of the group of units $M^\times$, then they also commute when considered as elements of $M$. That is, if $u_1 \cdot u_2 = u_2 \cdot u_1$ holds in $M^\times$, then $(u_1 : M) \cdot u_2 = u_2 \cdot (u_1 : M)$ holds in $M$.

Commute.units_of_val theorem

: Commute (u₁ : M) u₂ → Commute u₁ u₂

Full source

@[to_additive]
theorem units_of_val : Commute (u₁ : M) u₂ → Commute u₁ u₂ :=
  SemiconjBy.units_of_val

Commutation of Underlying Elements Implies Commutation of Units: $(u_1 : M) \cdot u_2 = u_2 \cdot (u_1 : M) \to u_1 \cdot u_2 = u_2 \cdot u_1$

Informal description

For any two units $u_1$ and $u_2$ in a monoid $M$, if the underlying elements $(u_1 : M)$ and $u_2$ commute (i.e., $(u_1 : M) \cdot u_2 = u_2 \cdot (u_1 : M)$), then the units $u_1$ and $u_2$ themselves commute in the group of units $M^\times$ (i.e., $u_1 \cdot u_2 = u_2 \cdot u_1$).

Commute.units_val_iff theorem

: Commute (u₁ : M) u₂ ↔ Commute u₁ u₂

Full source

@[to_additive (attr := simp)]
theorem units_val_iff : CommuteCommute (u₁ : M) u₂ ↔ Commute u₁ u₂ :=
  SemiconjBy.units_val_iff

Commutation of Units and Their Underlying Elements

Informal description

For any two units $u_1$ and $u_2$ in a monoid $M$, the elements $u_1$ and $u_2$ commute (i.e., $u_1 \cdot u_2 = u_2 \cdot u_1$) if and only if the units themselves commute in the group of units $M^\times$.

Units.leftOfMul definition

(u : Mˣ) (a b : M) (hu : a * b = u) (hc : Commute a b) : Mˣ

Full source

/-- If the product of two commuting elements is a unit, then the left multiplier is a unit. -/
@[to_additive "If the sum of two commuting elements is an additive unit, then the left summand is
an additive unit."]
def Units.leftOfMul (u : Mˣ) (a b : M) (hu : a * b = u) (hc : Commute a b) : Mˣ where
  val := a
  inv := b * ↑u⁻¹
  val_inv := by rw [← mul_assoc, hu, u.mul_inv]
  inv_val := by
    have : Commute a u := hu ▸ (Commute.refl _).mul_right hc
    rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]

Left factor of a commuting product of elements is a unit when the product is a unit

Informal description

Given a unit $ u $ in a monoid $ M $ and elements $ a, b \in M $ such that $ a * b = u $ and $ a $ commutes with $ b $, the element $ a $ is a unit. The inverse of $ a $ is given by $ b * u^{-1} $.

Units.rightOfMul definition

(u : Mˣ) (a b : M) (hu : a * b = u) (hc : Commute a b) : Mˣ

Full source

/-- If the product of two commuting elements is a unit, then the right multiplier is a unit. -/
@[to_additive "If the sum of two commuting elements is an additive unit, then the right summand
is an additive unit."]
def Units.rightOfMul (u : Mˣ) (a b : M) (hu : a * b = u) (hc : Commute a b) : Mˣ :=
  u.leftOfMul b a (hc.eq ▸ hu) hc.symm

Right factor of a commuting product of elements is a unit when the product is a unit

Informal description

Given a unit $ u $ in a monoid $ M $ and elements $ a, b \in M $ such that $ a * b = u $ and $ a $ commutes with $ b $, the element $ b $ is a unit. The inverse of $ b $ is given by $ a * u^{-1} $.

Commute.isUnit_mul_iff theorem

(h : Commute a b) : IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b

Full source

@[to_additive]
theorem Commute.isUnit_mul_iff (h : Commute a b) : IsUnitIsUnit (a * b) ↔ IsUnit a ∧ IsUnit b :=
  ⟨fun ⟨u, hu⟩ => ⟨(u.leftOfMul a b hu.symm h).isUnit, (u.rightOfMul a b hu.symm h).isUnit⟩,
  fun H => H.1.mul H.2⟩

Product of Commuting Elements is a Unit iff Both Elements are Units

Informal description

For any two commuting elements $a$ and $b$ in a monoid $M$, the product $a \cdot b$ is a unit if and only if both $a$ and $b$ are units.

isUnit_mul_self_iff theorem

: IsUnit (a * a) ↔ IsUnit a

Full source

@[to_additive (attr := simp)]
theorem isUnit_mul_self_iff : IsUnitIsUnit (a * a) ↔ IsUnit a :=
  (Commute.refl a).isUnit_mul_iff.trans and_self_iff

Square of an Element is a Unit iff the Element is a Unit

Informal description

For any element $a$ in a monoid, the product $a \cdot a$ is a unit if and only if $a$ is a unit.

Commute.units_zpow_right theorem

(h : Commute a u) (m : ℤ) : Commute a ↑(u ^ m)

Full source

@[to_additive (attr := simp)]
lemma Commute.units_zpow_right (h : Commute a u) (m : ℤ) : Commute a ↑(u ^ m) :=
  SemiconjBy.units_zpow_right h m

Commutation with Integer Powers of Units: $a * u^m = u^m * a$

Informal description

Let $a$ and $u$ be elements in a monoid such that $a$ and $u$ commute (i.e., $a * u = u * a$). Then for any integer $m$, $a$ commutes with the $m$-th power of $u$ (i.e., $a * u^m = u^m * a$).

Commute.units_zpow_left theorem

(h : Commute (↑u) a) (m : ℤ) : Commute (↑(u ^ m)) a

Full source

@[to_additive (attr := simp)]
lemma Commute.units_zpow_left (h : Commute ↑u a) (m : ℤ) : Commute ↑(u ^ m) a :=
  (h.symm.units_zpow_right m).symm

Commutation of Integer Powers of Units: $u^m \cdot a = a \cdot u^m$

Informal description

Let $u$ be a unit in a monoid and $a$ an element such that $u$ commutes with $a$ (i.e., $u \cdot a = a \cdot u$). Then for any integer $m$, the $m$-th power of $u$ commutes with $a$ (i.e., $u^m \cdot a = a \cdot u^m$).

Units.ofPow definition

(u : Mˣ) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : x ^ n = u) : Mˣ

Full source

/-- If a natural power of `x` is a unit, then `x` is a unit. -/
@[to_additive "If a natural multiple of `x` is an additive unit, then `x` is an additive unit."]
def Units.ofPow (u : Mˣ) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : x ^ n = u) : Mˣ :=
  u.leftOfMul x (x ^ (n - 1))
    (by rwa [← _root_.pow_succ', Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)])
    (Commute.self_pow _ _)

Unit condition for elements with unit power

Informal description

Given a unit $ u $ in a monoid $ M $, an element $ x \in M $, and a nonzero natural number $ n $ such that $ x^n = u $, the element $ x $ is a unit. The inverse of $ x $ is constructed using the left factor of the product $ x \cdot x^{n-1} = u $, leveraging the fact that $ x $ commutes with its powers.

isUnit_pow_iff theorem

(hn : n ≠ 0) : IsUnit (a ^ n) ↔ IsUnit a

Full source

@[to_additive (attr := simp)] lemma isUnit_pow_iff (hn : n ≠ 0) : IsUnitIsUnit (a ^ n) ↔ IsUnit a :=
  ⟨fun ⟨u, hu⟩ ↦ (u.ofPow a hn hu.symm).isUnit, IsUnit.pow n⟩

Unit Power Equivalence: $a^n$ is a unit iff $a$ is a unit for $n \neq 0$

Informal description

For any element $a$ in a monoid $M$ and any nonzero natural number $n$, the power $a^n$ is a unit if and only if $a$ itself is a unit.

isUnit_pow_succ_iff theorem

: IsUnit (a ^ (n + 1)) ↔ IsUnit a

Full source

@[to_additive]
lemma isUnit_pow_succ_iff : IsUnitIsUnit (a ^ (n + 1)) ↔ IsUnit a := isUnit_pow_iff n.succ_ne_zero

Unit Power Equivalence: $a^{n+1}$ is a unit iff $a$ is a unit

Informal description

For any element $a$ in a monoid $M$ and any natural number $n$, the power $a^{n+1}$ is a unit if and only if $a$ itself is a unit.

isUnit_pow_iff_of_not_isUnit theorem

(hx : ¬IsUnit a) {n : ℕ} : IsUnit (a ^ n) ↔ n = 0

Full source

lemma isUnit_pow_iff_of_not_isUnit (hx : ¬ IsUnit a) {n : ℕ} :
    IsUnitIsUnit (a ^ n) ↔ n = 0 := by
  rcases n with (_|n) <;>
  simp [hx]

Non-unit Elements Have Zeroth Power as Only Unit Power

Informal description

For any element $a$ in a monoid $M$ that is not a unit, and for any natural number $n$, the element $a^n$ is a unit if and only if $n = 0$.

Units.ofPowEqOne definition

(a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0) : Mˣ

Full source

/-- If `a ^ n = 1`, `n ≠ 0`, then `a` is a unit. -/
@[to_additive (attr := simps!) "If `n • x = 0`, `n ≠ 0`, then `x` is an additive unit."]
def Units.ofPowEqOne (a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0) : Mˣ := Units.ofPow 1 a hn ha

Unit from power equaling identity

Informal description

Given an element $a$ in a monoid $M$ and a nonzero natural number $n$ such that $a^n = 1$, the element $a$ is a unit in $M$.

Units.pow_ofPowEqOne theorem

(ha : a ^ n = 1) (hn : n ≠ 0) : Units.ofPowEqOne _ n ha hn ^ n = 1

Full source

@[to_additive (attr := simp)]
lemma Units.pow_ofPowEqOne (ha : a ^ n = 1) (hn : n ≠ 0) :
    Units.ofPowEqOne _ n ha hn ^ n = 1 := Units.ext <| by simp [ha]

Power of Unit Constructed from $a^n = 1$ is Identity

Informal description

Let $a$ be an element of a monoid $M$ and $n$ a nonzero natural number such that $a^n = 1$. Then the unit element constructed from $a$ via `Units.ofPowEqOne` satisfies $(a^\times)^n = 1$, where $a^\times$ denotes the unit associated with $a$.

IsUnit.of_pow_eq_one theorem

(ha : a ^ n = 1) (hn : n ≠ 0) : IsUnit a

Full source

@[to_additive]
lemma IsUnit.of_pow_eq_one (ha : a ^ n = 1) (hn : n ≠ 0) : IsUnit a :=
  (Units.ofPowEqOne _ n ha hn).isUnit

Element with Power Identity is a Unit

Informal description

For any element $a$ in a monoid $M$ and any nonzero natural number $n$, if $a^n = 1$, then $a$ is a unit in $M$.

Commute.div_eq_div_iff_of_isUnit theorem

(hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) : a / b = c / d ↔ a * d = c * b

Full source

@[to_additive]
lemma Commute.div_eq_div_iff_of_isUnit (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
    a / b = c / d ↔ a * d = c * b := by
  rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, hbd.right_comm,
    hd.div_mul_cancel]

Equality of Fractions with Commuting Units: $\frac{a}{b} = \frac{c}{d} \leftrightarrow a \cdot d = c \cdot b$

Informal description

Let $a, b, c, d$ be elements in a division monoid such that $b$ and $d$ commute (i.e., $b * d = d * b$), and suppose $b$ and $d$ are units. Then the equality of fractions $\frac{a}{b} = \frac{c}{d}$ holds if and only if $a * d = c * b$.