doc-next-gen

Mathlib.Algebra.Group.Equiv.Opposite

Module docstring

{"# Group isomorphism between a group and its opposite "}

MulOpposite.opAddEquiv definition
[Add α] : α ≃+ αᵐᵒᵖ
Full source 
/-- The function `MulOpposite.op` is an additive equivalence. -/
@[simps! -fullyApplied +simpRhs apply symm_apply]
def opAddEquiv [Add α] : α ≃+ αᵐᵒᵖ where
  toEquiv := opEquiv
  map_add' _ _ := rfl
Additive equivalence between a group and its opposite
Informal description
The function $\text{op} : \alpha \to \alpha^\text{op}$ is an additive equivalence between an additive group $\alpha$ and its opposite group $\alpha^\text{op}$. Here, $\alpha^\text{op}$ denotes the opposite group, where the addition is defined by $x +^\text{op} y = y + x$.
MulOpposite.opAddEquiv_toEquiv theorem
[Add α] : ((opAddEquiv : α ≃+ αᵐᵒᵖ) : α ≃ αᵐᵒᵖ) = opEquiv
Full source 
@[simp] lemma opAddEquiv_toEquiv [Add α] : ((opAddEquiv : α ≃+ αᵐᵒᵖ) : α ≃ αᵐᵒᵖ) = opEquiv := rfl
Underlying Equivalence of Opposite Additive Isomorphism
Informal description
For any additive group $\alpha$, the underlying equivalence of the additive group isomorphism $\text{opAddEquiv} \colon \alpha \simeq^+ \alpha^\text{op}$ is equal to the canonical equivalence $\text{opEquiv} \colon \alpha \simeq \alpha^\text{op}$.
AddOpposite.opMulEquiv definition
[Mul α] : α ≃* αᵃᵒᵖ
Full source 
/-- The function `AddOpposite.op` is a multiplicative equivalence. -/
@[simps! -fullyApplied +simpRhs]
def opMulEquiv [Mul α] : α ≃* αᵃᵒᵖ where
  toEquiv := opEquiv
  map_mul' _ _ := rfl
Multiplicative equivalence to the opposite structure
Informal description
The function $\text{op} : \alpha \to \alpha^{\text{op}}$ is a multiplicative equivalence between a multiplicative structure $\alpha$ and its opposite $\alpha^{\text{op}}$. This means it is a bijection that preserves multiplication, i.e., $\text{op}(x \cdot y) = \text{op}(y) \cdot \text{op}(x)$ for all $x, y \in \alpha$.
AddOpposite.opMulEquiv_toEquiv theorem
[Mul α] : ((opMulEquiv : α ≃* αᵃᵒᵖ) : α ≃ αᵃᵒᵖ) = opEquiv
Full source 
@[simp] lemma opMulEquiv_toEquiv [Mul α] : ((opMulEquiv : α ≃* αᵃᵒᵖ) : α ≃ αᵃᵒᵖ) = opEquiv := rfl
Underlying Equivalence of Opposite Multiplicative Isomorphism
Informal description
For any multiplicative structure $\alpha$, the underlying equivalence of the multiplicative equivalence $\text{opMulEquiv} \colon \alpha \simeq^* \alpha^{\text{op}}$ is equal to the canonical equivalence $\text{opEquiv} \colon \alpha \simeq \alpha^{\text{op}}$. In other words, when viewing the multiplicative isomorphism $\text{opMulEquiv}$ as a plain equivalence (forgetting its multiplicative structure), it coincides with the standard bijection $\text{opEquiv}$ between $\alpha$ and its opposite $\alpha^{\text{op}}$.
MulEquiv.inv' definition
(G : Type*) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ
Full source 
/-- Inversion on a group is a `MulEquiv` to the opposite group. When `G` is commutative, there is
`MulEquiv.inv`. -/
@[to_additive (attr := simps! -fullyApplied +simpRhs)
      "Negation on an additive group is an `AddEquiv` to the opposite group. When `G`
      is commutative, there is `AddEquiv.inv`."]
def MulEquiv.inv' (G : Type*) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ :=
  { (Equiv.inv G).trans opEquiv with map_mul' x y := unop_injective <| mul_inv_rev x y }
Inversion as multiplicative equivalence to the opposite monoid
Informal description
The inversion operation $x \mapsto x^{-1}$ on a division monoid $G$ induces a multiplicative equivalence between $G$ and its opposite monoid $G^\text{op}$. This equivalence is constructed by composing the inversion permutation (which is a bijection) with the canonical equivalence to the opposite monoid, and it satisfies the property that the multiplication in the opposite monoid corresponds to the reversed multiplication followed by inversion in the original monoid, i.e., $(x \cdot y)^{-1} = y^{-1} \cdot x^{-1}$.
MulHom.toOpposite definition
{M N : Type*} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ x y, Commute (f x) (f y)) : M →ₙ* Nᵐᵒᵖ
Full source 
/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
defines a semigroup homomorphism to `Nᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied)
"An additive semigroup homomorphism `f : AddHom M N` such that `f x` additively
commutes with `f y` for all `x, y` defines an additive semigroup homomorphism to `Sᵃᵒᵖ`."]
def MulHom.toOpposite {M N : Type*} [Mul M] [Mul N] (f : M →ₙ* N)
    (hf : ∀ x y, Commute (f x) (f y)) : M →ₙ* Nᵐᵒᵖ where
  toFun := opop ∘ f
  map_mul' x y := by simp [(hf x y).eq]
Non-unital multiplicative homomorphism to opposite structure
Informal description
Given a non-unital multiplicative homomorphism \( f \colon M \to N \) between multiplicative structures \( M \) and \( N \), if \( f(x) \) commutes with \( f(y) \) for all \( x, y \in M \), then \( f \) induces a non-unital multiplicative homomorphism from \( M \) to the opposite multiplicative structure \( N^\text{op} \), defined by composing \( f \) with the canonical map \( \text{op} \colon N \to N^\text{op} \).
MulHom.fromOpposite definition
{M N : Type*} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ x y, Commute (f x) (f y)) : Mᵐᵒᵖ →ₙ* N
Full source 
/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
defines a semigroup homomorphism from `Mᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied)
"An additive semigroup homomorphism `f : AddHom M N` such that `f x` additively
commutes with `f y` for all `x`, `y` defines an additive semigroup homomorphism from `Mᵃᵒᵖ`."]
def MulHom.fromOpposite {M N : Type*} [Mul M] [Mul N] (f : M →ₙ* N)
    (hf : ∀ x y, Commute (f x) (f y)) : MᵐᵒᵖMᵐᵒᵖ →ₙ* N where
  toFun := f ∘ MulOpposite.unop
  map_mul' _ _ := (f.map_mul _ _).trans (hf _ _).eq
Non-unital multiplicative homomorphism from opposite structure
Informal description
Given a non-unital multiplicative homomorphism \( f \colon M \to N \) between multiplicative structures \( M \) and \( N \), if \( f(x) \) commutes with \( f(y) \) for all \( x, y \in M \), then \( f \) induces a non-unital multiplicative homomorphism from the opposite multiplicative structure \( M^\text{op} \) to \( N \), defined by composing \( f \) with the canonical map \( \text{unop} \colon M^\text{op} \to M \).
MonoidHom.toOpposite definition
{M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ x y, Commute (f x) (f y)) : M →* Nᵐᵒᵖ
Full source 
/-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
a monoid homomorphism to `Nᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied)
"An additive monoid homomorphism `f : M →+ N` such that `f x` additively commutes
with `f y` for all `x, y` defines an additive monoid homomorphism to `Sᵃᵒᵖ`."]
def MonoidHom.toOpposite {M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N)
    (hf : ∀ x y, Commute (f x) (f y)) : M →* Nᵐᵒᵖ where
  toFun := opop ∘ f
  map_one' := congrArg op f.map_one
  map_mul' x y := by simp [(hf x y).eq]
Monoid homomorphism to opposite monoid
Informal description
Given a monoid homomorphism \( f \colon M \to N \) such that \( f(x) \) commutes with \( f(y) \) for all \( x, y \in M \), there exists a monoid homomorphism from \( M \) to the opposite monoid \( N^\text{op} \) defined by composing \( f \) with the canonical map \( \text{op} \colon N \to N^\text{op} \).
MonoidHom.fromOpposite definition
{M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ x y, Commute (f x) (f y)) : Mᵐᵒᵖ →* N
Full source 
/-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
a monoid homomorphism from `Mᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied)
"An additive monoid homomorphism `f : M →+ N` such that `f x` additively commutes
with `f y` for all `x`, `y` defines an additive monoid homomorphism from `Mᵃᵒᵖ`."]
def MonoidHom.fromOpposite {M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N)
    (hf : ∀ x y, Commute (f x) (f y)) : MᵐᵒᵖMᵐᵒᵖ →* N where
  toFun := f ∘ MulOpposite.unop
  map_one' := f.map_one
  map_mul' _ _ := (f.map_mul _ _).trans (hf _ _).eq
Monoid homomorphism from opposite monoid induced by commuting homomorphism
Informal description
Given a monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$ such that $f(x)$ commutes with $f(y)$ for all $x, y \in M$, there exists a monoid homomorphism from the opposite monoid $M^\text{op}$ to $N$ defined by composing $f$ with the canonical map $\text{unop} \colon M^\text{op} \to M$.
MulHom.op definition
{M N} [Mul M] [Mul N] : (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ)
Full source 
/-- A semigroup homomorphism `M →ₙ* N` can equivalently be viewed as a semigroup homomorphism
`Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[to_additive (attr := simps)
"An additive semigroup homomorphism `AddHom M N` can equivalently be viewed as an additive semigroup
homomorphism `AddHom Mᵃᵒᵖ Nᵃᵒᵖ`. This is the action of the
(fully faithful)`ᵃᵒᵖ`-functor on morphisms."]
def MulHom.op {M N} [Mul M] [Mul N] : (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) where
  toFun f :=
    { toFun := MulOpposite.opMulOpposite.op ∘ f ∘ unop,
      map_mul' x y := unop_injective (f.map_mul y.unop x.unop) }
  invFun f :=
    { toFun := unopunop ∘ f ∘ MulOpposite.op,
      map_mul' x y := congrArg unop (f.map_mul (MulOpposite.op y) (MulOpposite.op x)) }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence of Non-unital Multiplicative Homomorphisms via Opposites
Informal description
The equivalence between non-unital multiplicative homomorphisms $f \colon M \to N$ and non-unital multiplicative homomorphisms $f^\text{op} \colon M^\text{op} \to N^\text{op}$, where $M^\text{op}$ denotes the opposite multiplicative structure of $M$. This equivalence is given by pre- and post-composing with the canonical operations of taking opposites (`op` and `unop`), and it respects the multiplicative structure. Specifically: - The forward map takes a homomorphism $f \colon M \to N$ and constructs $f^\text{op} \colon M^\text{op} \to N^\text{op}$ defined by $f^\text{op}(x) = \text{op}(f(\text{unop}(x)))$. - The inverse map takes a homomorphism $g \colon M^\text{op} \to N^\text{op}$ and constructs $g^\text{unop} \colon M \to N$ defined by $g^\text{unop}(x) = \text{unop}(g(\text{op}(x)))$.
MulHom.unop definition
{M N} [Mul M] [Mul N] : (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)
Full source 
/-- The 'unopposite' of a semigroup homomorphism `Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. Inverse to `MulHom.op`. -/
@[to_additive (attr := simp)
"The 'unopposite' of an additive semigroup homomorphism `Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ`. Inverse to `AddHom.op`."]
def MulHom.unop {M N} [Mul M] [Mul N] : (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N) :=
  MulHom.op.symm
Inverse equivalence of non-unital multiplicative homomorphisms via opposites
Informal description
The inverse of the equivalence `MulHom.op`, which converts a non-unital multiplicative homomorphism between opposite multiplicative structures $f \colon M^\text{op} \to N^\text{op}$ back to a non-unital multiplicative homomorphism $f \colon M \to N$ by pre- and post-composing with the canonical operations of taking opposites (`op` and `unop`). This preserves the multiplicative structure.
AddHom.mulOp definition
{M N} [Add M] [Add N] : AddHom M N ≃ AddHom Mᵐᵒᵖ Nᵐᵒᵖ
Full source 
/-- An additive semigroup homomorphism `AddHom M N` can equivalently be viewed as an additive
homomorphism `AddHom Mᵐᵒᵖ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on
morphisms. -/
@[simps]
def AddHom.mulOp {M N} [Add M] [Add N] : AddHomAddHom M N ≃ AddHom Mᵐᵒᵖ Nᵐᵒᵖ where
  toFun f :=
    { toFun := MulOpposite.opMulOpposite.op ∘ f ∘ MulOpposite.unop,
      map_add' x y := unop_injective (f.map_add x.unop y.unop) }
  invFun f :=
    { toFun := MulOpposite.unopMulOpposite.unop ∘ f ∘ MulOpposite.op,
      map_add' :=
        fun x y => congrArg MulOpposite.unop (f.map_add (MulOpposite.op x) (MulOpposite.op y)) }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence of additive homomorphisms via opposites
Informal description
The equivalence between non-unital additive homomorphisms $f : M \to N$ and non-unital additive homomorphisms $f^\text{op} : M^\text{op} \to N^\text{op}$, where $M^\text{op}$ denotes the opposite additive structure of $M$. This equivalence is given by pre- and post-composing with the canonical operations of taking opposites (`op` and `unop`), and it respects the additive structure.
AddHom.mulUnop definition
{α β} [Add α] [Add β] : AddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β
Full source 
/-- The 'unopposite' of an additive semigroup hom `αᵐᵒᵖ →+ βᵐᵒᵖ`. Inverse to
`AddHom.mul_op`. -/
@[simp]
def AddHom.mulUnop {α β} [Add α] [Add β] : AddHomAddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β :=
  AddHom.mulOp.symm
Inverse equivalence of additive homomorphisms via opposites
Informal description
The inverse of the equivalence `AddHom.mulOp`, which converts an additive homomorphism between opposite additive structures $f : \alpha^\text{op} \to \beta^\text{op}$ back to an additive homomorphism $f : \alpha \to \beta$ by pre- and post-composing with the canonical operations of taking opposites (`op` and `unop`). This preserves the additive structure.
MonoidHom.op definition
{M N} [MulOneClass M] [MulOneClass N] : (M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ)
Full source 
/-- A monoid homomorphism `M →* N` can equivalently be viewed as a monoid homomorphism
`Mᵐᵒᵖ →* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[to_additive (attr := simps)
"An additive monoid homomorphism `M →+ N` can equivalently be viewed as an additive monoid
homomorphism `Mᵃᵒᵖ →+ Nᵃᵒᵖ`. This is the action of the (fully faithful)
`ᵃᵒᵖ`-functor on morphisms."]
def MonoidHom.op {M N} [MulOneClass M] [MulOneClass N] : (M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ) where
  toFun f :=
    { toFun := MulOpposite.opMulOpposite.op ∘ f ∘ unop, map_one' := congrArg MulOpposite.op f.map_one,
      map_mul' x y := unop_injective (f.map_mul y.unop x.unop) }
  invFun f :=
    { toFun := unopunop ∘ f ∘ MulOpposite.op, map_one' := congrArg unop f.map_one,
      map_mul' x y := congrArg unop (f.map_mul (MulOpposite.op y) (MulOpposite.op x)) }
  left_inv _ := rfl
  right_inv _ := rfl
Monoid homomorphism equivalence via opposites
Informal description
The equivalence between monoid homomorphisms $M \to^* N$ and monoid homomorphisms $M^\text{op} \to^* N^\text{op}$, where $M^\text{op}$ denotes the opposite monoid of $M$. This equivalence is given by pre- and post-composing with the canonical operations of taking opposites (`op` and `unop`), and it respects the monoid structure.
MonoidHom.unop definition
{M N} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N)
Full source 
/-- The 'unopposite' of a monoid homomorphism `Mᵐᵒᵖ →* Nᵐᵒᵖ`. Inverse to `MonoidHom.op`. -/
@[to_additive (attr := simp)
"The 'unopposite' of an additive monoid homomorphism `Mᵃᵒᵖ →+ Nᵃᵒᵖ`. Inverse to `AddMonoidHom.op`."]
def MonoidHom.unop {M N} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N) :=
  MonoidHom.op.symm
Inverse of monoid homomorphism equivalence via opposites
Informal description
The inverse of the equivalence `MonoidHom.op`, which converts a monoid homomorphism between opposite monoids $f : M^\text{op} \to N^\text{op}$ back to a monoid homomorphism $f : M \to N$ by pre- and post-composing with the canonical operations of taking opposites (`op` and `unop`). This preserves the monoid structure.
MulEquiv.opOp definition
(M : Type*) [Mul M] : M ≃* Mᵐᵒᵖᵐᵒᵖ
Full source 
/-- A monoid is isomorphic to the opposite of its opposite. -/
@[to_additive (attr := simps!)
      "A additive monoid is isomorphic to the opposite of its opposite."]
def MulEquiv.opOp (M : Type*) [Mul M] : M ≃* Mᵐᵒᵖᵐᵒᵖ where
  __ := MulOpposite.opEquiv.trans MulOpposite.opEquiv
  map_mul' _ _ := rfl
Isomorphism between a multiplicative structure and its double opposite
Informal description
For any multiplicative structure $M$, there is a multiplicative isomorphism between $M$ and the opposite of its opposite $M^{\text{op}\text{op}}$. This isomorphism is constructed by composing the canonical equivalences that take $M$ to its opposite and back.
AddMonoidHom.mulOp definition
{M N} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ)
Full source 
/-- An additive homomorphism `M →+ N` can equivalently be viewed as an additive homomorphism
`Mᵐᵒᵖ →+ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps]
def AddMonoidHom.mulOp {M N} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ) where
  toFun f :=
    { toFun := MulOpposite.opMulOpposite.op ∘ f ∘ MulOpposite.unop, map_zero' := unop_injective f.map_zero,
      map_add' x y := unop_injective (f.map_add x.unop y.unop) }
  invFun f :=
    { toFun := MulOpposite.unopMulOpposite.unop ∘ f ∘ MulOpposite.op,
      map_zero' := congrArg MulOpposite.unop f.map_zero,
      map_add' :=
        fun x y => congrArg MulOpposite.unop (f.map_add (MulOpposite.op x) (MulOpposite.op y)) }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between additive homomorphisms and their opposite counterparts
Informal description
The equivalence between additive monoid homomorphisms $M \to^+ N$ and additive monoid homomorphisms $M^\text{op} \to^+ N^\text{op}$, where $M^\text{op}$ denotes the opposite monoid of $M$. Specifically, this defines: 1. A function that takes an additive homomorphism $f: M \to N$ and constructs a homomorphism $f^\text{op}: M^\text{op} \to N^\text{op}$ by composing with the opposite operations. 2. An inverse function that reverses this process. 3. Proofs that these operations are mutual inverses.
AddMonoidHom.mulUnop definition
{α β} [AddZeroClass α] [AddZeroClass β] : (αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)
Full source 
/-- The 'unopposite' of an additive monoid hom `αᵐᵒᵖ →+ βᵐᵒᵖ`. Inverse to
`AddMonoidHom.mul_op`. -/
@[simp]
def AddMonoidHom.mulUnop {α β} [AddZeroClass α] [AddZeroClass β] : (αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β) :=
  AddMonoidHom.mulOp.symm
Inverse of the opposite additive monoid homomorphism equivalence
Informal description
The inverse of the equivalence `AddMonoidHom.mulOp`, which converts an additive monoid homomorphism from the opposite of `α` to the opposite of `β` back to an additive monoid homomorphism from `α` to `β`. More precisely, this defines a bijection between: 1. Additive monoid homomorphisms $f: \alpha^\text{op} \to^+ \beta^\text{op}$ 2. Additive monoid homomorphisms $g: \alpha \to^+ \beta$ where $\alpha^\text{op}$ denotes the opposite monoid of $\alpha$.
AddEquiv.mulOp definition
{α β} [Add α] [Add β] : α ≃+ β ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ)
Full source 
/-- An iso `α ≃+ β` can equivalently be viewed as an iso `αᵐᵒᵖ ≃+ βᵐᵒᵖ`. -/
@[simps]
def AddEquiv.mulOp {α β} [Add α] [Add β] : α ≃+ βα ≃+ β ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ) where
  toFun f := opAddEquiv.symm.trans (f.trans opAddEquiv)
  invFun f := opAddEquiv.trans (f.trans opAddEquiv.symm)
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between additive group isomorphisms and their opposites
Informal description
For any additive groups $\alpha$ and $\beta$, there is a natural equivalence between the type of additive group isomorphisms $\alpha \simeq^+ \beta$ and the type of additive group isomorphisms $\alpha^\text{op} \simeq^+ \beta^\text{op}$. Specifically, this defines: 1. A function that takes an additive isomorphism $f: \alpha \simeq^+ \beta$ and constructs an isomorphism $\alpha^\text{op} \simeq^+ \beta^\text{op}$ by composing with the opposite operations. 2. An inverse function that reverses this process. 3. Proofs that these operations are mutual inverses.
AddEquiv.mulUnop definition
{α β} [Add α] [Add β] : αᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β)
Full source 
/-- The 'unopposite' of an iso `αᵐᵒᵖ ≃+ βᵐᵒᵖ`. Inverse to `AddEquiv.mul_op`. -/
@[simp]
def AddEquiv.mulUnop {α β} [Add α] [Add β] : αᵐᵒᵖαᵐᵒᵖ ≃+ βᵐᵒᵖαᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β) :=
  AddEquiv.mulOp.symm
Inverse of the opposite additive group isomorphism equivalence
Informal description
The inverse of the equivalence `AddEquiv.mulOp`, which converts an additive group isomorphism from the opposite of `α` to the opposite of `β` back to an additive group isomorphism from `α` to `β`. More precisely, this defines a bijection between: 1. Additive group isomorphisms $f: \alpha^\text{op} \simeq^+ \beta^\text{op}$ 2. Additive group isomorphisms $g: \alpha \simeq^+ \beta$ where $\alpha^\text{op}$ denotes the opposite group of $\alpha$.
MulEquiv.op definition
{α β} [Mul α] [Mul β] : α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)
Full source 
/-- An iso `α ≃* β` can equivalently be viewed as an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. -/
@[to_additive (attr := simps)
  "An iso `α ≃+ β` can equivalently be viewed as an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`."]
def MulEquiv.op {α β} [Mul α] [Mul β] : α ≃* βα ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ) where
  toFun f :=
    { toFun := MulOpposite.opMulOpposite.op ∘ f ∘ unop, invFun := MulOpposite.opMulOpposite.op ∘ f.symm ∘ unop,
      left_inv x := unop_injective (f.symm_apply_apply x.unop),
      right_inv x := unop_injective (f.apply_symm_apply x.unop),
      map_mul' x y := unop_injective (map_mul f y.unop x.unop) }
  invFun f :=
    { toFun := unopunop ∘ f ∘ MulOpposite.op, invFun := unopunop ∘ f.symm ∘ MulOpposite.op,
      left_inv x := by simp,
      right_inv x := by simp,
      map_mul' x y := congr_arg unop (map_mul f (MulOpposite.op y) (MulOpposite.op x)) }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between multiplicative equivalences and their opposites
Informal description
For any types $\alpha$ and $\beta$ equipped with multiplication operations, there is a natural equivalence between the type of multiplicative equivalences $\alpha \simeq^* \beta$ and the type of multiplicative equivalences $\alpha^\text{op} \simeq^* \beta^\text{op}$. The forward direction maps a multiplicative equivalence $f : \alpha \simeq^* \beta$ to the equivalence $\alpha^\text{op} \simeq^* \beta^\text{op}$ defined by composing with the opposite operations, and the inverse direction reverses this process.
MulEquiv.unop definition
{α β} [Mul α] [Mul β] : αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β)
Full source 
/-- The 'unopposite' of an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. Inverse to `MulEquiv.op`. -/
@[to_additive (attr := simp)
  "The 'unopposite' of an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`. Inverse to `AddEquiv.op`."]
def MulEquiv.unop {α β} [Mul α] [Mul β] : αᵐᵒᵖαᵐᵒᵖ ≃* βᵐᵒᵖαᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β) := MulEquiv.op.symm
Inverse of the opposite multiplicative group isomorphism equivalence
Informal description
The inverse of the equivalence `MulEquiv.op`, which converts a multiplicative group isomorphism from the opposite of `α` to the opposite of `β` back to a multiplicative group isomorphism from `α` to `β`. More precisely, this defines a bijection between: 1. Multiplicative group isomorphisms $f: \alpha^\text{op} \simeq^* \beta^\text{op}$ 2. Multiplicative group isomorphisms $g: \alpha \simeq^* \beta$ where $\alpha^\text{op}$ denotes the opposite group of $\alpha$.
AddMonoidHom.mul_op_ext theorem
{α β} [AddZeroClass α] [AddZeroClass β] (f g : αᵐᵒᵖ →+ β) (h : f.comp (opAddEquiv : α ≃+ αᵐᵒᵖ).toAddMonoidHom = g.comp (opAddEquiv : α ≃+ αᵐᵒᵖ).toAddMonoidHom) : f = g
Full source 
/-- This ext lemma changes equalities on `αᵐᵒᵖ →+ β` to equalities on `α →+ β`.
This is useful because there are often ext lemmas for specific `α`s that will apply
to an equality of `α →+ β` such as `Finsupp.addHom_ext'`. -/
@[ext]
lemma AddMonoidHom.mul_op_ext {α β} [AddZeroClass α] [AddZeroClass β] (f g : αᵐᵒᵖαᵐᵒᵖ →+ β)
    (h :
      f.comp (opAddEquiv : α ≃+ αᵐᵒᵖ).toAddMonoidHom =
        g.comp (opAddEquiv : α ≃+ αᵐᵒᵖ).toAddMonoidHom) :
    f = g :=
  AddMonoidHom.ext <| MulOpposite.rec' fun x => (DFunLike.congr_fun h :) x
Extensionality of Additive Monoid Homomorphisms via Opposite Group
Informal description
Let $\alpha$ and $\beta$ be additive monoids (or groups), and let $f, g \colon \alpha^\text{op} \to \beta$ be additive monoid homomorphisms. If the compositions $f \circ \text{op}$ and $g \circ \text{op}$ are equal, where $\text{op} \colon \alpha \to \alpha^\text{op}$ is the canonical additive equivalence, then $f = g$. Here, $\alpha^\text{op}$ denotes the opposite monoid (or group) of $\alpha$, where the addition is defined by $x +^\text{op} y = y + x$.