Mathlib.Algebra.Group.Hom.Basic

powMonoidHom definition

(n : ℕ) : α →* α

Full source

/-- The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of
monoids. -/
@[to_additive (attr := simps) "Multiplication by a natural `n` on a commutative additive monoid,
considered as a morphism of additive monoids."]
def powMonoidHom (n : ℕ) : α →* α where
  toFun := (· ^ n)
  map_one' := one_pow _
  map_mul' a b := mul_pow a b n

$n$-th power monoid homomorphism

Informal description

For a commutative monoid $\alpha$ and a natural number $n$, the $n$-th power map $x \mapsto x^n$ is a monoid homomorphism from $\alpha$ to itself. It maps the identity element to itself ($1^n = 1$) and preserves multiplication ($(ab)^n = a^n b^n$ for all $a, b \in \alpha$).

zpowGroupHom definition

(n : ℤ) : α →* α

Full source

/-- The `n`-th power map (for an integer `n`) on a commutative group, considered as a group
homomorphism. -/
@[to_additive (attr := simps) "Multiplication by an integer `n` on a commutative additive group,
considered as an additive group homomorphism."]
def zpowGroupHom (n : ℤ) : α →* α where
  toFun := (· ^ n)
  map_one' := one_zpow n
  map_mul' a b := mul_zpow a b n

$n$-th power group homomorphism

Informal description

For a commutative group $\alpha$ and an integer $n$, the $n$-th power map $x \mapsto x^n$ is a group homomorphism from $\alpha$ to itself. It maps the identity element to itself ($1^n = 1$) and preserves multiplication ($(ab)^n = a^n b^n$ for all $a, b \in \alpha$).

invMonoidHom definition

: α →* α

Full source

/-- Inversion on a commutative group, considered as a monoid homomorphism. -/
@[to_additive "Negation on a commutative additive group, considered as an additive monoid
homomorphism."]
def invMonoidHom : α →* α where
  toFun := Inv.inv
  map_one' := inv_one
  map_mul' := mul_inv

Inversion as a monoid homomorphism

Informal description

The inversion operation on a commutative group, considered as a monoid homomorphism from the group to itself. It maps each element $a$ to its inverse $a^{-1}$, preserves the identity element ($1^{-1} = 1$), and satisfies the homomorphism property $(ab)^{-1} = a^{-1}b^{-1}$ for all $a, b$ in the group.

coe_invMonoidHom theorem

: (invMonoidHom : α → α) = Inv.inv

Full source

@[simp]
theorem coe_invMonoidHom : (invMonoidHom : α → α) = Inv.inv := rfl

Inversion Homomorphism Equals Inversion Operation

Informal description

The underlying function of the inversion monoid homomorphism `invMonoidHom` is equal to the inversion operation `Inv.inv` on the group $\alpha$. That is, for any element $a \in \alpha$, we have $\text{invMonoidHom}(a) = a^{-1}$.

invMonoidHom_apply theorem

(a : α) : invMonoidHom a = a⁻¹

Full source

@[simp]
theorem invMonoidHom_apply (a : α) : invMonoidHom a = a⁻¹ := rfl

Inversion Homomorphism Evaluation: $\text{invMonoidHom}(a) = a^{-1}$

Informal description

For any element $a$ in a commutative group $\alpha$, the inversion monoid homomorphism evaluated at $a$ equals the inverse of $a$, i.e., $\text{invMonoidHom}(a) = a^{-1}$.

MulHom.instMul instance

[Mul M] [CommSemigroup N] : Mul (M →ₙ* N)

Full source

/-- Given two mul morphisms `f`, `g` to a commutative semigroup, `f * g` is the mul morphism
sending `x` to `f x * g x`. -/
@[to_additive "Given two additive morphisms `f`, `g` to an additive commutative semigroup,
`f + g` is the additive morphism sending `x` to `f x + g x`."]
instance [Mul M] [CommSemigroup N] : Mul (M →ₙ* N) :=
  ⟨fun f g =>
    { toFun := fun m => f m * g m,
      map_mul' := fun x y => by
        show f (x * y) * g (x * y) = f x * g x * (f y * g y)
        rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)] }⟩

Pointwise Multiplication of Multiplicative Homomorphisms into a Commutative Semigroup

Informal description

For any type $M$ with a multiplication operation and any commutative semigroup $N$, the set of multiplicative homomorphisms from $M$ to $N$ forms a multiplicative structure where the product of two homomorphisms $f$ and $g$ is defined pointwise by $(f \cdot g)(x) = f(x) \cdot g(x)$ for all $x \in M$.

MulHom.mul_apply theorem

{M N} [Mul M] [CommSemigroup N] (f g : M →ₙ* N) (x : M) : (f * g) x = f x * g x

Full source

@[to_additive (attr := simp)]
theorem mul_apply {M N} [Mul M] [CommSemigroup N] (f g : M →ₙ* N) (x : M) :
    (f * g) x = f x * g x := rfl

Pointwise Product Evaluation of Multiplicative Homomorphisms

Informal description

Let $M$ be a type with a multiplication operation and $N$ be a commutative semigroup. For any multiplicative homomorphisms $f, g \colon M \to N$ and any element $x \in M$, the evaluation of the pointwise product $f \cdot g$ at $x$ equals the product of the evaluations $f(x) \cdot g(x)$, i.e., $(f \cdot g)(x) = f(x) \cdot g(x)$.

MulHom.mul_comp theorem

 [Mul M] [Mul N] [CommSemigroup P] (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Full source

@[to_additive]
theorem mul_comp [Mul M] [Mul N] [CommSemigroup P] (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N) :
    (g₁ * g₂).comp f = g₁.comp f * g₂.comp f := rfl

Composition of Multiplicative Homomorphisms Distributes Over Pointwise Product

Informal description

Let $M$, $N$, and $P$ be types equipped with multiplication operations, where $P$ is a commutative semigroup. For any multiplicative homomorphisms $g₁, g₂ : N →ₙ* P$ and $f : M →ₙ* N$, the composition of the pointwise product $g₁ \cdot g₂$ with $f$ is equal to the pointwise product of the compositions $g₁ \circ f$ and $g₂ \circ f$. In other words, $(g₁ \cdot g₂) \circ f = (g₁ \circ f) \cdot (g₂ \circ f)$.

MulHom.comp_mul theorem

 [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Full source

@[to_additive]
theorem comp_mul [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
  ext
  simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]

Composition Distributes Over Pointwise Product of Multiplicative Homomorphisms

Informal description

Let $M$, $N$, and $P$ be types equipped with multiplication operations, where $N$ and $P$ are commutative semigroups. For any multiplicative homomorphism $g \colon N \to P$ and any multiplicative homomorphisms $f₁, f₂ \colon M \to N$, the composition of $g$ with the pointwise product $f₁ \cdot f₂$ is equal to the pointwise product of the compositions $g \circ f₁$ and $g \circ f₂$. In other words, $g \circ (f₁ \cdot f₂) = (g \circ f₁) \cdot (g \circ f₂)$.

injective_iff_map_eq_one theorem

 {G H} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
  Function.Injective f ↔ ∀ a, f a = 1 → a = 1

Full source

/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial.
For the iff statement on the triviality of the kernel, see `injective_iff_map_eq_one'`. -/
@[to_additive
  "A homomorphism from an additive group to an additive monoid is injective iff
  its kernel is trivial. For the iff statement on the triviality of the kernel,
  see `injective_iff_map_eq_zero'`."]
theorem _root_.injective_iff_map_eq_one {G H} [Group G] [MulOneClass H]
    [FunLike F G H] [MonoidHomClass F G H]
    (f : F) : Function.InjectiveFunction.Injective f ↔ ∀ a, f a = 1 → a = 1 :=
  ⟨fun h _ => (map_eq_one_iff f h).mp, fun h x y hxy =>
    mul_inv_eq_one.1 <| h _ <| by rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]⟩

Injective Group Homomorphism Characterization via Kernel Triviality

Informal description

Let $G$ be a group and $H$ be a monoid. For any monoid homomorphism $f \colon G \to H$, the following are equivalent: 1. $f$ is injective. 2. For every $a \in G$, if $f(a) = 1$ then $a = 1$. In other words, a group homomorphism to a monoid is injective if and only if its kernel is trivial.

injective_iff_map_eq_one' theorem

 {G H} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
  Function.Injective f ↔ ∀ a, f a = 1 ↔ a = 1

Full source

/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial,
stated as an iff on the triviality of the kernel.
For the implication, see `injective_iff_map_eq_one`. -/
@[to_additive
  "A homomorphism from an additive group to an additive monoid is injective iff its
  kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see
  `injective_iff_map_eq_zero`."]
theorem _root_.injective_iff_map_eq_one' {G H} [Group G] [MulOneClass H]
    [FunLike F G H] [MonoidHomClass F G H]
    (f : F) : Function.InjectiveFunction.Injective f ↔ ∀ a, f a = 1 ↔ a = 1 :=
  (injective_iff_map_eq_one f).trans <|
    forall_congr' fun _ => ⟨fun h => ⟨h, fun H => H.symm ▸ map_one f⟩, Iff.mp⟩

Injective Group Homomorphism Characterization via Kernel Triviality (Bidirectional Form)

Informal description

Let $G$ be a group and $H$ be a monoid. For any monoid homomorphism $f \colon G \to H$, the following are equivalent: 1. $f$ is injective. 2. For every $a \in G$, $f(a) = 1$ if and only if $a = 1$. In other words, a group homomorphism to a monoid is injective if and only if its kernel is trivial (i.e., contains only the identity element).

MonoidHom.ofMapMulInv definition

{H : Type*} [Group H] (f : G → H) (map_div : ∀ a b : G, f (a * b⁻¹) = f a * (f b)⁻¹) : G →* H

Full source

/-- Makes a group homomorphism from a proof that the map preserves right division
`fun x y => x * y⁻¹`. See also `MonoidHom.of_map_div` for a version using `fun x y => x / y`.
-/
@[to_additive
  "Makes an additive group homomorphism from a proof that the map preserves
  the operation `fun a b => a + -b`. See also `AddMonoidHom.ofMapSub` for a version using
  `fun a b => a - b`."]
def ofMapMulInv {H : Type*} [Group H] (f : G → H)
    (map_div : ∀ a b : G, f (a * b⁻¹) = f a * (f b)⁻¹) : G →* H :=
  (mk' f) fun x y =>
    calc
      f (x * y) = f x * (f <| 1 * 1⁻¹ * y⁻¹)⁻¹ := by
        { simp only [one_mul, inv_one, ← map_div, inv_inv] }
      _ = f x * f y := by
        { simp only [map_div]
          simp only [mul_inv_cancel, one_mul, inv_inv] }

Monoid homomorphism from a right division-preserving map

Informal description

Given a group $H$ and a function $f \colon G \to H$ that preserves the operation $x * y^{-1}$ (i.e., $f(a * b^{-1}) = f(a) * f(b)^{-1}$ for all $a, b \in G$), this constructs a monoid homomorphism from $G$ to $H$.

MonoidHom.coe_of_map_mul_inv theorem

 {H : Type*} [Group H] (f : G → H) (map_div : ∀ a b : G, f (a * b⁻¹) = f a * (f b)⁻¹) : ↑(ofMapMulInv f map_div) = f

Full source

@[to_additive (attr := simp)]
theorem coe_of_map_mul_inv {H : Type*} [Group H] (f : G → H)
    (map_div : ∀ a b : G, f (a * b⁻¹) = f a * (f b)⁻¹) :
  ↑(ofMapMulInv f map_div) = f := rfl

Equality of Monoid Homomorphism Construction from Right Division-Preserving Map

Informal description

Let $G$ and $H$ be groups, and let $f \colon G \to H$ be a function satisfying $f(a * b^{-1}) = f(a) * f(b)^{-1}$ for all $a, b \in G$. Then the underlying function of the monoid homomorphism constructed from $f$ via `ofMapMulInv` is equal to $f$ itself, i.e., $\text{ofMapMulInv}(f) = f$.

MonoidHom.ofMapDiv definition

{H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) : G →* H

Full source

/-- Define a morphism of additive groups given a map which respects ratios. -/
@[to_additive "Define a morphism of additive groups given a map which respects difference."]
def ofMapDiv {H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) : G →* H :=
  ofMapMulInv f (by simpa only [div_eq_mul_inv] using hf)

Monoid homomorphism from a division-preserving map

Informal description

Given a group $H$ and a function $f \colon G \to H$ that preserves division (i.e., $f(x / y) = f(x) / f(y)$ for all $x, y \in G$), this constructs a monoid homomorphism from $G$ to $H$.

MonoidHom.coe_of_map_div theorem

{H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) : ↑(ofMapDiv f hf) = f

Full source

@[to_additive (attr := simp)]
theorem coe_of_map_div {H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) :
    ↑(ofMapDiv f hf) = f := rfl

Equality of Monoid Homomorphism Construction from Division-Preserving Map

Informal description

Let $G$ and $H$ be groups, and let $f \colon G \to H$ be a function satisfying $f(x / y) = f(x) / f(y)$ for all $x, y \in G$. Then the underlying function of the monoid homomorphism constructed from $f$ via `ofMapDiv` is equal to $f$ itself, i.e., $\text{ofMapDiv}(f) = f$.

MonoidHom.mul instance

: Mul (M →* N)

Full source

/-- Given two monoid morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid morphism
sending `x` to `f x * g x`. -/
@[to_additive]
instance mul : Mul (M →* N) :=
  ⟨fun f g =>
    { toFun := fun m => f m * g m,
      map_one' := show f 1 * g 1 = 1 by simp,
      map_mul' := fun x y => by
        show f (x * y) * g (x * y) = f x * g x * (f y * g y)
        rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)] }⟩

Pointwise Multiplication of Monoid Homomorphisms to a Commutative Monoid

Informal description

For any commutative monoid $N$, the set of monoid homomorphisms from a monoid $M$ to $N$ forms a monoid under pointwise multiplication. That is, given two monoid homomorphisms $f, g: M \to N$, their product $f \cdot g$ is the homomorphism defined by $(f \cdot g)(x) = f(x) \cdot g(x)$ for all $x \in M$.

MonoidHom.mul_apply theorem

(f g : M →* N) (x : M) : (f * g) x = f x * g x

Full source

@[to_additive (attr := simp)] lemma mul_apply (f g : M →* N) (x : M) : (f * g) x = f x * g x := rfl

Pointwise Product Evaluation of Monoid Homomorphisms

Informal description

For any monoid homomorphisms $f, g \colon M \to N$ and any element $x \in M$, the evaluation of their pointwise product at $x$ equals the product of their evaluations, i.e., $(f \cdot g)(x) = f(x) \cdot g(x)$.

MonoidHom.mul_comp theorem

[MulOneClass P] (g₁ g₂ : M →* N) (f : P →* M) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Full source

@[to_additive]
lemma mul_comp [MulOneClass P] (g₁ g₂ : M →* N) (f : P →* M) :
    (g₁ * g₂).comp f = g₁.comp f * g₂.comp f := rfl

Composition of Product Homomorphisms Equals Product of Compositions

Informal description

Let $P$, $M$, and $N$ be monoids (with $P$ having a `MulOneClass` structure). For any monoid homomorphisms $g₁, g₂ \colon M \to N$ and $f \colon P \to M$, the composition of the product homomorphism $(g₁ \cdot g₂)$ with $f$ is equal to the product of the compositions $g₁ \circ f$ and $g₂ \circ f$. That is, $(g₁ \cdot g₂) \circ f = (g₁ \circ f) \cdot (g₂ \circ f)$.

MonoidHom.comp_mul theorem

[CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Full source

@[to_additive]
lemma comp_mul [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
  ext; simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]

Composition Distributes Over Product of Monoid Homomorphisms

Informal description

Let $M$, $N$, and $P$ be monoids with $P$ commutative. For any monoid homomorphism $g \colon N \to P$ and any monoid homomorphisms $f₁, f₂ \colon M \to N$, the composition of $g$ with the product homomorphism $f₁ \cdot f₂$ equals the product of the compositions $g \circ f₁$ and $g \circ f₂$, i.e., $g \circ (f₁ \cdot f₂) = (g \circ f₁) \cdot (g \circ f₂)$.

MonoidHom.instInv instance

: Inv (M →* G)

Full source

/-- If `f` is a monoid homomorphism to a commutative group, then `f⁻¹` is the homomorphism sending
`x` to `(f x)⁻¹`. -/
@[to_additive "If `f` is an additive monoid homomorphism to an additive commutative group,
then `-f` is the homomorphism sending `x` to `-(f x)`."]
instance : Inv (M →* G) where
  inv f := mk' (fun g ↦ (f g)⁻¹) fun a b ↦ by simp_rw [← mul_inv, f.map_mul]

Inverse of a Monoid Homomorphism to a Commutative Group

Informal description

For any monoid homomorphism $f \colon M \to G$ where $G$ is a commutative group, the inverse homomorphism $f^{-1}$ is defined by $f^{-1}(x) = (f(x))^{-1}$ for all $x \in M$.

MonoidHom.inv_apply theorem

(f : M →* G) (x : M) : f⁻¹ x = (f x)⁻¹

Full source

@[to_additive (attr := simp)] lemma inv_apply (f : M →* G) (x : M) : f⁻¹ x = (f x)⁻¹ := rfl

Inverse Homomorphism Evaluation Formula: $f^{-1}(x) = (f(x))^{-1}$

Informal description

For any monoid homomorphism $f \colon M \to G$ where $G$ is a commutative group, and for any element $x \in M$, the evaluation of the inverse homomorphism $f^{-1}$ at $x$ equals the inverse of $f(x)$ in $G$, i.e., $f^{-1}(x) = (f(x))^{-1}$.

MonoidHom.inv_comp theorem

(φ : N →* G) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ)⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_comp (φ : N →* G) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ)⁻¹ := rfl

Inverse of Composition of Monoid Homomorphisms

Informal description

For any monoid homomorphisms $\phi \colon N \to G$ and $\psi \colon M \to N$, the composition of the inverse homomorphism $\phi^{-1}$ with $\psi$ equals the inverse of the composition of $\phi$ with $\psi$, i.e., $\phi^{-1} \circ \psi = (\phi \circ \psi)^{-1}$.

MonoidHom.comp_inv theorem

(φ : G →* H) (ψ : M →* G) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Full source

@[to_additive (attr := simp)]
theorem comp_inv (φ : G →* H) (ψ : M →* G) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹ := by
  ext
  simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]

Composition with Inverse Homomorphism Equals Inverse of Composition

Informal description

For any monoid homomorphisms $\phi \colon G \to H$ and $\psi \colon M \to G$, the composition of $\phi$ with the inverse homomorphism $\psi^{-1}$ equals the inverse of the composition of $\phi$ with $\psi$, i.e., $\phi \circ \psi^{-1} = (\phi \circ \psi)^{-1}$.

MonoidHom.instDiv instance

: Div (M →* G)

Full source

/-- If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism
sending `x` to `(f x) / (g x)`. -/
@[to_additive "If `f` and `g` are monoid homomorphisms to an additive commutative group,
then `f - g` is the homomorphism sending `x` to `(f x) - (g x)`."]
instance : Div (M →* G) where
  div f g := mk' (fun x ↦ f x / g x) fun a b ↦ by
    simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]

Division of Monoid Homomorphisms into a Commutative Group

Informal description

For any monoid homomorphisms $f, g : M \to G$ where $G$ is a commutative group, there is a division operation defined by $(f / g)(x) = f(x) / g(x)$ for all $x \in M$.

MonoidHom.div_apply theorem

(f g : M →* G) (x : M) : (f / g) x = f x / g x

Full source

@[to_additive (attr := simp)] lemma div_apply (f g : M →* G) (x : M) : (f / g) x = f x / g x := rfl

Evaluation of Quotient Homomorphism Equals Quotient of Evaluations

Informal description

For any monoid homomorphisms $f, g \colon M \to G$ where $G$ is a commutative group, and for any element $x \in M$, the evaluation of the quotient homomorphism $f / g$ at $x$ is equal to the quotient of the evaluations $f(x) / g(x)$.

MonoidHom.div_comp theorem

(f g : N →* G) (h : M →* N) : (f / g).comp h = f.comp h / g.comp h

Full source

@[to_additive (attr := simp)]
lemma div_comp (f g : N →* G) (h : M →* N) : (f / g).comp h = f.comp h / g.comp h := rfl

Composition of Quotient Homomorphism with Another Homomorphism

Informal description

For any monoid homomorphisms $f, g \colon N \to G$ where $G$ is a commutative group, and any monoid homomorphism $h \colon M \to N$, the composition of the quotient homomorphism $f / g$ with $h$ is equal to the quotient of the compositions $f \circ h$ and $g \circ h$, i.e., $(f / g) \circ h = (f \circ h) / (g \circ h)$.

MonoidHom.comp_div theorem

(f : G →* H) (g h : M →* G) : f.comp (g / h) = f.comp g / f.comp h

Full source

@[to_additive (attr := simp)]
lemma comp_div (f : G →* H) (g h : M →* G) : f.comp (g / h) = f.comp g / f.comp h := by
  ext; simp only [Function.comp_apply, div_apply, map_div, coe_comp]

Composition Preserves Division of Homomorphisms

Informal description

For any monoid homomorphism $f \colon G \to H$ and any monoid homomorphisms $g, h \colon M \to G$, the composition of $f$ with the quotient homomorphism $g / h$ is equal to the quotient of the compositions $f \circ g$ and $f \circ h$, i.e., $f \circ (g / h) = (f \circ g) / (f \circ h)$.

MonoidHom.commGroupOfInjective definition

[Group G] [CommGroup H] (f : G →* H) (hf : Function.Injective f) : CommGroup G

Full source

/-- If `H` is commutative and `G →* H` is injective, then `G` is commutative. -/
def commGroupOfInjective [Group G] [CommGroup H] (f : G →* H) (hf : Function.Injective f) :
    CommGroup G :=
  ⟨by simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]⟩

Injective monoid homomorphism from a group to a commutative group implies commutativity

Informal description

Let $G$ be a group and $H$ be a commutative group. If there exists an injective monoid homomorphism $f : G \to H$, then $G$ is also commutative.

MonoidHom.commGroupOfSurjective definition

[CommGroup G] [Group H] (f : G →* H) (hf : Function.Surjective f) : CommGroup H

Full source

/-- If `G` is commutative and `G →* H` is surjective, then `H` is commutative. -/
def commGroupOfSurjective [CommGroup G] [Group H] (f : G →* H) (hf : Function.Surjective f) :
    CommGroup H :=
  ⟨by simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]⟩

Surjective monoid homomorphism from a commutative group implies commutativity

Informal description

If $ G $ is a commutative group and $ H $ is a group, then any surjective monoid homomorphism $ f : G \to H $ implies that $ H $ is also commutative.