Mathlib.Algebra.Group.Invertible.Basic

unitOfInvertible definition

[Monoid α] (a : α) [Invertible a] : αˣ

Full source

/-- An `Invertible` element is a unit. -/
@[simps]
def unitOfInvertible [Monoid α] (a : α) [Invertible a] : αˣ where
  val := a
  inv := ⅟ a
  val_inv := by simp
  inv_val := by simp

Unit associated with an invertible element

Informal description

Given a monoid $\alpha$ and an element $a \in \alpha$ that is invertible (i.e., there exists an element $b \in \alpha$ such that $a \cdot b = b \cdot a = 1$), the function `unitOfInvertible` constructs the unit (invertible element) associated with $a$, where the underlying element is $a$ itself and its inverse is the explicitly given inverse $\text{⅟} a$ of $a$.

isUnit_of_invertible theorem

[Monoid α] (a : α) [Invertible a] : IsUnit a

Full source

theorem isUnit_of_invertible [Monoid α] (a : α) [Invertible a] : IsUnit a :=
  ⟨unitOfInvertible a, rfl⟩

Invertible Elements are Units in a Monoid

Informal description

For any monoid $\alpha$ and any invertible element $a \in \alpha$, the element $a$ is a unit (i.e., there exists an element $b \in \alpha$ such that $a \cdot b = b \cdot a = 1$).

Units.invertible definition

[Monoid α] (u : αˣ) : Invertible (u : α)

Full source

/-- Units are invertible in their associated monoid. -/
def Units.invertible [Monoid α] (u : αˣ) :
    Invertible (u : α) where
  invOf := ↑u⁻¹
  invOf_mul_self := u.inv_mul
  mul_invOf_self := u.mul_inv

Invertibility of units in a monoid

Informal description

For any monoid $\alpha$ and any unit $u$ in $\alpha$, the element $u$ is invertible with inverse given by the inverse of $u$ in the group of units. Specifically, the inverse satisfies $u \cdot u^{-1} = 1$ and $u^{-1} \cdot u = 1$.

invOf_units theorem

[Monoid α] (u : αˣ) [Invertible (u : α)] : ⅟ (u : α) = ↑u⁻¹

Full source

@[simp]
theorem invOf_units [Monoid α] (u : αˣ) [Invertible (u : α)] : ⅟ (u : α) = ↑u⁻¹ :=
  invOf_eq_right_inv u.mul_inv

Inverse of Unit in Monoid Equals Group Inverse

Informal description

Let $\alpha$ be a monoid and $u$ be a unit in $\alpha$. If $u$ is invertible, then the inverse of $u$ (denoted by $⅟u$) is equal to the inverse of $u$ in the group of units (denoted by $u^{-1}$). In other words, $⅟u = u^{-1}$.

IsUnit.nonempty_invertible theorem

[Monoid α] {a : α} (h : IsUnit a) : Nonempty (Invertible a)

Full source

theorem IsUnit.nonempty_invertible [Monoid α] {a : α} (h : IsUnit a) : Nonempty (Invertible a) :=
  let ⟨x, hx⟩ := h
  ⟨x.invertible.copy _ hx.symm⟩

Existence of Invertible Structure for Units in a Monoid

Informal description

For any element $a$ in a monoid $\alpha$, if $a$ is a unit (i.e., $a$ has a multiplicative inverse), then there exists an invertible structure for $a$.

IsUnit.invertible definition

[Monoid α] {a : α} (h : IsUnit a) : Invertible a

Full source

/-- Convert `IsUnit` to `Invertible` using `Classical.choice`.

Prefer `casesI h.nonempty_invertible` over `letI := h.invertible` if you want to avoid choice. -/
noncomputable def IsUnit.invertible [Monoid α] {a : α} (h : IsUnit a) : Invertible a :=
  Classical.choice h.nonempty_invertible

Invertible structure for a unit element

Informal description

Given a monoid $\alpha$ and an element $a \in \alpha$ that is a unit (i.e., has a multiplicative inverse), the definition constructs an `Invertible a` instance using the axiom of choice via `Classical.choice`. This provides explicit access to the inverse of $a$ within the `Invertible` structure.

nonempty_invertible_iff_isUnit theorem

[Monoid α] (a : α) : Nonempty (Invertible a) ↔ IsUnit a

Full source

@[simp]
theorem nonempty_invertible_iff_isUnit [Monoid α] (a : α) : NonemptyNonempty (Invertible a) ↔ IsUnit a :=
  ⟨Nonempty.rec <| @isUnit_of_invertible _ _ _, IsUnit.nonempty_invertible⟩

Equivalence of Invertibility and Being a Unit in a Monoid

Informal description

For any element $a$ in a monoid $\alpha$, the existence of an invertible structure for $a$ is equivalent to $a$ being a unit (i.e., having a multiplicative inverse).

Commute.invOf_right theorem

[Monoid α] {a b : α} [Invertible b] (h : Commute a b) : Commute a (⅟ b)

Full source

theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a b) :
    Commute a (⅟ b) :=
  calc
    a * ⅟ b = ⅟ b * (b * a * ⅟ b) := by simp [mul_assoc]
    _ = ⅟ b * (a * b * ⅟ b) := by rw [h.eq]
    _ = ⅟ b * a := by simp [mul_assoc]

Commutation with Inverses: Right Version

Informal description

Let $\alpha$ be a monoid and $a, b \in \alpha$ such that $b$ is invertible with inverse $\inv{b}$. If $a$ commutes with $b$, then $a$ also commutes with the inverse of $b$, i.e., $a \cdot \inv{b} = \inv{b} \cdot a$.

Commute.invOf_left theorem

[Monoid α] {a b : α} [Invertible b] (h : Commute b a) : Commute (⅟ b) a

Full source

theorem Commute.invOf_left [Monoid α] {a b : α} [Invertible b] (h : Commute b a) :
    Commute (⅟ b) a :=
  calc
    ⅟ b * a = ⅟ b * (a * b * ⅟ b) := by simp [mul_assoc]
    _ = ⅟ b * (b * a * ⅟ b) := by rw [h.eq]
    _ = a * ⅟ b := by simp [mul_assoc]

Inverse Commutes with Element if Original Commutes

Informal description

Let $\alpha$ be a monoid and let $a, b \in \alpha$ such that $b$ is invertible with inverse $⅟b$. If $b$ commutes with $a$ (i.e., $ba = ab$), then the inverse $⅟b$ commutes with $a$ (i.e., $(⅟b)a = a(⅟b)$).

commute_invOf theorem

{M : Type*} [One M] [Mul M] (m : M) [Invertible m] : Commute m (⅟ m)

Full source

theorem commute_invOf {M : Type*} [One M] [Mul M] (m : M) [Invertible m] : Commute m (⅟ m) :=
  calc
    m * ⅟ m = 1 := mul_invOf_self m
    _ = ⅟ m * m := (invOf_mul_self m).symm

Commutativity of an Element with Its Inverse in a Monoid

Informal description

For any element $m$ in a monoid $M$ with a multiplicative identity and multiplication operation, if $m$ is invertible, then $m$ commutes with its inverse $⅟m$, i.e., $m \cdot ⅟m = ⅟m \cdot m$.

invertibleOfInvertibleMul abbrev

(a b : α) [Invertible a] [Invertible (a * b)] : Invertible b

Full source

/-- This is the `Invertible` version of `Units.isUnit_units_mul` -/
abbrev invertibleOfInvertibleMul (a b : α) [Invertible a] [Invertible (a * b)] : Invertible b where
  invOf := ⅟ (a * b) * a
  invOf_mul_self := by rw [mul_assoc, invOf_mul_self]
  mul_invOf_self := by
    rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]

Invertibility of factor in invertible product

Informal description

Let $a$ and $b$ be elements of a monoid $\alpha$. If $a$ is invertible and the product $a \cdot b$ is invertible, then $b$ is invertible.

invertibleOfMulInvertible abbrev

(a b : α) [Invertible (a * b)] [Invertible b] : Invertible a

Full source

/-- This is the `Invertible` version of `Units.isUnit_mul_units` -/
abbrev invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : Invertible a where
  invOf := b * ⅟ (a * b)
  invOf_mul_self := by
    rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
  mul_invOf_self := by rw [← mul_assoc, mul_invOf_self]

Invertibility of Left Factor in Invertible Product

Informal description

Let $a$ and $b$ be elements of a monoid $\alpha$. If the product $a \cdot b$ is invertible and $b$ is invertible, then $a$ is invertible.

Invertible.mulLeft definition

{a : α} (_ : Invertible a) (b : α) : Invertible b ≃ Invertible (a * b)

Full source

/-- `invertibleOfInvertibleMul` and `invertibleMul` as an equivalence. -/
@[simps apply symm_apply]
def Invertible.mulLeft {a : α} (_ : Invertible a) (b : α) : InvertibleInvertible b ≃ Invertible (a * b) where
  toFun _ := invertibleMul a b
  invFun _ := invertibleOfInvertibleMul a _
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between invertibility of $b$ and $a \cdot b$ when $a$ is invertible

Informal description

For elements $a$ and $b$ in a monoid $\alpha$, if $a$ is invertible, then there is an equivalence between the invertibility of $b$ and the invertibility of the product $a \cdot b$. Specifically: - The forward direction constructs an invertible element for $a \cdot b$ given that $b$ is invertible. - The backward direction recovers the invertibility of $b$ given that $a \cdot b$ is invertible.

Invertible.mulRight definition

(a : α) {b : α} (_ : Invertible b) : Invertible a ≃ Invertible (a * b)

Full source

/-- `invertibleOfMulInvertible` and `invertibleMul` as an equivalence. -/
@[simps apply symm_apply]
def Invertible.mulRight (a : α) {b : α} (_ : Invertible b) : InvertibleInvertible a ≃ Invertible (a * b) where
  toFun _ := invertibleMul a b
  invFun _ := invertibleOfMulInvertible _ b
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between invertibility of $a$ and $a \cdot b$ when $b$ is invertible

Informal description

For elements $a$ and $b$ in a monoid $\alpha$, if $b$ is invertible, then there is an equivalence between the invertibility of $a$ and the invertibility of the product $a \cdot b$. Specifically: - The forward direction constructs an invertible element for $a \cdot b$ given that $a$ is invertible. - The backward direction recovers the invertibility of $a$ given that $a \cdot b$ is invertible.

invertiblePow instance

(m : α) [Invertible m] (n : ℕ) : Invertible (m ^ n)

Full source

instance invertiblePow (m : α) [Invertible m] (n : ℕ) : Invertible (m ^ n) where
  invOf := ⅟ m ^ n
  invOf_mul_self := by rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
  mul_invOf_self := by rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]

Powers of Invertible Elements are Invertible

Informal description

For any invertible element $m$ in a type $\alpha$ and any natural number $n$, the power $m^n$ is also invertible.

invOf_pow theorem

(m : α) [Invertible m] (n : ℕ) [Invertible (m ^ n)] : ⅟ (m ^ n) = ⅟ m ^ n

Full source

lemma invOf_pow (m : α) [Invertible m] (n : ℕ) [Invertible (m ^ n)] : ⅟ (m ^ n) = ⅟ m ^ n :=
  @invertible_unique _ _ _ _ _ (invertiblePow m n) rfl

Inverse of Power Equals Power of Inverse: $\frac{1}{m^n} = \left(\frac{1}{m}\right)^n$

Informal description

For any invertible element $m$ in a type $\alpha$ and any natural number $n$, the inverse of $m^n$ is equal to the $n$-th power of the inverse of $m$, i.e., $\frac{1}{m^n} = \left(\frac{1}{m}\right)^n$.

invertibleOfPowEqOne definition

(x : α) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) : Invertible x

Full source

/-- If `x ^ n = 1` then `x` has an inverse, `x^(n - 1)`. -/
def invertibleOfPowEqOne (x : α) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) : Invertible x :=
  (Units.ofPowEqOne x n hx hn).invertible

Invertibility from power equaling one

Informal description

Given an element $x$ in a monoid $\alpha$ and a natural number $n \neq 0$ such that $x^n = 1$, the element $x$ is invertible with inverse $x^{n-1}$.

Invertible.map definition

 {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [MulOneClass S] [FunLike F R S] [MonoidHomClass F R S] (f : F)
  (r : R) [Invertible r] : Invertible (f r)

Full source

/-- Monoid homs preserve invertibility. -/
def Invertible.map {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [MulOneClass S]
    [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R) [Invertible r] :
    Invertible (f r) where
  invOf := f (⅟ r)
  invOf_mul_self := by rw [← map_mul, invOf_mul_self, map_one]
  mul_invOf_self := by rw [← map_mul, mul_invOf_self, map_one]

Invertibility under monoid homomorphisms

Informal description

Given monoids $R$ and $S$, a monoid homomorphism $f \colon R \to S$, and an invertible element $r \in R$, the image $f(r)$ is invertible in $S$ with inverse $f(r^{-1})$.

map_invOf theorem

 {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R)
  [Invertible r] [ifr : Invertible (f r)] : f (⅟ r) = ⅟ (f r)

Full source

/-- Note that the `Invertible (f r)` argument can be satisfied by using `letI := Invertible.map f r`
before applying this lemma. -/
theorem map_invOf {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [Monoid S]
    [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R)
    [Invertible r] [ifr : Invertible (f r)] :
    f (⅟ r) = ⅟ (f r) :=
  have h : ifr = Invertible.map f r := Subsingleton.elim _ _
  by subst h; rfl

Homomorphism Preserves Inverses: $f(⅟r) = ⅟(f r)$

Informal description

Let $R$ and $S$ be monoids, and let $F$ be a type of functions from $R$ to $S$ that preserves the monoid structure. Given a monoid homomorphism $f \colon R \to S$ and an invertible element $r \in R$ with inverse $⅟r$, the image of the inverse under $f$ equals the inverse of the image, i.e., $f(⅟r) = ⅟(f r)$.

Invertible.ofLeftInverse definition

 {R : Type*} {S : Type*} {G : Type*} [MulOneClass R] [MulOneClass S] [FunLike G S R] [MonoidHomClass G S R] (f : R → S)
  (g : G) (r : R) (h : Function.LeftInverse g f) [Invertible (f r)] : Invertible r

Full source

/-- If a function `f : R → S` has a left-inverse that is a monoid hom,
  then `r : R` is invertible if `f r` is.

The inverse is computed as `g (⅟(f r))` -/
@[simps! -isSimp]
def Invertible.ofLeftInverse {R : Type*} {S : Type*} {G : Type*} [MulOneClass R] [MulOneClass S]
    [FunLike G S R] [MonoidHomClass G S R] (f : R → S) (g : G) (r : R)
    (h : Function.LeftInverse g f) [Invertible (f r)] : Invertible r :=
  (Invertible.map g (f r)).copy _ (h r).symm

Invertibility via left inverse monoid homomorphism

Informal description

Given monoids $R$ and $S$, a function $f \colon R \to S$, and a monoid homomorphism $g \colon S \to R$ that is a left inverse of $f$, if $f(r)$ is invertible in $S$ for some $r \in R$, then $r$ is invertible in $R$. The inverse of $r$ is computed as $g(⅟(f r))$.

invertibleEquivOfLeftInverse definition

 {R : Type*} {S : Type*} {F G : Type*} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R]
  [MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse g f) : Invertible (f r) ≃ Invertible r

Full source

/-- Invertibility on either side of a monoid hom with a left-inverse is equivalent. -/
@[simps]
def invertibleEquivOfLeftInverse {R : Type*} {S : Type*} {F G : Type*} [Monoid R] [Monoid S]
    [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [MonoidHomClass G S R]
    (f : F) (g : G) (r : R) (h : Function.LeftInverse g f) : InvertibleInvertible (f r) ≃ Invertible r where
  toFun _ := Invertible.ofLeftInverse f _ _ h
  invFun _ := Invertible.map f _
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence of invertibility under monoid homomorphism with left inverse

Informal description

Given monoids $R$ and $S$, monoid homomorphisms $f \colon R \to S$ and $g \colon S \to R$ such that $g$ is a left inverse of $f$, and an element $r \in R$, there is an equivalence between the invertibility of $f(r)$ in $S$ and the invertibility of $r$ in $R$. Specifically: 1. The forward direction maps an invertibility proof of $f(r)$ to an invertibility proof of $r$ via $g(⅟(f r))$. 2. The backward direction maps an invertibility proof of $r$ to an invertibility proof of $f(r)$ via $f(⅟ r)$. This equivalence is bijective and preserves the invertibility structure.