doc-next-gen

Mathlib.Algebra.Group.Equiv.Basic

Module docstring

{"# Multiplicative and additive equivs

This file contains basic results on MulEquiv and AddEquiv.

Tags

Equiv, MulEquiv, AddEquiv ","## Monoids "}

MulEquivClass.toMulEquiv_injective theorem
[Mul α] [Mul β] [MulEquivClass F α β] : Function.Injective ((↑) : F → α ≃* β)
Full source 
@[to_additive]
theorem MulEquivClass.toMulEquiv_injective [Mul α] [Mul β] [MulEquivClass F α β] :
    Function.Injective ((↑) : F → α ≃* β) :=
  fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e
Injectivity of the Canonical Map from Multiplicative Equivalence Class to Multiplicative Equivalences
Informal description
For any multiplicative structures $\alpha$ and $\beta$, and any type $F$ in the `MulEquivClass` of multiplicative equivalences between $\alpha$ and $\beta$, the canonical map from $F$ to the type $\alpha \simeq^* \beta$ of multiplicative equivalences is injective. In other words, if two elements of $F$ induce the same multiplicative equivalence when coerced, then they must be equal.
MulEquiv.ofUnique definition
{M N} [Unique M] [Unique N] [Mul M] [Mul N] : M ≃* N
Full source 
/-- The `MulEquiv` between two monoids with a unique element. -/
@[to_additive "The `AddEquiv` between two `AddMonoid`s with a unique element."]
def ofUnique {M N} [Unique M] [Unique N] [Mul M] [Mul N] : M ≃* N :=
  { Equiv.ofUnique M N with map_mul' := fun _ _ => Subsingleton.elim _ _ }
Multiplicative equivalence between monoids with unique elements
Informal description
Given two monoids $M$ and $N$ each with a unique element, there exists a multiplicative equivalence (i.e., a bijective homomorphism) between them. The equivalence maps the unique element of $M$ to the unique element of $N$ and preserves the multiplication operation.
MulEquiv.instUnique instance
{M N} [Unique M] [Unique N] [Mul M] [Mul N] : Unique (M ≃* N)
Full source 
/-- There is a unique monoid homomorphism between two monoids with a unique element. -/
@[to_additive "There is a unique additive monoid homomorphism between two additive monoids with
  a unique element."]
instance {M N} [Unique M] [Unique N] [Mul M] [Mul N] : Unique (M ≃* N) where
  default := ofUnique
  uniq _ := ext fun _ => Subsingleton.elim _ _
Uniqueness of Multiplicative Equivalence Between Monoids with Unique Elements
Informal description
For any two monoids $M$ and $N$ each with a unique element and equipped with multiplication operations, there is a unique multiplicative equivalence (i.e., a bijective homomorphism) between them.
MulEquiv.arrowCongr definition
{M N P Q : Type*} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) : (M → P) ≃* (N → Q)
Full source 
/-- A multiplicative analogue of `Equiv.arrowCongr`,
where the equivalence between the targets is multiplicative.
-/
@[to_additive (attr := simps apply) "An additive analogue of `Equiv.arrowCongr`,
  where the equivalence between the targets is additive."]
def arrowCongr {M N P Q : Type*} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) :
    (M → P) ≃* (N → Q) where
  toFun h n := g (h (f.symm n))
  invFun k m := g.symm (k (f m))
  left_inv h := by ext; simp
  right_inv k := by ext; simp
  map_mul' h k := by ext; simp
Multiplicative equivalence of function spaces via conjugation
Informal description
Given a bijection $f : M \simeq N$ between types $M$ and $N$, and a multiplicative equivalence $g : P \simeq^* Q$ between multiplicative structures on $P$ and $Q$, the structure `MulEquiv.arrowCongr` defines a multiplicative equivalence between the function spaces $M \to P$ and $N \to Q$. The equivalence maps a function $h : M \to P$ to the function $n \mapsto g(h(f^{-1}(n)))$, and its inverse maps a function $k : N \to Q$ to $m \mapsto g^{-1}(k(f(m)))$. This equivalence preserves the multiplicative structure of the function spaces.
MulEquiv.monoidHomCongr definition
{M N P Q} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) : (M →* P) ≃* (N →* Q)
Full source 
/-- A multiplicative analogue of `Equiv.arrowCongr`,
for multiplicative maps from a monoid to a commutative monoid.
-/
@[to_additive (attr := simps apply)
  "An additive analogue of `Equiv.arrowCongr`,
  for additive maps from an additive monoid to a commutative additive monoid."]
def monoidHomCongr {M N P Q} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q]
    (f : M ≃* N) (g : P ≃* Q) : (M →* P) ≃* (N →* Q) where
  toFun h := g.toMonoidHom.comp (h.comp f.symm.toMonoidHom)
  invFun k := g.symm.toMonoidHom.comp (k.comp f.toMonoidHom)
  left_inv h := by ext; simp
  right_inv k := by ext; simp
  map_mul' h k := by ext; simp
Multiplicative equivalence of monoid homomorphism spaces via conjugation
Informal description
Given multiplicative equivalences $f : M \simeq N$ between monoids $M$ and $N$, and $g : P \simeq Q$ between commutative monoids $P$ and $Q$, the structure `MulEquiv.monoidHomCongr` defines a multiplicative equivalence between the monoid homomorphisms $M \to P$ and $N \to Q$. The equivalence is constructed by conjugating with $f$ and $g$, i.e., a homomorphism $h : M \to P$ is mapped to $g \circ h \circ f^{-1} : N \to Q$, and similarly for the inverse direction.
MulEquiv.piCongrRight definition
{η : Type*} {Ms Ns : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)] (es : ∀ j, Ms j ≃* Ns j) : (∀ j, Ms j) ≃* ∀ j, Ns j
Full source 
/-- A family of multiplicative equivalences `Π j, (Ms j ≃* Ns j)` generates a
multiplicative equivalence between `Π j, Ms j` and `Π j, Ns j`.

This is the `MulEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`MulEquiv.arrowCongr`.
-/
@[to_additive (attr := simps apply)
  "A family of additive equivalences `Π j, (Ms j ≃+ Ns j)`
  generates an additive equivalence between `Π j, Ms j` and `Π j, Ns j`.

  This is the `AddEquiv` version of `Equiv.piCongrRight`, and the dependent version of
  `AddEquiv.arrowCongr`."]
def piCongrRight {η : Type*} {Ms Ns : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)]
    (es : ∀ j, Ms j ≃* Ns j) : (∀ j, Ms j) ≃* ∀ j, Ns j :=
  { Equiv.piCongrRight fun j => (es j).toEquiv with
    toFun := fun x j => es j (x j),
    invFun := fun x j => (es j).symm (x j),
    map_mul' := fun x y => funext fun j => map_mul (es j) (x j) (y j) }
Multiplicative equivalence of product types via component-wise multiplicative equivalences
Informal description
Given an index type $\eta$ and families of multiplicative structures $(Ms_j)_{j \in \eta}$ and $(Ns_j)_{j \in \eta}$, along with a family of multiplicative equivalences $(es_j : Ms_j \simeq^* Ns_j)_{j \in \eta}$, there is a multiplicative equivalence between the product types $\prod_{j \in \eta} Ms_j$ and $\prod_{j \in \eta} Ns_j$. This equivalence is constructed by applying each $es_j$ component-wise to the elements of the product types, and it preserves the multiplicative structure.
MulEquiv.piCongrRight_refl theorem
{η : Type*} {Ms : η → Type*} [∀ j, Mul (Ms j)] : (piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl _
Full source 
@[to_additive (attr := simp)]
theorem piCongrRight_refl {η : Type*} {Ms : η → Type*} [∀ j, Mul (Ms j)] :
    (piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl _ := rfl
Identity Component-wise Multiplicative Equivalence Yields Identity on Product
Informal description
For any index type $\eta$ and family of multiplicative structures $(Ms_j)_{j \in \eta}$, the multiplicative equivalence obtained by applying the identity equivalence component-wise to each $Ms_j$ is equal to the identity equivalence on the product type $\prod_{j \in \eta} Ms_j$.
MulEquiv.piCongrRight_symm theorem
{η : Type*} {Ms Ns : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)] (es : ∀ j, Ms j ≃* Ns j) : (piCongrRight es).symm = piCongrRight fun i => (es i).symm
Full source 
@[to_additive (attr := simp)]
theorem piCongrRight_symm {η : Type*} {Ms Ns : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)]
    (es : ∀ j, Ms j ≃* Ns j) : (piCongrRight es).symm = piCongrRight fun i => (es i).symm := rfl
Inverse of Component-wise Multiplicative Equivalence of Product Types
Informal description
Given an index type $\eta$ and families of multiplicative structures $(Ms_j)_{j \in \eta}$ and $(Ns_j)_{j \in \eta}$, along with a family of multiplicative equivalences $(es_j : Ms_j \simeq^* Ns_j)_{j \in \eta}$, the inverse of the multiplicative equivalence $\prod_{j \in \eta} Ms_j \simeq^* \prod_{j \in \eta} Ns_j$ (constructed component-wise via $es_j$) is equal to the multiplicative equivalence constructed component-wise via the inverses $(es_j)^{-1} : Ns_j \simeq^* Ms_j$.
MulEquiv.piCongrRight_trans theorem
{η : Type*} {Ms Ns Ps : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)] [∀ j, Mul (Ps j)] (es : ∀ j, Ms j ≃* Ns j) (fs : ∀ j, Ns j ≃* Ps j) : (piCongrRight es).trans (piCongrRight fs) = piCongrRight fun i => (es i).trans (fs i)
Full source 
@[to_additive (attr := simp)]
theorem piCongrRight_trans {η : Type*} {Ms Ns Ps : η → Type*} [∀ j, Mul (Ms j)]
    [∀ j, Mul (Ns j)] [∀ j, Mul (Ps j)] (es : ∀ j, Ms j ≃* Ns j) (fs : ∀ j, Ns j ≃* Ps j) :
    (piCongrRight es).trans (piCongrRight fs) = piCongrRight fun i => (es i).trans (fs i) := rfl
Composition of Component-wise Multiplicative Equivalences
Informal description
Let $\eta$ be an index type and $(Ms_j)_{j \in \eta}$, $(Ns_j)_{j \in \eta}$, $(Ps_j)_{j \in \eta}$ be families of multiplicative types. Given families of multiplicative equivalences $(es_j : Ms_j \simeq^* Ns_j)_{j \in \eta}$ and $(fs_j : Ns_j \simeq^* Ps_j)_{j \in \eta}$, the composition of the component-wise multiplicative equivalences $\prod_{j \in \eta} es_j$ and $\prod_{j \in \eta} fs_j$ is equal to the component-wise composition of the individual equivalences, i.e., \[ \left(\prod_{j \in \eta} es_j\right) \circ \left(\prod_{j \in \eta} fs_j\right) = \prod_{j \in \eta} (es_j \circ fs_j). \]
MulEquiv.piUnique definition
{ι : Type*} (M : ι → Type*) [∀ j, Mul (M j)] [Unique ι] : (∀ j, M j) ≃* M default
Full source 
/-- A family indexed by a type with a unique element
is `MulEquiv` to the element at the single index. -/
@[to_additive (attr := simps!)
  "A family indexed by a type with a unique element
  is `AddEquiv` to the element at the single index."]
def piUnique {ι : Type*} (M : ι → Type*) [∀ j, Mul (M j)] [Unique ι] :
    (∀ j, M j) ≃* M default :=
  { Equiv.piUnique M with map_mul' := fun _ _ => Pi.mul_apply _ _ _ }
Multiplicative equivalence between dependent functions on a unique type and their value at the default element
Informal description
Given a type `ι` with a unique element (i.e., `[Unique ι]`) and a family of multiplicative types `M : ι → Type*` (i.e., `[∀ j, Mul (M j)]`), there is a multiplicative equivalence between the product type `(∀ j, M j)` (the type of dependent functions on `ι`) and `M default` (the type at the default element of `ι`). This equivalence maps a dependent function `f` to its value at the default element, and conversely, any element of `M default` can be uniquely extended to a dependent function on `ι` via the unique elimination principle. The equivalence preserves multiplication, meaning that the product of two functions is mapped to the product of their values at the default element.
MonoidHom.precompEquiv definition
{α β : Type*} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type*) [Monoid γ] : (β →* γ) ≃ (α →* γ)
Full source 
/-- The equivalence `(β →* γ) ≃ (α →* γ)` obtained by precomposition with
a multiplicative equivalence `e : α ≃* β`. -/
@[to_additive (attr := simps)
"The equivalence `(β →+ γ) ≃ (α →+ γ)` obtained by precomposition with
an additive equivalence `e : α ≃+ β`."]
def precompEquiv {α β : Type*} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type*) [Monoid γ] :
    (β →* γ) ≃ (α →* γ) where
  toFun f := f.comp e
  invFun g := g.comp e.symm
  left_inv _ := by ext; simp
  right_inv _ := by ext; simp
Precomposition equivalence for monoid homomorphisms
Informal description
Given monoids $\alpha$, $\beta$, and $\gamma$, and a multiplicative equivalence $e : \alpha \simeq^* \beta$, the equivalence $\text{MonoidHom.precompEquiv}$ maps between the types of monoid homomorphisms $\beta \to^* \gamma$ and $\alpha \to^* \gamma$ by precomposition with $e$ or its inverse $e^{-1}$. Specifically: - The forward direction sends a homomorphism $f : \beta \to^* \gamma$ to $f \circ e : \alpha \to^* \gamma$. - The backward direction sends a homomorphism $g : \alpha \to^* \gamma$ to $g \circ e^{-1} : \beta \to^* \gamma$.
MonoidHom.postcompEquiv definition
{α β : Type*} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type*) [Monoid γ] : (γ →* α) ≃ (γ →* β)
Full source 
/-- The equivalence `(γ →* α) ≃ (γ →* β)` obtained by postcomposition with
a multiplicative equivalence `e : α ≃* β`. -/
@[to_additive (attr := simps)
"The equivalence `(γ →+ α) ≃ (γ →+ β)` obtained by postcomposition with
an additive equivalence `e : α ≃+ β`."]
def postcompEquiv {α β : Type*} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type*) [Monoid γ] :
    (γ →* α) ≃ (γ →* β) where
  toFun f := e.toMonoidHom.comp f
  invFun g := e.symm.toMonoidHom.comp g
  left_inv _ := by ext; simp
  right_inv _ := by ext; simp
Postcomposition equivalence for monoid homomorphisms
Informal description
Given monoids $\alpha$, $\beta$, and $\gamma$, and a multiplicative equivalence $e : \alpha \simeq^* \beta$, the equivalence $\text{MonoidHom.postcompEquiv}$ maps between the types of monoid homomorphisms $\gamma \to^* \alpha$ and $\gamma \to^* \beta$ by postcomposition with $e$ or its inverse $e^{-1}$. Specifically: - The forward direction sends a homomorphism $f : \gamma \to^* \alpha$ to $e \circ f : \gamma \to^* \beta$. - The backward direction sends a homomorphism $g : \gamma \to^* \beta$ to $e^{-1} \circ g : \gamma \to^* \alpha$.
Equiv.inv definition
: Perm G
Full source 
/-- Inversion on a `Group` or `GroupWithZero` is a permutation of the underlying type. -/
@[to_additive (attr := simps! -fullyApplied apply)
    "Negation on an `AddGroup` is a permutation of the underlying type."]
protected def inv : Perm G :=
  inv_involutive.toPerm _
Inversion permutation of a group
Informal description
The permutation on a group $G$ induced by the inversion operation $x \mapsto x^{-1}$, which is a bijective map since inversion is involutive (i.e., $(x^{-1})^{-1} = x$ for all $x \in G$).
Equiv.inv_symm theorem
: (Equiv.inv G).symm = Equiv.inv G
Full source 
@[to_additive (attr := simp)]
theorem inv_symm : (Equiv.inv G).symm = Equiv.inv G := rfl
Inversion Permutation is Self-Inverse
Informal description
For any group $G$, the inverse of the inversion permutation $\text{Equiv.inv} : \text{Perm}(G)$ is equal to itself, i.e., $(\text{Equiv.inv})^{-1} = \text{Equiv.inv}$.