doc-next-gen

Mathlib.Algebra.Group.Units.Equiv

Module docstring

{"# Multiplicative and additive equivalence acting on units. "}

toUnits definition
[Group G] : G ≃* Gˣ
Full source 
/-- A group is isomorphic to its group of units. -/
@[to_additive (attr := simps apply_val symm_apply)
"An additive group is isomorphic to its group of additive units"]
def toUnits [Group G] : G ≃* Gˣ where
  toFun x := ⟨x, x⁻¹, mul_inv_cancel _, inv_mul_cancel _⟩
  invFun x := x
  left_inv _ := rfl
  right_inv _ := Units.ext rfl
  map_mul' _ _ := Units.ext rfl
Group isomorphism with its units
Informal description
For any group $G$, the map $\text{toUnits} : G \to G^\times$ is a multiplicative isomorphism between $G$ and its group of units $G^\times$. The isomorphism is defined by sending each element $x \in G$ to the unit $\langle x, x^{-1}, \text{mul\_inv\_cancel}\ x, \text{inv\_mul\_cancel}\ x \rangle \in G^\times$, with the inverse map being the canonical inclusion of units back into $G$.
toUnits_val_apply theorem
{G : Type*} [Group G] (x : Gˣ) : toUnits (x : G) = x
Full source 
@[to_additive (attr := simp)]
lemma toUnits_val_apply {G : Type*} [Group G] (x : Gˣ) : toUnits (x : G) = x := by
  simp_rw [MulEquiv.apply_eq_iff_symm_apply, toUnits_symm_apply]
$\text{toUnits}$ fixes units
Informal description
For any group $G$ and any unit $x \in G^\times$, the multiplicative isomorphism $\text{toUnits}$ applied to the underlying element of $x$ in $G$ returns $x$ itself, i.e., $\text{toUnits}(x) = x$.
Units.mapEquiv definition
(h : M ≃* N) : Mˣ ≃* Nˣ
Full source 
/-- A multiplicative equivalence of monoids defines a multiplicative equivalence
of their groups of units. -/
def mapEquiv (h : M ≃* N) : MˣMˣ ≃* Nˣ :=
  { map h.toMonoidHom with
    invFun := map h.symm.toMonoidHom,
    left_inv := fun u => ext <| h.left_inv u,
    right_inv := fun u => ext <| h.right_inv u }
Multiplicative equivalence of units induced by a monoid isomorphism
Informal description
Given a multiplicative equivalence (isomorphism) $h \colon M \simeq^* N$ between monoids $M$ and $N$, the function `Units.mapEquiv` induces a multiplicative equivalence between the groups of units $M^\times$ and $N^\times$. Specifically, for any unit $u \in M^\times$, the equivalence maps $u$ to $h(u) \in N^\times$, and the inverse equivalence maps any unit $v \in N^\times$ to $h^{-1}(v) \in M^\times$.
Units.mapEquiv_symm theorem
(h : M ≃* N) : (mapEquiv h).symm = mapEquiv h.symm
Full source 
@[simp]
theorem mapEquiv_symm (h : M ≃* N) : (mapEquiv h).symm = mapEquiv h.symm :=
  rfl
Inverse of Induced Unit Equivalence Equals Induced Inverse Equivalence
Informal description
For any multiplicative isomorphism $h \colon M \simeq^* N$ between monoids $M$ and $N$, the inverse of the induced multiplicative equivalence on units $\text{mapEquiv}(h) \colon M^\times \simeq^* N^\times$ is equal to the multiplicative equivalence on units induced by the inverse isomorphism $\text{mapEquiv}(h^{-1}) \colon N^\times \simeq^* M^\times$. In other words, $(\text{mapEquiv}(h))^{-1} = \text{mapEquiv}(h^{-1})$.
Units.coe_mapEquiv theorem
(h : M ≃* N) (x : Mˣ) : (mapEquiv h x : N) = h x
Full source 
@[simp]
theorem coe_mapEquiv (h : M ≃* N) (x : Mˣ) : (mapEquiv h x : N) = h x :=
  rfl
Commutativity of Unit Equivalence with Underlying Monoid Equivalence
Informal description
For any multiplicative equivalence $h \colon M \simeq^* N$ between monoids $M$ and $N$, and any unit $x \in M^\times$, the underlying element of $N$ obtained by applying the induced equivalence $\text{mapEquiv}(h)$ to $x$ is equal to $h(x)$. In other words, the following diagram commutes: $$(M^\times \hookrightarrow M) \xrightarrow{\text{mapEquiv}(h)} (N^\times \hookrightarrow N) = M \xrightarrow{h} N.$$
Units.mulLeft definition
(u : Mˣ) : Equiv.Perm M
Full source 
/-- Left multiplication by a unit of a monoid is a permutation of the underlying type. -/
@[to_additive (attr := simps -fullyApplied apply)
  "Left addition of an additive unit is a permutation of the underlying type."]
def mulLeft (u : Mˣ) : Equiv.Perm M where
  toFun x := u * x
  invFun x := u⁻¹ * x
  left_inv := u.inv_mul_cancel_left
  right_inv := u.mul_inv_cancel_left
Left multiplication by a unit as a permutation
Informal description
For any unit \( u \) in a monoid \( M \), the function \( x \mapsto u \cdot x \) is a permutation of \( M \), with inverse function \( x \mapsto u^{-1} \cdot x \).
Units.mulLeft_symm theorem
(u : Mˣ) : u.mulLeft.symm = u⁻¹.mulLeft
Full source 
@[to_additive (attr := simp)]
theorem mulLeft_symm (u : Mˣ) : u.mulLeft.symm = u⁻¹.mulLeft :=
  Equiv.ext fun _ => rfl
Inverse of Left Multiplication by Unit Equals Left Multiplication by Inverse Unit
Informal description
For any unit $u$ in a monoid $M$, the inverse of the left multiplication permutation by $u$ is equal to the left multiplication permutation by $u^{-1}$. That is, $(u \cdot \_)^{-1} = u^{-1} \cdot \_$.
Units.mulLeft_bijective theorem
(a : Mˣ) : Function.Bijective ((a * ·) : M → M)
Full source 
@[to_additive]
theorem mulLeft_bijective (a : Mˣ) : Function.Bijective ((a * ·) : M → M) :=
  (mulLeft a).bijective
Bijectivity of Left Multiplication by a Unit
Informal description
For any unit $a$ in a monoid $M$, the left multiplication map $x \mapsto a \cdot x$ is bijective on $M$.
Units.mulRight definition
(u : Mˣ) : Equiv.Perm M
Full source 
/-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
@[to_additive (attr := simps -fullyApplied apply)
"Right addition of an additive unit is a permutation of the underlying type."]
def mulRight (u : Mˣ) : Equiv.Perm M where
  toFun x := x * u
  invFun x := x * ↑u⁻¹
  left_inv x := mul_inv_cancel_right x u
  right_inv x := inv_mul_cancel_right x u
Right multiplication permutation by a unit
Informal description
For any unit $u$ in a monoid $M$, the function `Units.mulRight u` is a permutation of $M$ defined by right multiplication by $u$. Specifically: - The forward map sends $x \in M$ to $x \cdot u$. - The inverse map sends $x \in M$ to $x \cdot u^{-1}$. The permutation properties follow from the cancellation laws for units: - Left inverse: $x \cdot u^{-1} \cdot u = x$ for all $x \in M$. - Right inverse: $x \cdot u \cdot u^{-1} = x$ for all $x \in M$.
Units.mulRight_symm theorem
(u : Mˣ) : u.mulRight.symm = u⁻¹.mulRight
Full source 
@[to_additive (attr := simp)]
theorem mulRight_symm (u : Mˣ) : u.mulRight.symm = u⁻¹.mulRight :=
  Equiv.ext fun _ => rfl
Inverse of Right Multiplication by a Unit Equals Right Multiplication by its Inverse
Informal description
For any unit $u$ in a monoid $M$, the inverse of the right multiplication permutation by $u$ is equal to the right multiplication permutation by $u^{-1}$. In other words, $(u \cdot \_)^{-1} = u^{-1} \cdot \_$.
Units.mulRight_bijective theorem
(a : Mˣ) : Function.Bijective ((· * a) : M → M)
Full source 
@[to_additive]
theorem mulRight_bijective (a : Mˣ) : Function.Bijective ((· * a) : M → M) :=
  (mulRight a).bijective
Bijectivity of Right Multiplication by a Unit
Informal description
For any unit $a$ in a monoid $M$, the right multiplication map $x \mapsto x \cdot a$ is bijective on $M$.
Equiv.mulLeft definition
(a : G) : Perm G
Full source 
/-- Left multiplication in a `Group` is a permutation of the underlying type. -/
@[to_additive "Left addition in an `AddGroup` is a permutation of the underlying type."]
protected def mulLeft (a : G) : Perm G :=
  (toUnits a).mulLeft
Left multiplication as a permutation in a group
Informal description
For any element $a$ in a group $G$, the left multiplication map $x \mapsto a \cdot x$ is a permutation of $G$. The inverse of this permutation is given by left multiplication with $a^{-1}$.
Equiv.coe_mulLeft theorem
(a : G) : ⇑(Equiv.mulLeft a) = (a * ·)
Full source 
@[to_additive (attr := simp)]
theorem coe_mulLeft (a : G) : ⇑(Equiv.mulLeft a) = (a * ·) :=
  rfl
Coefficient of Left Multiplication Equivalence in a Group
Informal description
For any element $a$ in a group $G$, the underlying function of the left multiplication equivalence $\text{Equiv.mulLeft}(a)$ is equal to the function $x \mapsto a * x$.
Equiv.mulLeft_symm_apply theorem
(a : G) : ((Equiv.mulLeft a).symm : G → G) = (a⁻¹ * ·)
Full source 
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
@[to_additive (attr := simp) "Extra simp lemma that `dsimp` can use. `simp` will never use this."]
theorem mulLeft_symm_apply (a : G) : ((Equiv.mulLeft a).symm : G → G) = (a⁻¹ * ·) :=
  rfl
Inverse of Left Multiplication Equivalence Acts as Left Multiplication by Inverse
Informal description
For any element $a$ in a group $G$, the inverse of the left multiplication equivalence $\text{mulLeft}(a)$ acts as left multiplication by $a^{-1}$, i.e., $(\text{mulLeft}(a))^{-1}(x) = a^{-1} \cdot x$ for all $x \in G$.
Equiv.mulLeft_symm theorem
(a : G) : (Equiv.mulLeft a).symm = Equiv.mulLeft a⁻¹
Full source 
@[to_additive (attr := simp)]
theorem mulLeft_symm (a : G) : (Equiv.mulLeft a).symm = Equiv.mulLeft a⁻¹ :=
  ext fun _ => rfl
Inverse of Left Multiplication Equivalence is Left Multiplication by Inverse
Informal description
For any element $a$ in a group $G$, the inverse of the left multiplication equivalence $\text{mulLeft}(a)$ is equal to the left multiplication equivalence $\text{mulLeft}(a^{-1})$.
Equiv.mulRight definition
(a : G) : Perm G
Full source 
/-- Right multiplication in a `Group` is a permutation of the underlying type. -/
@[to_additive "Right addition in an `AddGroup` is a permutation of the underlying type."]
protected def mulRight (a : G) : Perm G :=
  (toUnits a).mulRight
Right multiplication permutation in a group
Informal description
For any element $a$ in a group $G$, the function $\text{mulRight}\ a$ is a permutation of $G$ defined by right multiplication by $a$. Specifically: - The forward map sends $x \in G$ to $x \cdot a$. - The inverse map sends $x \in G$ to $x \cdot a^{-1}$.
Equiv.coe_mulRight theorem
(a : G) : ⇑(Equiv.mulRight a) = fun x => x * a
Full source 
@[to_additive (attr := simp)]
theorem coe_mulRight (a : G) : ⇑(Equiv.mulRight a) = fun x => x * a :=
  rfl
Right Multiplication Permutation as Function: $\text{mulRight}\ a = (x \mapsto x \cdot a)$
Informal description
For any element $a$ in a group $G$, the function corresponding to the right multiplication permutation $\text{mulRight}\ a$ is given by $x \mapsto x \cdot a$.
Equiv.mulRight_symm theorem
(a : G) : (Equiv.mulRight a).symm = Equiv.mulRight a⁻¹
Full source 
@[to_additive (attr := simp)]
theorem mulRight_symm (a : G) : (Equiv.mulRight a).symm = Equiv.mulRight a⁻¹ :=
  ext fun _ => rfl
Inverse of Right Multiplication Permutation Equals Right Multiplication by Inverse
Informal description
For any element $a$ in a group $G$, the inverse of the right multiplication permutation by $a$ is equal to the right multiplication permutation by $a^{-1}$. That is, $(\text{mulRight}\ a)^{-1} = \text{mulRight}\ a^{-1}$.
Equiv.mulRight_symm_apply theorem
(a : G) : ((Equiv.mulRight a).symm : G → G) = fun x => x * a⁻¹
Full source 
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
@[to_additive (attr := simp) "Extra simp lemma that `dsimp` can use. `simp` will never use this."]
theorem mulRight_symm_apply (a : G) : ((Equiv.mulRight a).symm : G → G) = fun x => x * a⁻¹ :=
  rfl
Inverse of Right Multiplication Equivalence in a Group
Informal description
For any element $a$ in a group $G$, the inverse of the right multiplication equivalence $\text{mulRight}\ a$ is given by the function $x \mapsto x \cdot a^{-1}$.
Equiv.divLeft definition
(a : G) : G ≃ G
Full source 
/-- A version of `Equiv.mulLeft a b⁻¹` that is defeq to `a / b`. -/
@[to_additive (attr := simps) " A version of `Equiv.addLeft a (-b)` that is defeq to `a - b`. "]
protected def divLeft (a : G) : G ≃ G where
  toFun b := a / b
  invFun b := b⁻¹ * a
  left_inv b := by simp [div_eq_mul_inv]
  right_inv b := by simp [div_eq_mul_inv]
Left division bijection in a group
Informal description
For an element \( a \) in a group \( G \), the function \( \text{divLeft}_a : G \to G \) is defined by \( \text{divLeft}_a(b) = a / b \), with its inverse given by \( \text{invFun}_a(b) = b^{-1} * a \). This forms a bijection on \( G \).
Equiv.divLeft_eq_inv_trans_mulLeft theorem
(a : G) : Equiv.divLeft a = (Equiv.inv G).trans (Equiv.mulLeft a)
Full source 
@[to_additive]
theorem divLeft_eq_inv_trans_mulLeft (a : G) :
    Equiv.divLeft a = (Equiv.inv G).trans (Equiv.mulLeft a) :=
  ext fun _ => div_eq_mul_inv _ _
Left Division as Inversion Followed by Left Multiplication
Informal description
For any element $a$ in a group $G$, the left division bijection $\text{divLeft}_a$ is equal to the composition of the inversion permutation on $G$ followed by the left multiplication permutation by $a$. That is, $\text{divLeft}_a = \text{inv} \circ \text{mulLeft}_a$.
Equiv.divRight definition
(a : G) : G ≃ G
Full source 
/-- A version of `Equiv.mulRight a⁻¹ b` that is defeq to `b / a`. -/
@[to_additive (attr := simps) " A version of `Equiv.addRight (-a) b` that is defeq to `b - a`. "]
protected def divRight (a : G) : G ≃ G where
  toFun b := b / a
  invFun b := b * a
  left_inv b := by simp [div_eq_mul_inv]
  right_inv b := by simp [div_eq_mul_inv]
Right division bijection in a group
Informal description
For an element \( a \) in a group \( G \), the function \( \text{divRight}_a : G \to G \) is defined by \( \text{divRight}_a(b) = b / a \), with its inverse given by \( \text{invFun}_a(b) = b * a \). This forms a bijection on \( G \).
Equiv.divRight_eq_mulRight_inv theorem
(a : G) : Equiv.divRight a = Equiv.mulRight a⁻¹
Full source 
@[to_additive]
theorem divRight_eq_mulRight_inv (a : G) : Equiv.divRight a = Equiv.mulRight a⁻¹ :=
  ext fun _ => div_eq_mul_inv _ _
Equality of Right Division and Right Multiplication by Inverse in a Group
Informal description
For any element $a$ in a group $G$, the right division bijection $\text{divRight}_a$ is equal to the right multiplication permutation by $a^{-1}$, i.e., $\text{divRight}_a = \text{mulRight}_{a^{-1}}$.
unitsEquivProdSubtype definition
[Monoid α] : αˣ ≃ { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }
Full source 
/-- The `αˣ` type is equivalent to a subtype of `α × α`. -/
@[simps]
def unitsEquivProdSubtype [Monoid α] : αˣαˣ ≃ {p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1} where
  toFun u := ⟨(u, ↑u⁻¹), u.val_inv, u.inv_val⟩
  invFun p := Units.mk (p : α × α).1 (p : α × α).2 p.prop.1 p.prop.2
  left_inv _ := Units.ext rfl
  right_inv _ := Subtype.ext <| Prod.ext rfl rfl
Bijection between units and multiplicative inverse pairs
Informal description
For a monoid $\alpha$, the type $\alpha^\times$ of units (invertible elements) of $\alpha$ is in bijection with the subtype of $\alpha \times \alpha$ consisting of pairs $(x, y)$ such that $x \cdot y = 1$ and $y \cdot x = 1$. The bijection maps a unit $u$ to the pair $(u, u^{-1})$, and its inverse maps a pair $(x, y)$ satisfying the conditions to the unit $\text{mk}(x, y)$.
MulEquiv.inv definition
(G : Type*) [DivisionCommMonoid G] : G ≃* G
Full source 
/-- In a `DivisionCommMonoid`, `Equiv.inv` is a `MulEquiv`. There is a variant of this
`MulEquiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case. -/
@[to_additive (attr := simps apply)
  "When the `AddGroup` is commutative, `Equiv.neg` is an `AddEquiv`."]
def MulEquiv.inv (G : Type*) [DivisionCommMonoid G] : G ≃* G :=
  { Equiv.inv G with toFun := Inv.inv, invFun := Inv.inv, map_mul' := mul_inv }
Inversion as multiplicative equivalence in a commutative division monoid
Informal description
For a commutative division monoid $G$, the inversion operation $x \mapsto x^{-1}$ is a multiplicative equivalence (isomorphism) from $G$ to itself. This means that inversion is a bijective map that preserves the multiplication operation, i.e., $(x \cdot y)^{-1} = x^{-1} \cdot y^{-1}$ for all $x, y \in G$.
MulEquiv.inv_symm theorem
(G : Type*) [DivisionCommMonoid G] : (MulEquiv.inv G).symm = MulEquiv.inv G
Full source 
@[to_additive (attr := simp)]
theorem MulEquiv.inv_symm (G : Type*) [DivisionCommMonoid G] :
    (MulEquiv.inv G).symm = MulEquiv.inv G :=
  rfl
Self-Inverse Property of Inversion as Multiplicative Equivalence
Informal description
For any commutative division monoid $G$, the inverse of the multiplicative equivalence given by the inversion operation $x \mapsto x^{-1}$ is equal to itself, i.e., $(f^{-1})^{-1} = f$ where $f$ is the inversion map.
MulEquiv.isUnit_map theorem
: IsUnit (f x) ↔ IsUnit x
Full source 
@[to_additive (attr := simp high)]
lemma MulEquiv.isUnit_map : IsUnitIsUnit (f x) ↔ IsUnit x where
  mp hx := by
    simpa using hx.map <| MonoidHom.mk ⟨EquivLike.inv f, EquivLike.injective f <| by simp⟩
      fun x y ↦ EquivLike.injective f <| by simp
  mpr := .map f
Multiplicative Equivalence Preserves Unit Status: $f(x)$ is a unit iff $x$ is a unit
Informal description
For any multiplicative equivalence $f$ between monoids and any element $x$ in the domain, $x$ is a unit if and only if $f(x)$ is a unit.
isLocalHom_equiv theorem
: IsLocalHom f
Full source 
@[instance] theorem isLocalHom_equiv : IsLocalHom f where map_nonunit := by simp
Multiplicative Equivalence Preserves Unit Status
Informal description
A multiplicative equivalence $f$ between monoids is a local homomorphism, meaning that for any element $x$ in the domain, $x$ is a unit if and only if $f(x)$ is a unit.