Mathlib.Algebra.Group.Equiv.Defs

EmbeddingLike.map_eq_one_iff theorem

{f : F} {x : M} : f x = 1 ↔ x = 1

Full source

@[to_additive (attr := simp)]
theorem map_eq_one_iff {f : F} {x : M} :
    f x = 1 ↔ x = 1 :=
  _root_.map_eq_one_iff f (EmbeddingLike.injective f)

Identity Preservation under Injective Homomorphisms: $f(x) = 1 \leftrightarrow x = 1$

Informal description

For any embedding-like function $f : F$ between monoids $M$ and $N$ (where $F$ preserves the identity element), and for any element $x \in M$, we have $f(x) = 1$ if and only if $x = 1$.

EmbeddingLike.map_ne_one_iff theorem

{f : F} {x : M} : f x ≠ 1 ↔ x ≠ 1

Full source

@[to_additive]
theorem map_ne_one_iff {f : F} {x : M} :
    f x ≠ 1f x ≠ 1 ↔ x ≠ 1 :=
  map_eq_one_iff.not

Non-Identity Preservation under Injective Homomorphisms: $f(x) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any embedding-like function $f \colon F$ between monoids $M$ and $N$ (where $F$ preserves the identity element), and for any element $x \in M$, we have $f(x) \neq 1$ if and only if $x \neq 1$.

AddEquiv structure

(A B : Type*) [Add A] [Add B] extends A ≃ B, AddHom A B

Full source

/-- `AddEquiv α β` is the type of an equiv `α ≃ β` which preserves addition. -/
structure AddEquiv (A B : Type*) [Add A] [Add B] extends A ≃ B, AddHom A B

Additive equivalence (additive isomorphism)

Informal description

The structure `AddEquiv α β` represents an equivalence (bijective map) between two types `α` and `β` equipped with addition operations, which preserves the addition structure. That is, for any `x, y ∈ α`, the equivalence `f : α ≃ β` satisfies `f(x + y) = f(x) + f(y)`.

AddEquivClass structure

(F : Type*) (A B : outParam Type*) [Add A] [Add B] [EquivLike F A B]

Full source

/-- `AddEquivClass F A B` states that `F` is a type of addition-preserving morphisms.
You should extend this class when you extend `AddEquiv`. -/
class AddEquivClass (F : Type*) (A B : outParam Type*) [Add A] [Add B] [EquivLike F A B] :
    Prop where
  /-- Preserves addition. -/
  map_add : ∀ (f : F) (a b), f (a + b) = f a + f b

Additive Equivalence Class

Informal description

The class `AddEquivClass F A B` states that `F` is a type of additive equivalence-preserving morphisms between types `A` and `B`, where both `A` and `B` are equipped with addition operations. This means that any element `f : F` is a bijection that preserves addition, i.e., for any `x, y ∈ A`, the equivalence `f` satisfies `f(x + y) = f(x) + f(y)`.

MulEquiv structure

(M N : Type*) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

Full source

/-- `MulEquiv α β` is the type of an equiv `α ≃ β` which preserves multiplication. -/
@[to_additive]
structure MulEquiv (M N : Type*) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

Multiplicative equivalence (or multiplicative isomorphism)

Informal description

The structure `MulEquiv M N` represents a multiplicative equivalence between types `M` and `N` equipped with multiplication operations. It consists of a bijection `M ≃ N` that preserves multiplication, i.e., for any `x, y ∈ M`, the equivalence maps `x * y` in `M` to `f(x) * f(y)` in `N`.

term_≃*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for a `MulEquiv`. -/
infixl:25 " ≃* " => MulEquiv

Multiplicative equivalence notation (`≃*`)

Informal description

The notation `≃*` denotes a multiplicative equivalence between two types with multiplication, i.e., a bijective map that preserves the multiplicative structure.

term_≃+_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for an `AddEquiv`. -/
infixl:25 " ≃+ " => AddEquiv

Additive equivalence notation

Informal description

The notation `≃+` represents an additive equivalence between two additive structures, i.e., a bijective map that preserves addition. This is used to denote isomorphisms of additive monoids or additive groups.

MulEquiv.toEquiv_injective theorem

{α β : Type*} [Mul α] [Mul β] : Function.Injective (toEquiv : (α ≃* β) → (α ≃ β))

Full source

@[to_additive]
lemma MulEquiv.toEquiv_injective {α β : Type*} [Mul α] [Mul β] :
    Function.Injective (toEquiv : (α ≃* β) → (α ≃ β))
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

Injectivity of the Underlying Equivalence in Multiplicative Isomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with multiplication operations, the function that maps a multiplicative equivalence $f : \alpha \simeq^* \beta$ to its underlying equivalence $f : \alpha \simeq \beta$ is injective.

MulEquivClass structure

(F : Type*) (A B : outParam Type*) [Mul A] [Mul B] [EquivLike F A B]

Full source

/-- `MulEquivClass F A B` states that `F` is a type of multiplication-preserving morphisms.
You should extend this class when you extend `MulEquiv`. -/
-- TODO: make this a synonym for MulHomClass?
@[to_additive]
class MulEquivClass (F : Type*) (A B : outParam Type*) [Mul A] [Mul B] [EquivLike F A B] :
    Prop where
  /-- Preserves multiplication. -/
  map_mul : ∀ (f : F) (a b), f (a * b) = f a * f b

Multiplicative Equivalence Class

Informal description

The class `MulEquivClass F A B` states that `F` is a type of multiplicative equivalences between types `A` and `B`, where both `A` and `B` are equipped with multiplication operations. These equivalences preserve the multiplicative structure, meaning they are bijective maps that respect multiplication. This class extends `EquivLike`, which provides the foundation for bijective coercions between types.

MulEquivClass.instMulHomClass instance

(F : Type*) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] : MulHomClass F M N

Full source

@[to_additive]
instance (priority := 100) instMulHomClass (F : Type*)
    [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] : MulHomClass F M N :=
  { h with }

Multiplicative Equivalences as Multiplication-Preserving Homomorphisms

Informal description

For any type `F` that represents multiplicative equivalences between multiplicative structures `M` and `N`, if `F` is an instance of `MulEquivClass`, then `F` is also an instance of `MulHomClass`. This means that every multiplicative equivalence in `F` preserves the multiplication operation, satisfying `f (x * y) = f x * f y` for all `x, y ∈ M`.

MulEquivClass.instMonoidHomClass instance

[MulOneClass M] [MulOneClass N] [MulEquivClass F M N] : MonoidHomClass F M N

Full source

@[to_additive]
instance (priority := 100) instMonoidHomClass
    [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
    MonoidHomClass F M N :=
  { MulEquivClass.instMulHomClass F with
    map_one := fun e =>
      calc
        e 1 = e 1 * 1 := (mul_one _).symm
        _ = e 1 * e (EquivLike.inv e (1 : N) : M) :=
          congr_arg _ (EquivLike.right_inv e 1).symm
        _ = e (EquivLike.inv e (1 : N)) := by rw [← map_mul, one_mul]
        _ = 1 := EquivLike.right_inv e 1 }

Multiplicative Equivalences as Monoid Homomorphisms

Informal description

For any multiplicative equivalence class $F$ between monoids $M$ and $N$ (both equipped with identity elements and multiplication operations), every element of $F$ is also a monoid homomorphism. This means that multiplicative equivalences preserve both the multiplication operation and the identity element, satisfying $f(x * y) = f(x) * f(y)$ for all $x, y \in M$ and $f(1) = 1$.

MulEquivClass.toMulEquiv definition

[Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β

Full source

/-- Turn an element of a type `F` satisfying `MulEquivClass F α β` into an actual
`MulEquiv`. This is declared as the default coercion from `F` to `α ≃* β`. -/
@[to_additive (attr := coe)
"Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual
`AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`."]
def MulEquivClass.toMulEquiv [Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β :=
  { (f : α ≃ β), (f : α →ₙ* β) with }

Conversion from multiplicative equivalence class to explicit multiplicative equivalence

Informal description

Given types $\alpha$ and $\beta$ equipped with multiplication operations and a type $F$ satisfying `MulEquivClass F α β`, the function converts an element $f : F$ into an explicit multiplicative equivalence $\alpha \simeq^* \beta$. This equivalence consists of: 1. A bijection between $\alpha$ and $\beta$ (as an $\alpha \simeq \beta$), 2. A multiplicative homomorphism preserving the operation (as an $\alpha \to^* \beta$).

instCoeTCMulEquivOfMulEquivClass instance

[Mul α] [Mul β] [MulEquivClass F α β] : CoeTC F (α ≃* β)

Full source

/-- Any type satisfying `MulEquivClass` can be cast into `MulEquiv` via
`MulEquivClass.toMulEquiv`. -/
@[to_additive "Any type satisfying `AddEquivClass` can be cast into `AddEquiv` via
`AddEquivClass.toAddEquiv`. "]
instance [Mul α] [Mul β] [MulEquivClass F α β] : CoeTC F (α ≃* β) :=
  ⟨MulEquivClass.toMulEquiv⟩

Canonical Conversion from Multiplicative Equivalence Class to Multiplicative Equivalence

Informal description

For any types $\alpha$ and $\beta$ equipped with multiplication operations, and any type $F$ satisfying `MulEquivClass F α β`, there is a canonical way to treat elements of $F$ as multiplicative equivalences $\alpha \simeq^* \beta$. This means that any $f : F$ can be automatically converted into a bijection between $\alpha$ and $\beta$ that preserves multiplication.

MulEquiv.instEquivLike instance

: EquivLike (M ≃* N) M N

Full source

@[to_additive]
instance : EquivLike (M ≃* N) M N where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁ h₂ := by
    cases f
    cases g
    congr
    apply Equiv.coe_fn_injective h₁

Multiplicative Equivalence as Equivalence-like Structure

Informal description

For any multiplicative equivalence $M \simeq^* N$ between types $M$ and $N$ equipped with multiplication operations, there is an equivalence-like structure that allows coercing the multiplicative equivalence to a bijection between $M$ and $N$.

MulEquiv.instCoeFunForall instance

: CoeFun (M ≃* N) fun _ ↦ M → N

Full source

@[to_additive] -- shortcut instance that doesn't generate any subgoals
instance : CoeFun (M ≃* N) fun _ ↦ M → N where
  coe f := f

Multiplicative Equivalence as Function

Informal description

For any multiplicative equivalence $M \simeq^* N$ between types $M$ and $N$ equipped with multiplication operations, there is a canonical way to treat it as a function from $M$ to $N$.

MulEquiv.instMulEquivClass instance

: MulEquivClass (M ≃* N) M N

Full source

@[to_additive]
instance : MulEquivClass (M ≃* N) M N where
  map_mul f := f.map_mul'

Multiplicative Equivalence Class for MulEquiv

Informal description

For any multiplicative equivalence $M \simeq^* N$ between types $M$ and $N$ equipped with multiplication operations, the structure $M \simeq^* N$ forms a multiplicative equivalence class. This means that multiplicative equivalences preserve the multiplicative structure, i.e., they are bijective maps that respect multiplication.

MulEquiv.ext theorem

{f g : MulEquiv M N} (h : ∀ x, f x = g x) : f = g

Full source

/-- Two multiplicative isomorphisms agree if they are defined by the
same underlying function. -/
@[to_additive (attr := ext)
  "Two additive isomorphisms agree if they are defined by the same underlying function."]
theorem ext {f g : MulEquiv M N} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Multiplicative Isomorphisms

Informal description

For any two multiplicative isomorphisms $f, g : M \simeq^* N$ between monoids $M$ and $N$, if $f(x) = g(x)$ for all $x \in M$, then $f = g$.

MulEquiv.congr_arg theorem

{f : MulEquiv M N} {x x' : M} : x = x' → f x = f x'

Full source

@[to_additive]
protected theorem congr_arg {f : MulEquiv M N} {x x' : M} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

Multiplicative Equivalence Preserves Equality: $x = x' \implies f(x) = f(x')$

Informal description

For any multiplicative equivalence $f : M \simeq^* N$ between monoids $M$ and $N$, and any elements $x, x' \in M$, if $x = x'$, then $f(x) = f(x')$.

MulEquiv.congr_fun theorem

{f g : MulEquiv M N} (h : f = g) (x : M) : f x = g x

Full source

@[to_additive]
protected theorem congr_fun {f g : MulEquiv M N} (h : f = g) (x : M) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Multiplicative Equivalences

Informal description

For any multiplicative equivalences $f, g : M \simeq^* N$ between monoids $M$ and $N$, if $f = g$, then for all $x \in M$, we have $f(x) = g(x)$.

MulEquiv.coe_mk theorem

(f : M ≃ N) (hf : ∀ x y, f (x * y) = f x * f y) : (mk f hf : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem coe_mk (f : M ≃ N) (hf : ∀ x y, f (x * y) = f x * f y) : (mk f hf : M → N) = f := rfl

Underlying Function of Multiplicative Equivalence Construction

Informal description

Given a bijection $f \colon M \to N$ between multiplicative structures $M$ and $N$, and a proof $hf$ that $f$ preserves multiplication (i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M$), the underlying function of the multiplicative equivalence constructed from $f$ and $hf$ is equal to $f$ itself.

MulEquiv.mk_coe theorem

(e : M ≃* N) (e' h₁ h₂ h₃) : (⟨⟨e, e', h₁, h₂⟩, h₃⟩ : M ≃* N) = e

Full source

@[to_additive (attr := simp)]
theorem mk_coe (e : M ≃* N) (e' h₁ h₂ h₃) : (⟨⟨e, e', h₁, h₂⟩, h₃⟩ : M ≃* N) = e :=
  ext fun _ => rfl

Constructed Multiplicative Equivalence Equals Original

Informal description

Given a multiplicative equivalence $e \colon M \simeq^* N$ between monoids $M$ and $N$, and components $e'$, $h₁$, $h₂$, $h₃$ constructing a new multiplicative equivalence, the constructed equivalence $\langle \langle e, e', h₁, h₂ \rangle, h₃ \rangle$ is equal to $e$.

MulEquiv.toEquiv_eq_coe theorem

(f : M ≃* N) : f.toEquiv = f

Full source

@[to_additive (attr := simp)]
theorem toEquiv_eq_coe (f : M ≃* N) : f.toEquiv = f :=
  rfl

Equality of Underlying Equivalence and Coercion in Multiplicative Isomorphism

Informal description

For any multiplicative equivalence $f \colon M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying equivalence $f.\text{toEquiv}$ is equal to $f$ when viewed as a function.

MulEquiv.toMulHom_eq_coe theorem

(f : M ≃* N) : f.toMulHom = ↑f

Full source

/-- The `simp`-normal form to turn something into a `MulHom` is via `MulHomClass.toMulHom`. -/
@[to_additive (attr := simp)]
theorem toMulHom_eq_coe (f : M ≃* N) : f.toMulHom = ↑f :=
  rfl

Equality of Multiplicative Homomorphism and Coercion in Multiplicative Isomorphism

Informal description

For any multiplicative isomorphism $f \colon M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying multiplicative homomorphism $f.\text{toMulHom}$ is equal to $f$ when viewed as a function.

MulEquiv.toFun_eq_coe theorem

(f : M ≃* N) : f.toFun = f

Full source

@[to_additive]
theorem toFun_eq_coe (f : M ≃* N) : f.toFun = f := rfl

Equality of Underlying Function and Coercion in Multiplicative Equivalence

Informal description

For any multiplicative equivalence $f : M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying function $f.\text{toFun}$ is equal to $f$ itself when viewed as a function.

MulEquiv.coe_toEquiv theorem

(f : M ≃* N) : ⇑(f : M ≃ N) = f

Full source

/-- `simp`-normal form of `toFun_eq_coe`. -/
@[to_additive (attr := simp)]
theorem coe_toEquiv (f : M ≃* N) : ⇑(f : M ≃ N) = f := rfl

Equality of Underlying Equivalence Function and Multiplicative Equivalence

Informal description

For any multiplicative equivalence $f : M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying function of the equivalence $f$ (viewed as a plain equivalence $M \simeq N$) is equal to $f$ itself when viewed as a function.

MulEquiv.coe_toMulHom theorem

{f : M ≃* N} : (f.toMulHom : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem coe_toMulHom {f : M ≃* N} : (f.toMulHom : M → N) = f := rfl

Coincidence of Multiplicative Homomorphism and Equivalence

Informal description

For any multiplicative equivalence $f : M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying multiplicative homomorphism $f.\text{toMulHom}$ coincides with $f$ when viewed as a function from $M$ to $N$.

MulEquiv.mk' definition

(f : M ≃ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃* N

Full source

/-- Makes a multiplicative isomorphism from a bijection which preserves multiplication. -/
@[to_additive "Makes an additive isomorphism from a bijection which preserves addition."]
def mk' (f : M ≃ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃* N := ⟨f, h⟩

Multiplicative isomorphism from bijection preserving multiplication

Informal description

Given a bijection $f : M \to N$ between two multiplicative structures that preserves multiplication (i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M$), this constructs a multiplicative isomorphism (equivalence) between $M$ and $N$.

MulEquiv.map_mul theorem

(f : M ≃* N) : ∀ x y, f (x * y) = f x * f y

Full source

/-- A multiplicative isomorphism preserves multiplication. -/
@[to_additive "An additive isomorphism preserves addition."]
protected theorem map_mul (f : M ≃* N) : ∀ x y, f (x * y) = f x * f y :=
  map_mul f

Multiplicative Isomorphism Preserves Multiplication

Informal description

For any multiplicative isomorphism $f \colon M \to N$ between multiplicative structures $M$ and $N$, the map $f$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M$.

MulEquiv.bijective theorem

(e : M ≃* N) : Function.Bijective e

Full source

@[to_additive]
protected theorem bijective (e : M ≃* N) : Function.Bijective e :=
  EquivLike.bijective e

Bijectivity of Multiplicative Isomorphisms

Informal description

For any multiplicative isomorphism $e \colon M \to N$ between multiplicative structures $M$ and $N$, the map $e$ is bijective, meaning it is both injective and surjective.

MulEquiv.injective theorem

(e : M ≃* N) : Function.Injective e

Full source

@[to_additive]
protected theorem injective (e : M ≃* N) : Function.Injective e :=
  EquivLike.injective e

Injectivity of multiplicative isomorphisms

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying function $e : M \to N$ is injective.

MulEquiv.surjective theorem

(e : M ≃* N) : Function.Surjective e

Full source

@[to_additive]
protected theorem surjective (e : M ≃* N) : Function.Surjective e :=
  EquivLike.surjective e

Surjectivity of Multiplicative Isomorphisms

Informal description

For any multiplicative equivalence (isomorphism) $e : M \simeq^* N$ between multiplicative structures $M$ and $N$, the underlying function $e : M \to N$ is surjective.

MulEquiv.apply_eq_iff_eq theorem

(e : M ≃* N) {x y : M} : e x = e y ↔ x = y

Full source

@[to_additive]
theorem apply_eq_iff_eq (e : M ≃* N) {x y : M} : e x = e y ↔ x = y :=
  e.injective.eq_iff

Multiplicative isomorphism preserves equality

Informal description

For any multiplicative isomorphism $e \colon M \simeq^* N$ between multiplicative structures $M$ and $N$, and for any elements $x, y \in M$, we have $e(x) = e(y)$ if and only if $x = y$.

MulEquiv.refl definition

(M : Type*) [Mul M] : M ≃* M

Full source

/-- The identity map is a multiplicative isomorphism. -/
@[to_additive (attr := refl) "The identity map is an additive isomorphism."]
def refl (M : Type*) [Mul M] : M ≃* M :=
  { Equiv.refl _ with map_mul' := fun _ _ => rfl }

Multiplicative identity isomorphism

Informal description

The multiplicative identity isomorphism on a type $M$ equipped with a multiplication operation, which is the bijection from $M$ to itself given by the identity function, preserving multiplication (i.e., $x * y$ maps to $x * y$).

MulEquiv.instInhabited instance

: Inhabited (M ≃* M)

Full source

@[to_additive]
instance : Inhabited (M ≃* M) := ⟨refl M⟩

Existence of Multiplicative Self-Equivalences

Informal description

For any type $M$ equipped with a multiplication operation, the type of multiplicative equivalences $M \simeq^* M$ is inhabited.

MulEquiv.coe_refl theorem

: ↑(refl M) = id

Full source

@[to_additive (attr := simp)]
theorem coe_refl : ↑(refl M) = id := rfl

Identity Multiplicative Isomorphism Coerces to Identity Function

Informal description

The coercion of the multiplicative identity isomorphism $\text{refl}_M$ to a function is equal to the identity function $\text{id}$ on $M$.

MulEquiv.refl_apply theorem

(m : M) : refl M m = m

Full source

@[to_additive (attr := simp)]
theorem refl_apply (m : M) : refl M m = m := rfl

Identity Multiplicative Isomorphism Acts as Identity Function

Informal description

For any element $m$ in a multiplicative structure $M$, the multiplicative identity isomorphism $\text{refl}_M$ maps $m$ to itself, i.e., $\text{refl}_M(m) = m$.

MulEquiv.symm_map_mul theorem

{M N : Type*} [Mul M] [Mul N] (h : M ≃* N) (x y : N) : h.symm (x * y) = h.symm x * h.symm y

Full source

/-- An alias for `h.symm.map_mul`. Introduced to fix the issue in
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth
-/
@[to_additive]
lemma symm_map_mul {M N : Type*} [Mul M] [Mul N] (h : M ≃* N) (x y : N) :
    h.symm (x * y) = h.symm x * h.symm y :=
  map_mul (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv) x y

Inverse of Multiplicative Equivalence Preserves Multiplication

Informal description

Let $M$ and $N$ be types equipped with multiplication operations, and let $h: M \simeq^* N$ be a multiplicative equivalence between them. Then for any elements $x, y \in N$, the inverse equivalence $h^{-1}$ preserves multiplication, i.e., $h^{-1}(x \cdot y) = h^{-1}(x) \cdot h^{-1}(y)$.

MulEquiv.symm definition

{M N : Type*} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M

Full source

/-- The inverse of an isomorphism is an isomorphism. -/
@[to_additive (attr := symm) "The inverse of an isomorphism is an isomorphism."]
def symm {M N : Type*} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
  ⟨h.toEquiv.symm, h.symm_map_mul⟩

Inverse of a multiplicative isomorphism

Informal description

Given a multiplicative isomorphism $h : M \simeq^* N$ between two types $M$ and $N$ equipped with multiplication operations, the inverse $h^{-1} : N \simeq^* M$ is also a multiplicative isomorphism, preserving the multiplication structure.

MulEquiv.invFun_eq_symm theorem

{f : M ≃* N} : f.invFun = f.symm

Full source

@[to_additive]
theorem invFun_eq_symm {f : M ≃* N} : f.invFun = f.symm := rfl

Inverse Function Equals Symmetric Isomorphism in Multiplicative Equivalence

Informal description

For any multiplicative isomorphism $f : M \simeq^* N$, the inverse function $f^{-1}$ is equal to the symmetric multiplicative isomorphism $f^{-1} : N \simeq^* M$.

MulEquiv.coe_toEquiv_symm theorem

(f : M ≃* N) : ((f : M ≃ N).symm : N → M) = f.symm

Full source

/-- `simp`-normal form of `invFun_eq_symm`. -/
@[to_additive (attr := simp)]
theorem coe_toEquiv_symm (f : M ≃* N) : ((f : M ≃ N).symm : N → M) = f.symm := rfl

Inverse of Multiplicative Equivalence as Underlying Equivalence's Inverse

Informal description

For any multiplicative equivalence $f : M \simeq^* N$ between types $M$ and $N$ with multiplication operations, the underlying equivalence's inverse function (as a map from $N$ to $M$) is equal to the inverse multiplicative equivalence $f^{-1} : N \simeq^* M$.

MulEquiv.equivLike_inv_eq_symm theorem

(f : M ≃* N) : EquivLike.inv f = f.symm

Full source

@[to_additive (attr := simp)]
theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl

Equality of EquivLike Inverse and Multiplicative Symmetry

Informal description

For any multiplicative isomorphism $f : M \simeq^* N$ between types $M$ and $N$ with multiplication operations, the inverse function defined by the `EquivLike` structure coincides with the multiplicative inverse $f^{-1} = f^{\text{symm}}$.

MulEquiv.toEquiv_symm theorem

(f : M ≃* N) : (f.symm : N ≃ M) = (f : M ≃ N).symm

Full source

@[to_additive (attr := simp)]
theorem toEquiv_symm (f : M ≃* N) : (f.symm : N ≃ M) = (f : M ≃ N).symm := rfl

Inverse of Multiplicative Isomorphism as Equivalence Inverse

Informal description

For any multiplicative isomorphism $f : M \simeq^* N$ between two types $M$ and $N$ equipped with multiplication operations, the underlying equivalence of the inverse isomorphism $f^{-1} : N \simeq^* M$ is equal to the inverse of the underlying equivalence of $f$.

MulEquiv.symm_symm theorem

(f : M ≃* N) : f.symm.symm = f

Full source

@[to_additive (attr := simp)]
theorem symm_symm (f : M ≃* N) : f.symm.symm = f := rfl

Double Inverse of Multiplicative Isomorphism

Informal description

For any multiplicative isomorphism $f : M \simeq^* N$ between two types $M$ and $N$ with multiplication operations, the double inverse $f^{-1^{-1}}$ equals $f$ itself, i.e., $(f^{-1})^{-1} = f$.

MulEquiv.symm_bijective theorem

: Function.Bijective (symm : (M ≃* N) → N ≃* M)

Full source

@[to_additive]
theorem symm_bijective : Function.Bijective (symm : (M ≃* N) → N ≃* M) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Multiplicative Isomorphisms

Informal description

The function that maps a multiplicative isomorphism $f : M \simeq^* N$ to its inverse $f^{-1} : N \simeq^* M$ is bijective.

MulEquiv.mk_coe' theorem

(e : M ≃* N) (f h₁ h₂ h₃) : (MulEquiv.mk ⟨f, e, h₁, h₂⟩ h₃ : N ≃* M) = e.symm

Full source

@[to_additive (attr := simp)]
theorem mk_coe' (e : M ≃* N) (f h₁ h₂ h₃) : (MulEquiv.mk ⟨f, e, h₁, h₂⟩ h₃ : N ≃* M) = e.symm :=
  symm_bijective.injective <| ext fun _ => rfl

Constructed Multiplicative Equivalence Equals Inverse

Informal description

Let $M$ and $N$ be types equipped with multiplication operations, and let $e : M \simeq^* N$ be a multiplicative isomorphism. For any bijection $f : M \to N$ and proofs $h₁, h₂, h₃$ establishing $f$ as a multiplicative isomorphism, the constructed multiplicative equivalence $\text{MulEquiv.mk}\, \langle f, e, h₁, h₂\rangle\, h₃$ from $N$ to $M$ is equal to the inverse $e^{-1} : N \simeq^* M$ of $e$.

MulEquiv.symm_mk theorem

(f : M ≃ N) (h) : (MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm_map_mul⟩

Full source

@[to_additive (attr := simp)]
theorem symm_mk (f : M ≃ N) (h) :
    (MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm_map_mul⟩ := rfl

Inverse of Constructed Multiplicative Equivalence

Informal description

Let $M$ and $N$ be types equipped with multiplication operations, and let $f : M \simeq N$ be a bijection between them. Given a proof $h$ that $f$ preserves multiplication, the inverse of the multiplicative equivalence $\text{MulEquiv.mk}\, f\, h$ is equal to the multiplicative equivalence constructed from the inverse bijection $f^{-1}$ and the proof that it preserves multiplication.

MulEquiv.refl_symm theorem

: (refl M).symm = refl M

Full source

@[to_additive (attr := simp)]
theorem refl_symm : (refl M).symm = refl M := rfl

Inverse of Multiplicative Identity Isomorphism is Itself

Informal description

For any type $M$ equipped with a multiplication operation, the inverse of the multiplicative identity isomorphism on $M$ is equal to itself, i.e., $(\text{refl}_M)^{-1} = \text{refl}_M$.

MulEquiv.apply_symm_apply theorem

(e : M ≃* N) (y : N) : e (e.symm y) = y

Full source

/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
@[to_additive (attr := simp) "`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`."]
theorem apply_symm_apply (e : M ≃* N) (y : N) : e (e.symm y) = y :=
  e.toEquiv.apply_symm_apply y

Multiplicative Isomorphism Recovery: $e(e^{-1}(y)) = y$

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between two types $M$ and $N$ equipped with multiplication operations, and for any element $y \in N$, applying $e$ to the inverse image $e^{-1}(y)$ recovers the original element $y$, i.e., $e(e^{-1}(y)) = y$.

MulEquiv.symm_apply_apply theorem

(e : M ≃* N) (x : M) : e.symm (e x) = x

Full source

/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
@[to_additive (attr := simp) "`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`."]
theorem symm_apply_apply (e : M ≃* N) (x : M) : e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply x

Inverse of Multiplicative Isomorphism Recovers Original Element

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between two multiplicative structures $M$ and $N$, and for any element $x \in M$, applying the inverse isomorphism $e^{-1}$ to the image $e(x)$ recovers the original element $x$, i.e., $e^{-1}(e(x)) = x$.

MulEquiv.symm_comp_self theorem

(e : M ≃* N) : e.symm ∘ e = id

Full source

@[to_additive (attr := simp)]
theorem symm_comp_self (e : M ≃* N) : e.symm ∘ e = id :=
  funext e.symm_apply_apply

Inverse Composition Yields Identity for Multiplicative Isomorphism

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between two types $M$ and $N$ equipped with multiplication operations, the composition of the inverse isomorphism $e^{-1}$ with $e$ is equal to the identity function on $M$, i.e., $e^{-1} \circ e = \text{id}_M$.

MulEquiv.self_comp_symm theorem

(e : M ≃* N) : e ∘ e.symm = id

Full source

@[to_additive (attr := simp)]
theorem self_comp_symm (e : M ≃* N) : e ∘ e.symm = id :=
  funext e.apply_symm_apply

Composition of Multiplicative Isomorphism with its Inverse Yields Identity

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between two multiplicative structures $M$ and $N$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity function on $N$, i.e., $e \circ e^{-1} = \text{id}_N$.

MulEquiv.apply_eq_iff_symm_apply theorem

(e : M ≃* N) {x : M} {y : N} : e x = y ↔ x = e.symm y

Full source

@[to_additive]
theorem apply_eq_iff_symm_apply (e : M ≃* N) {x : M} {y : N} : e x = y ↔ x = e.symm y :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

Multiplicative Isomorphism Application Equality: $e(x) = y \leftrightarrow x = e^{-1}(y)$

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between two types $M$ and $N$ equipped with multiplication operations, and for any elements $x \in M$ and $y \in N$, we have $e(x) = y$ if and only if $x = e^{-1}(y)$.

MulEquiv.symm_apply_eq theorem

(e : M ≃* N) {x y} : e.symm x = y ↔ x = e y

Full source

@[to_additive]
theorem symm_apply_eq (e : M ≃* N) {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

Inverse Characterization for Multiplicative Isomorphisms: $e^{-1}(x) = y \leftrightarrow x = e(y)$

Informal description

For any multiplicative isomorphism $e : M \simeq^* N$ between two multiplicative structures $M$ and $N$, and for any elements $x \in N$ and $y \in M$, the equality $e^{-1}(x) = y$ holds if and only if $x = e(y)$.

MulEquiv.comp_symm_eq theorem

{α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) : g ∘ e.symm = f ↔ g = f ∘ e

Full source

@[to_additive]
theorem comp_symm_eq {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
    g ∘ e.symmg ∘ e.symm = f ↔ g = f ∘ e :=
  e.toEquiv.comp_symm_eq f g

Composition Condition for Multiplicative Isomorphism Inverses

Informal description

Let $M$ and $N$ be types equipped with multiplication operations, and let $e : M \simeq^* N$ be a multiplicative isomorphism between them. For any type $\alpha$ and functions $f : N \to \alpha$, $g : M \to \alpha$, the composition $g \circ e^{-1}$ equals $f$ if and only if $g$ equals $f \circ e$.

MulEquiv.symm_comp_eq theorem

{α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) : e.symm ∘ g = f ↔ g = e ∘ f

Full source

@[to_additive]
theorem symm_comp_eq {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
    e.symm ∘ ge.symm ∘ g = f ↔ g = e ∘ f :=
  e.toEquiv.symm_comp_eq f g

Characterization of Composition with Inverse Multiplicative Isomorphism: $e^{-1} \circ g = f \leftrightarrow g = e \circ f$

Informal description

Let $M$ and $N$ be types equipped with multiplication operations, and let $e : M \simeq^* N$ be a multiplicative isomorphism. For any type $\alpha$ and functions $f : \alpha \to M$, $g : \alpha \to N$, the composition $e^{-1} \circ g$ equals $f$ if and only if $g$ equals $e \circ f$.

MulEquivClass.apply_coe_symm_apply theorem

 {α β} [Mul α] [Mul β] {F} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : β) : e ((e : α ≃* β).symm x) = x

Full source

@[to_additive (attr := simp)]
theorem _root_.MulEquivClass.apply_coe_symm_apply {α β} [Mul α] [Mul β] {F} [EquivLike F α β]
    [MulEquivClass F α β] (e : F) (x : β) :
    e ((e : α ≃* β).symm x) = x :=
  (e : α ≃* β).right_inv x

Multiplicative Equivalence Cancellation: $e(e^{-1}(x)) = x$

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication operations, and let $F$ be a type satisfying `MulEquivClass F α β`. For any multiplicative equivalence $e : F$ and any element $x \in \beta$, we have $e(e^{-1}(x)) = x$, where $e^{-1}$ denotes the inverse of the equivalence $e$.

MulEquivClass.coe_symm_apply_apply theorem

 {α β} [Mul α] [Mul β] {F} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : α) : (e : α ≃* β).symm (e x) = x

Full source

@[to_additive (attr := simp)]
theorem _root_.MulEquivClass.coe_symm_apply_apply {α β} [Mul α] [Mul β] {F} [EquivLike F α β]
    [MulEquivClass F α β] (e : F) (x : α) :
    (e : α ≃* β).symm (e x) = x :=
  (e : α ≃* β).left_inv x

Inverse Property of Multiplicative Equivalence: $e^{-1}(e(x)) = x$

Informal description

For any multiplicative equivalence $e$ between two types $\alpha$ and $\beta$ equipped with multiplication operations, and for any element $x \in \alpha$, the inverse of $e$ evaluated at $e(x)$ equals $x$, i.e., $e^{-1}(e(x)) = x$.

MulEquiv.Simps.symm_apply definition

(e : M ≃* N) : N → M

Full source

/-- See Note [custom simps projection] -/
@[to_additive "See Note [custom simps projection]"] -- this comment fixes the syntax highlighting "
def Simps.symm_apply (e : M ≃* N) : N → M :=
  e.symm

Inverse function of a multiplicative isomorphism

Informal description

Given a multiplicative isomorphism $e : M \simeq^* N$ between two types $M$ and $N$ equipped with multiplication operations, the function maps an element $y \in N$ to its preimage $x \in M$ under $e$, i.e., $x = e^{-1}(y)$ where $e^{-1}$ is the inverse isomorphism of $e$.

MulEquiv.trans definition

(h1 : M ≃* N) (h2 : N ≃* P) : M ≃* P

Full source

/-- Transitivity of multiplication-preserving isomorphisms -/
@[to_additive (attr := trans) "Transitivity of addition-preserving isomorphisms"]
def trans (h1 : M ≃* N) (h2 : N ≃* P) : M ≃* P :=
  { h1.toEquiv.trans h2.toEquiv with
    map_mul' := fun x y => show h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y) by
      rw [map_mul, map_mul] }

Composition of multiplicative isomorphisms

Informal description

Given two multiplicative isomorphisms $h_1: M \simeq^* N$ and $h_2: N \simeq^* P$, their composition $h_2 \circ h_1$ forms a multiplicative isomorphism $M \simeq^* P$, where the multiplication is preserved as $h_2(h_1(x \cdot y)) = h_2(h_1(x)) \cdot h_2(h_1(y))$ for all $x, y \in M$.

MulEquiv.coe_trans theorem

(e₁ : M ≃* N) (e₂ : N ≃* P) : ↑(e₁.trans e₂) = e₂ ∘ e₁

Full source

@[to_additive (attr := simp)]
theorem coe_trans (e₁ : M ≃* N) (e₂ : N ≃* P) : ↑(e₁.trans e₂) = e₂ ∘ e₁ := rfl

Composition of Multiplicative Isomorphisms Preserves Underlying Functions

Informal description

For any multiplicative isomorphisms $e₁: M \simeq^* N$ and $e₂: N \simeq^* P$, the underlying function of their composition $e₁.trans e₂$ is equal to the composition of the underlying functions $e₂ \circ e₁$.

MulEquiv.trans_apply theorem

(e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : e₁.trans e₂ m = e₂ (e₁ m)

Full source

@[to_additive (attr := simp)]
theorem trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : e₁.trans e₂ m = e₂ (e₁ m) := rfl

Application of Composition of Multiplicative Isomorphisms

Informal description

For any multiplicative isomorphisms $e_1: M \simeq^* N$ and $e_2: N \simeq^* P$, and any element $m \in M$, the application of the composed isomorphism $e_1 \circ e_2$ to $m$ equals the application of $e_2$ to the result of applying $e_1$ to $m$, i.e., $(e_1 \circ e_2)(m) = e_2(e_1(m))$.

MulEquiv.symm_trans_apply theorem

(e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) : (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)

Full source

@[to_additive (attr := simp)]
theorem symm_trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
    (e₁.trans e₂).symm p = e₁.symm (e₂.symm p) := rfl

Inverse of Composition of Multiplicative Isomorphisms

Informal description

Let $M$, $N$, and $P$ be types equipped with multiplication operations, and let $e_1: M \simeq^* N$ and $e_2: N \simeq^* P$ be multiplicative isomorphisms. For any element $p \in P$, the inverse of the composition $e_1 \circ e_2$ applied to $p$ equals the composition of the inverses $e_1^{-1} \circ e_2^{-1}$ applied to $p$, i.e., $$(e_1 \circ e_2)^{-1}(p) = e_1^{-1}(e_2^{-1}(p)).$$

MulEquiv.symm_trans_self theorem

(e : M ≃* N) : e.symm.trans e = refl N

Full source

@[to_additive (attr := simp)]
theorem symm_trans_self (e : M ≃* N) : e.symm.trans e = refl N :=
  DFunLike.ext _ _ e.apply_symm_apply

Inverse Composition Yields Identity: $e^{-1} \circ e = \text{id}_N$

Informal description

For any multiplicative isomorphism $e \colon M \simeq^* N$ between types $M$ and $N$ equipped with multiplication operations, the composition of the inverse isomorphism $e^{-1}$ with $e$ is equal to the identity isomorphism on $N$, i.e., $e^{-1} \circ e = \text{id}_N$.

MulEquiv.self_trans_symm theorem

(e : M ≃* N) : e.trans e.symm = refl M

Full source

@[to_additive (attr := simp)]
theorem self_trans_symm (e : M ≃* N) : e.trans e.symm = refl M :=
  DFunLike.ext _ _ e.symm_apply_apply

Composition of Isomorphism with Its Inverse Yields Identity

Informal description

For any multiplicative isomorphism $e \colon M \simeq^* N$ between two multiplicative structures $M$ and $N$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity isomorphism on $M$, i.e., $e \circ e^{-1} = \text{id}_M$.

MulEquiv.coe_monoidHom_refl theorem

: (refl M : M →* M) = MonoidHom.id M

Full source

@[to_additive (attr := simp)]
theorem coe_monoidHom_refl : (refl M : M →* M) = MonoidHom.id M := rfl

Identity Multiplicative Isomorphism Yields Identity Monoid Homomorphism

Informal description

The monoid homomorphism associated with the multiplicative identity isomorphism $\text{refl}_M \colon M \simeq^* M$ is equal to the identity monoid homomorphism $\text{id}_M \colon M \to^* M$.

MulEquiv.coe_monoidHom_trans theorem

(e₁ : M ≃* N) (e₂ : N ≃* P) : (e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁

Full source

@[to_additive (attr := simp)]
lemma coe_monoidHom_trans (e₁ : M ≃* N) (e₂ : N ≃* P) :
    (e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁ := rfl

Composition of Multiplicative Isomorphisms as Monoid Homomorphisms

Informal description

For any multiplicative isomorphisms $e_1 \colon M \simeq^* N$ and $e_2 \colon N \simeq^* P$, the monoid homomorphism corresponding to the composition $e_1 \circ e_2$ is equal to the composition of the monoid homomorphisms corresponding to $e_2$ and $e_1$. In other words, $(e_1 \circ e_2)^* = e_2^* \circ e_1^*$, where $e^*$ denotes the monoid homomorphism associated with the multiplicative isomorphism $e$.

MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm theorem

(e : M ≃* N) : (e : M →* N).comp e.symm = MonoidHom.id _

Full source

@[to_additive (attr := simp)]
lemma coe_monoidHom_comp_coe_monoidHom_symm (e : M ≃* N) :
    (e : M →* N).comp e.symm = MonoidHom.id _ := by ext; simp

Composition of Multiplicative Isomorphism with Its Inverse Yields Identity Homomorphism

Informal description

For any multiplicative isomorphism $e \colon M \simeq^* N$ between monoids $M$ and $N$, the composition of the associated monoid homomorphism $e \colon M \to^* N$ with its inverse $e^{-1} \colon N \to^* M$ is equal to the identity monoid homomorphism on $N$, i.e., $e \circ e^{-1} = \text{id}_N$.

MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom theorem

(e : M ≃* N) : (e.symm : N →* M).comp e = MonoidHom.id _

Full source

@[to_additive (attr := simp)]
lemma coe_monoidHom_symm_comp_coe_monoidHom (e : M ≃* N) :
    (e.symm : N →* M).comp e = MonoidHom.id _ := by ext; simp

Inverse-Post-Composition Yields Identity Monoid Homomorphism

Informal description

For any multiplicative isomorphism $e \colon M \simeq^* N$ between monoids $M$ and $N$, the composition of the monoid homomorphism associated with the inverse isomorphism $e^{-1} \colon N \to^* M$ and the monoid homomorphism associated with $e \colon M \to^* N$ is equal to the identity monoid homomorphism on $M$. That is, $e^{-1} \circ e = \text{id}_M$.

MulEquiv.comp_left_injective theorem

(e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N)

Full source

@[to_additive]
lemma comp_left_injective (e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N) :=
  LeftInverse.injective (g := fun f ↦ f.comp e.symm) fun f ↦ by simp [MonoidHom.comp_assoc]

Injectivity of Post-Composition with Multiplicative Isomorphism

Informal description

Let $M$, $N$, and $P$ be monoids, and let $e \colon M \simeq^* N$ be a multiplicative isomorphism. Then the function that post-composes monoid homomorphisms $f \colon N \to^* P$ with $e$ is injective. In other words, if $f_1 \circ e = f_2 \circ e$ for $f_1, f_2 \colon N \to^* P$, then $f_1 = f_2$.

MulEquiv.comp_right_injective theorem

(e : M ≃* N) : Injective fun f : P →* M ↦ (e : M →* N).comp f

Full source

@[to_additive]
lemma comp_right_injective (e : M ≃* N) : Injective fun f : P →* M ↦ (e : M →* N).comp f :=
  LeftInverse.injective (g := (e.symm : N →* M).comp) fun f ↦ by simp [← MonoidHom.comp_assoc]

Injectivity of Pre-Composition with Multiplicative Isomorphism

Informal description

For any multiplicative isomorphism $e \colon M \simeq^* N$ between monoids $M$ and $N$, the function that maps a monoid homomorphism $f \colon P \to^* M$ to the composition $e \circ f \colon P \to^* N$ is injective.

MulEquiv.map_one theorem

(h : M ≃* N) : h 1 = 1

Full source

/-- A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism). -/
@[to_additive
  "An additive isomorphism of additive monoids sends `0` to `0`
  (and is hence an additive monoid isomorphism)."]
protected theorem map_one (h : M ≃* N) : h 1 = 1 := map_one h

Multiplicative Isomorphism Preserves Identity Element

Informal description

For any multiplicative isomorphism $h : M \simeq^* N$ between monoids $M$ and $N$, the image of the identity element $1 \in M$ under $h$ is the identity element $1 \in N$, i.e., $h(1) = 1$.

MulEquiv.map_eq_one_iff theorem

(h : M ≃* N) {x : M} : h x = 1 ↔ x = 1

Full source

@[to_additive]
protected theorem map_eq_one_iff (h : M ≃* N) {x : M} : h x = 1 ↔ x = 1 :=
  EmbeddingLike.map_eq_one_iff

Multiplicative Isomorphism Preserves Identity: $h(x) = 1 \leftrightarrow x = 1$

Informal description

For any multiplicative isomorphism $h \colon M \simeq^* N$ between monoids $M$ and $N$, and for any element $x \in M$, we have $h(x) = 1$ if and only if $x = 1$.

MulEquiv.map_ne_one_iff theorem

(h : M ≃* N) {x : M} : h x ≠ 1 ↔ x ≠ 1

Full source

@[to_additive]
theorem map_ne_one_iff (h : M ≃* N) {x : M} : h x ≠ 1h x ≠ 1 ↔ x ≠ 1 :=
  EmbeddingLike.map_ne_one_iff

Non-Identity Preservation under Multiplicative Isomorphism: $h(x) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any multiplicative isomorphism $h \colon M \simeq^* N$ between monoids $M$ and $N$, and for any element $x \in M$, we have $h(x) \neq 1$ if and only if $x \neq 1$.

MulEquiv.ofBijective definition

{M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Bijective f) : M ≃* N

Full source

/-- A bijective `Semigroup` homomorphism is an isomorphism -/
@[to_additive (attr := simps! apply) "A bijective `AddSemigroup` homomorphism is an isomorphism"]
noncomputable def ofBijective {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N]
    (f : F) (hf : Bijective f) : M ≃* N :=
  { Equiv.ofBijective f hf with map_mul' := map_mul f }

Multiplicative isomorphism from a bijective homomorphism

Informal description

Given a bijective multiplicative homomorphism $ f \colon M \to N $ between multiplicative structures $ M $ and $ N $, the function constructs a multiplicative equivalence (isomorphism) $ M \simeq^* N $. This equivalence preserves the multiplication operation, i.e., for any $ x, y \in M $, $ f(x \cdot y) = f(x) \cdot f(y) $.

MulEquiv.ofBijective_apply_symm_apply theorem

{n : N} (f : M →* N) (hf : Bijective f) : f ((ofBijective f hf).symm n) = n

Full source

@[to_additive (attr := simp)]
theorem ofBijective_apply_symm_apply {n : N} (f : M →* N) (hf : Bijective f) :
    f ((ofBijective f hf).symm n) = n := (ofBijective f hf).apply_symm_apply n

Recovery of Element via Bijective Monoid Homomorphism: $f(f^{-1}(n)) = n$

Informal description

Let $f \colon M \to N$ be a bijective monoid homomorphism between monoids $M$ and $N$. For any element $n \in N$, applying $f$ to the inverse image of $n$ under the multiplicative isomorphism $\text{ofBijective}(f, hf)$ recovers $n$, i.e., $f((\text{ofBijective}(f, hf))^{-1}(n)) = n$.

MulEquiv.toMonoidHom definition

(h : M ≃* N) : M →* N

Full source

/-- Extract the forward direction of a multiplicative equivalence
as a multiplication-preserving function.
-/
@[to_additive "Extract the forward direction of an additive equivalence
  as an addition-preserving function."]
def toMonoidHom (h : M ≃* N) : M →* N :=
  { h with map_one' := h.map_one }

Conversion of multiplicative equivalence to monoid homomorphism

Informal description

Given a multiplicative equivalence (isomorphism) $h \colon M \simeq^* N$ between monoids $M$ and $N$, the function `MulEquiv.toMonoidHom` converts $h$ into a monoid homomorphism $M \to^* N$ that preserves the multiplicative structure and the identity element. Specifically, for any $x, y \in M$, the homomorphism satisfies $h(x \cdot y) = h(x) \cdot h(y)$, and $h(1) = 1$.

MulEquiv.coe_toMonoidHom theorem

(e : M ≃* N) : ⇑e.toMonoidHom = e

Full source

@[to_additive (attr := simp)]
theorem coe_toMonoidHom (e : M ≃* N) : ⇑e.toMonoidHom = e := rfl

Coercion of Multiplicative Equivalence to Monoid Homomorphism Preserves Underlying Function

Informal description

For any multiplicative equivalence $e \colon M \simeq^* N$ between monoids $M$ and $N$, the underlying function of the monoid homomorphism obtained from $e$ via `MulEquiv.toMonoidHom` is equal to $e$ itself. In other words, the coercion of the monoid homomorphism representation of $e$ coincides with $e$ as a function.

MulEquiv.toMonoidHom_eq_coe theorem

(f : M ≃* N) : f.toMonoidHom = (f : M →* N)

Full source

@[to_additive (attr := simp)]
theorem toMonoidHom_eq_coe (f : M ≃* N) : f.toMonoidHom = (f : M →* N) :=
  rfl

Equality of Monoid Homomorphism Conversion and Coercion for Multiplicative Equivalence

Informal description

For any multiplicative equivalence $f \colon M \simeq^* N$ between monoids $M$ and $N$, the monoid homomorphism obtained by applying `toMonoidHom` to $f$ is equal to the coercion of $f$ to a monoid homomorphism.

MulEquiv.toMonoidHom_injective theorem

: Injective (toMonoidHom : M ≃* N → M →* N)

Full source

@[to_additive]
theorem toMonoidHom_injective : Injective (toMonoidHom : M ≃* N → M →* N) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Conversion from Multiplicative Equivalence to Monoid Homomorphism

Informal description

The function that converts a multiplicative equivalence (isomorphism) $h \colon M \simeq^* N$ between monoids $M$ and $N$ into a monoid homomorphism $M \to^* N$ is injective. That is, if two multiplicative equivalences $h_1, h_2 \colon M \simeq^* N$ satisfy $h_1.toMonoidHom = h_2.toMonoidHom$, then $h_1 = h_2$.

MulEquiv.map_inv theorem

[Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹

Full source

/-- A multiplicative equivalence of groups preserves inversion. -/
@[to_additive "An additive equivalence of additive groups preserves negation."]
protected theorem map_inv [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) :
    h x⁻¹ = (h x)⁻¹ :=
  map_inv h x

Multiplicative equivalence preserves inverses: $h(x^{-1}) = (h(x))^{-1}$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any multiplicative equivalence (group isomorphism) $h \colon G \simeq^* H$ and any element $x \in G$, the image of the inverse $h(x^{-1})$ is equal to the inverse of the image $(h(x))^{-1}$ in $H$.

MulEquiv.map_div theorem

[Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G) : h (x / y) = h x / h y

Full source

/-- A multiplicative equivalence of groups preserves division. -/
@[to_additive "An additive equivalence of additive groups preserves subtractions."]
protected theorem map_div [Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G) :
    h (x / y) = h x / h y :=
  map_div h x y

Multiplicative Equivalence Preserves Division: $h(x / y) = h(x) / h(y)$

Informal description

Let $G$ be a group and $H$ a division monoid. For any multiplicative equivalence (group isomorphism) $h \colon G \simeq^* H$ and any elements $x, y \in G$, the equivalence $h$ preserves division, i.e., $h(x / y) = h(x) / h(y)$.

MulHom.toMulEquiv definition

 [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.id _) : M ≃* N

Full source

/-- Given a pair of multiplicative homomorphisms `f`, `g` such that `g.comp f = id` and
`f.comp g = id`, returns a multiplicative equivalence with `toFun = f` and `invFun = g`. This
constructor is useful if the underlying type(s) have specialized `ext` lemmas for multiplicative
homomorphisms. -/
@[to_additive (attr := simps -fullyApplied)
  "Given a pair of additive homomorphisms `f`, `g` such that `g.comp f = id` and
  `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`. This
  constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
  homomorphisms."]
def MulHom.toMulEquiv [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id _)
    (h₂ : f.comp g = MulHom.id _) : M ≃* N where
  toFun := f
  invFun := g
  left_inv := DFunLike.congr_fun h₁
  right_inv := DFunLike.congr_fun h₂
  map_mul' := f.map_mul

Multiplicative equivalence from homomorphisms with inverse conditions

Informal description

Given multiplicative structures $M$ and $N$, and non-unital multiplicative homomorphisms $f \colon M \to N$ and $g \colon N \to M$ such that $g \circ f$ is the identity homomorphism on $M$ and $f \circ g$ is the identity homomorphism on $N$, this constructs a multiplicative equivalence (isomorphism) between $M$ and $N$ with $f$ as the forward map and $g$ as the inverse map. The equivalence preserves the multiplicative structure, meaning $f(x * y) = f(x) * f(y)$ for all $x, y \in M$.

MonoidHom.toMulEquiv definition

 [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id _)
  (h₂ : f.comp g = MonoidHom.id _) : M ≃* N

Full source

/-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
returns a multiplicative equivalence with `toFun = f` and `invFun = g`.  This constructor is
useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
@[to_additive (attr := simps -fullyApplied)
  "Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id`
  and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`.  This
  constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
  monoid homomorphisms."]
def MonoidHom.toMulEquiv [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M)
    (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) : M ≃* N where
  toFun := f
  invFun := g
  left_inv := DFunLike.congr_fun h₁
  right_inv := DFunLike.congr_fun h₂
  map_mul' := f.map_mul

Monoid Homomorphism to Multiplicative Equivalence

Informal description

Given monoids $ M $ and $ N $, and monoid homomorphisms $ f \colon M \to N $ and $ g \colon N \to M $ such that $ g \circ f $ is the identity homomorphism on $ M $ and $ f \circ g $ is the identity homomorphism on $ N $, this constructs a multiplicative equivalence (isomorphism) between $ M $ and $ N $ with $ f $ as the forward map and $ g $ as the inverse map. The equivalence preserves the multiplicative structure.

Mathlib.Algebra.Group.Equiv.Defs

Main definitions

Notations

Tags