Mathlib.Algebra.Group.Units.Opposite

Units.opEquiv definition

{M} [Monoid M] : Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ

Full source

/-- The units of the opposites are equivalent to the opposites of the units. -/
@[to_additive
      "The additive units of the additive opposites are equivalent to the additive opposites
      of the additive units."]
def Units.opEquiv {M} [Monoid M] : MᵐᵒᵖMᵐᵒᵖˣMᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ where
  toFun u := op ⟨unop u, unop ↑u⁻¹, op_injective u.4, op_injective u.3⟩
  invFun := MulOpposite.rec' fun u => ⟨op ↑u, op ↑u⁻¹, unop_injective <| u.4, unop_injective u.3⟩
  map_mul' _ _ := unop_injective <| Units.ext <| rfl
  left_inv x := Units.ext <| by simp
  right_inv x := unop_injective <| Units.ext <| by rfl

Equivalence between units of multiplicative opposite and opposite of units

Informal description

For any monoid $M$, there is a multiplicative equivalence between the units of the multiplicative opposite $M^\text{op}$ and the multiplicative opposite of the units of $M$. Specifically, the equivalence maps a unit $u$ in $M^\text{op}$ to $\text{op}(u^{-1})$ in $(M^\text{op})^\times$, and vice versa, preserving the multiplicative structure.

Units.coe_unop_opEquiv theorem

{M} [Monoid M] (u : Mᵐᵒᵖˣ) : ((Units.opEquiv u).unop : M) = unop (u : Mᵐᵒᵖ)

Full source

@[to_additive (attr := simp)]
theorem Units.coe_unop_opEquiv {M} [Monoid M] (u : MᵐᵒᵖMᵐᵒᵖˣ) :
    ((Units.opEquiv u).unop : M) = unop (u : Mᵐᵒᵖ) :=
  rfl

Compatibility of Unit Equivalence with Projection in Multiplicative Opposite

Informal description

For any monoid $M$ and any unit $u$ in the multiplicative opposite $M^\text{op}$, the underlying element of $M$ obtained by first applying the equivalence `Units.opEquiv` to $u$ and then projecting back via `unop` is equal to the projection of $u$ via `unop$ directly. In other words, $(\text{Units.opEquiv}(u))^\text{unop} = u^\text{unop}$.

Units.coe_opEquiv_symm theorem

{M} [Monoid M] (u : Mˣᵐᵒᵖ) : (Units.opEquiv.symm u : Mᵐᵒᵖ) = op (u.unop : M)

Full source

@[to_additive (attr := simp)]
theorem Units.coe_opEquiv_symm {M} [Monoid M] (u : MˣMˣᵐᵒᵖ) :
    (Units.opEquiv.symm u : Mᵐᵒᵖ) = op (u.unop : M) :=
  rfl

Equality of Inverse Embedding and Opposite Projection for Units in Multiplicative Opposite

Informal description

For any monoid $M$ and any unit $u$ in the multiplicative opposite of the units of $M$, the canonical embedding of the inverse of the multiplicative equivalence `Units.opEquiv.symm` applied to $u$ is equal to the multiplicative opposite of the projection of $u$ back to $M$. In symbols, $\text{op}(u^{-1}) = \text{op}(u^{\text{unop}})$.

IsUnit.op theorem

{M} [Monoid M] {m : M} (h : IsUnit m) : IsUnit (op m)

Full source

@[to_additive]
nonrec theorem IsUnit.op {M} [Monoid M] {m : M} (h : IsUnit m) : IsUnit (op m) :=
  let ⟨u, hu⟩ := h
  hu ▸ ⟨Units.opEquiv.symm (op u), rfl⟩

Preservation of Units under Multiplicative Opposite Embedding

Informal description

For any monoid $M$ and element $m \in M$, if $m$ is a unit (i.e., invertible), then its image under the canonical embedding into the multiplicative opposite $\text{op}(m) \in M^\text{op}$ is also a unit.

IsUnit.unop theorem

{M} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) : IsUnit (unop m)

Full source

@[to_additive]
nonrec theorem IsUnit.unop {M} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) : IsUnit (unop m) :=
  let ⟨u, hu⟩ := h
  hu ▸ ⟨unop (Units.opEquiv u), rfl⟩

Projection of Units from Multiplicative Opposite Preserves Unit Status

Informal description

For any monoid $M$ and any element $m$ in the multiplicative opposite $M^\text{op}$, if $m$ is a unit in $M^\text{op}$, then its projection $\text{unop}(m)$ is a unit in $M$.

isUnit_op theorem

{M} [Monoid M] {m : M} : IsUnit (op m) ↔ IsUnit m

Full source

@[to_additive (attr := simp)]
theorem isUnit_op {M} [Monoid M] {m : M} : IsUnitIsUnit (op m) ↔ IsUnit m :=
  ⟨IsUnit.unop, IsUnit.op⟩

Unit Correspondence under Multiplicative Opposite: $\text{IsUnit}(\text{op}(m)) \leftrightarrow \text{IsUnit}(m)$

Informal description

For any monoid $M$ and element $m \in M$, the element $\text{op}(m)$ in the multiplicative opposite $M^\text{op}$ is a unit if and only if $m$ is a unit in $M$.

isUnit_unop theorem

{M} [Monoid M] {m : Mᵐᵒᵖ} : IsUnit (unop m) ↔ IsUnit m

Full source

@[to_additive (attr := simp)]
theorem isUnit_unop {M} [Monoid M] {m : Mᵐᵒᵖ} : IsUnitIsUnit (unop m) ↔ IsUnit m :=
  ⟨IsUnit.op, IsUnit.unop⟩

Unit Status Preservation under Projection from Multiplicative Opposite

Informal description

For any monoid $M$ and any element $m$ in the multiplicative opposite $M^\text{op}$, the projection $\text{unop}(m)$ is a unit in $M$ if and only if $m$ is a unit in $M^\text{op}$.