Mathlib.Algebra.Group.Hom.Defs

ZeroHom structure

(M : Type*) (N : Type*) [Zero M] [Zero N]

Full source

/-- `ZeroHom M N` is the type of functions `M → N` that preserve zero.

When possible, instead of parametrizing results over `(f : ZeroHom M N)`,
you should parametrize over `(F : Type*) [ZeroHomClass F M N] (f : F)`.

When you extend this structure, make sure to also extend `ZeroHomClass`.
-/
structure ZeroHom (M : Type*) (N : Type*) [Zero M] [Zero N] where
  /-- The underlying function -/
  protected toFun : M → N
  /-- The proposition that the function preserves 0 -/
  protected map_zero' : toFun 0 = 0

Zero-preserving homomorphism

Informal description

The structure `ZeroHom M N` represents functions from `M` to `N` that preserve the zero element, i.e., a function `f : M → N` such that `f(0) = 0`.

ZeroHomClass structure

(F : Type*) (M N : outParam Type*) [Zero M] [Zero N] [FunLike F M N]

Full source

/-- `ZeroHomClass F M N` states that `F` is a type of zero-preserving homomorphisms.

You should extend this typeclass when you extend `ZeroHom`.
-/
class ZeroHomClass (F : Type*) (M N : outParam Type*) [Zero M] [Zero N] [FunLike F M N] :
    Prop where
  /-- The proposition that the function preserves 0 -/
  map_zero : ∀ f : F, f 0 = 0

Zero-preserving homomorphism class

Informal description

The class `ZeroHomClass F M N` states that `F` is a type of zero-preserving homomorphisms from `M` to `N`, where `M` and `N` are types equipped with zero elements. Specifically, any element `f : F` is a function from `M$ to $N$ that satisfies $f(0) = 0$.

AddHom structure

(M : Type*) (N : Type*) [Add M] [Add N]

Full source

/-- `M →ₙ+ N` is the type of functions `M → N` that preserve addition. The `ₙ` in the notation
stands for "non-unital" because it is intended to match the notation for `NonUnitalAlgHom` and
`NonUnitalRingHom`, so a `AddHom` is a non-unital additive monoid hom.

When possible, instead of parametrizing results over `(f : AddHom M N)`,
you should parametrize over `(F : Type*) [AddHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `AddHomClass`.
-/
structure AddHom (M : Type*) (N : Type*) [Add M] [Add N] where
  /-- The underlying function -/
  protected toFun : M → N
  /-- The proposition that the function preserves addition -/
  protected map_add' : ∀ x y, toFun (x + y) = toFun x + toFun y

Non-unital additive homomorphism

Informal description

The structure representing a non-unital additive homomorphism between types `M` and `N` equipped with addition operations. An element of `AddHom M N` is a function `f : M → N` that preserves addition, i.e., satisfies `f (x + y) = f x + f y` for all `x, y ∈ M`.

term_→ₙ+_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M →ₙ+ N` denotes the type of addition-preserving maps from `M` to `N`. -/
infixr:25 " →ₙ+ " => AddHom

Notation for addition-preserving maps

Informal description

The notation `M →ₙ+ N` represents the type of addition-preserving maps from `M` to `N`.

AddHomClass structure

(F : Type*) (M N : outParam Type*) [Add M] [Add N] [FunLike F M N]

Full source

/-- `AddHomClass F M N` states that `F` is a type of addition-preserving homomorphisms.
You should declare an instance of this typeclass when you extend `AddHom`.
-/
class AddHomClass (F : Type*) (M N : outParam Type*) [Add M] [Add N] [FunLike F M N] : Prop where
  /-- The proposition that the function preserves addition -/
  map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y

Addition-Preserving Homomorphism Class

Informal description

The class `AddHomClass F M N` asserts that `F` is a type of addition-preserving homomorphisms between additive structures `M` and `N`. Specifically, any element `f : F` is a function from `M` to `N` that preserves addition, i.e., satisfies $f(x + y) = f(x) + f(y)$ for all $x, y \in M$.

AddMonoidHom structure

(M : Type*) (N : Type*) [AddZeroClass M] [AddZeroClass N] extends
  ZeroHom M N, AddHom M N

Full source

/-- `M →+ N` is the type of functions `M → N` that preserve the `AddZeroClass` structure.

`AddMonoidHom` is also used for group homomorphisms.

When possible, instead of parametrizing results over `(f : M →+ N)`,
you should parametrize over `(F : Type*) [AddMonoidHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `AddMonoidHomClass`.
-/
structure AddMonoidHom (M : Type*) (N : Type*) [AddZeroClass M] [AddZeroClass N] extends
  ZeroHom M N, AddHom M N

Additive Monoid Homomorphism

Informal description

The structure `AddMonoidHom M N` represents bundled homomorphisms between additive monoids (or groups) `M` and `N`. These are functions `f : M → N` that preserve the additive structure, including the zero element and addition. More precisely, an `AddMonoidHom` is a function that satisfies: 1. $f(0) = 0$ (preservation of zero) 2. $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ (preservation of addition) This structure is also used for group homomorphisms between additive groups.

term_→+_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M →+ N` denotes the type of additive monoid homomorphisms from `M` to `N`. -/
infixr:25 " →+ " => AddMonoidHom

Additive monoid homomorphism notation

Informal description

The notation `M →+ N` represents the type of additive monoid homomorphisms from `M` to `N`.

AddMonoidHomClass structure

(F : Type*) (M N : outParam Type*)
    [AddZeroClass M] [AddZeroClass N] [FunLike F M N] : Prop
    extends AddHomClass F M N, ZeroHomClass F M N

Full source

/-- `AddMonoidHomClass F M N` states that `F` is a type of `AddZeroClass`-preserving
homomorphisms.

You should also extend this typeclass when you extend `AddMonoidHom`.
-/
class AddMonoidHomClass (F : Type*) (M N : outParam Type*)
    [AddZeroClass M] [AddZeroClass N] [FunLike F M N] : Prop
    extends AddHomClass F M N, ZeroHomClass F M N

Class of Additive Monoid Homomorphisms

Informal description

The class `AddMonoidHomClass F M N` states that `F` is a type of additive monoid homomorphisms between additive monoids `M` and `N`, i.e., functions that preserve both the additive structure and the zero element. This class extends `AddHomClass` (preservation of addition) and `ZeroHomClass` (preservation of zero).

OneHom structure

(M : Type*) (N : Type*) [One M] [One N]

Full source

/-- `OneHom M N` is the type of functions `M → N` that preserve one.

When possible, instead of parametrizing results over `(f : OneHom M N)`,
you should parametrize over `(F : Type*) [OneHomClass F M N] (f : F)`.

When you extend this structure, make sure to also extend `OneHomClass`.
-/
@[to_additive]
structure OneHom (M : Type*) (N : Type*) [One M] [One N] where
  /-- The underlying function -/
  protected toFun : M → N
  /-- The proposition that the function preserves 1 -/
  protected map_one' : toFun 1 = 1

Identity-preserving homomorphism

Informal description

The structure `OneHom M N` represents functions from a type `M` with a distinguished element `1` to a type `N` with a distinguished element `1` that preserve the identity element, i.e., a function `f : M → N` such that `f(1) = 1`.

OneHomClass structure

(F : Type*) (M N : outParam Type*) [One M] [One N] [FunLike F M N]

Full source

/-- `OneHomClass F M N` states that `F` is a type of one-preserving homomorphisms.
You should extend this typeclass when you extend `OneHom`.
-/
@[to_additive]
class OneHomClass (F : Type*) (M N : outParam Type*) [One M] [One N] [FunLike F M N] : Prop where
  /-- The proposition that the function preserves 1 -/
  map_one : ∀ f : F, f 1 = 1

Class of identity-preserving homomorphisms

Informal description

The class `OneHomClass F M N` states that `F` is a type of homomorphisms between types `M` and `N` (each equipped with a distinguished element `1`) that preserve the identity element, i.e., for any `f : F`, we have `f(1) = 1`.

OneHom.funLike instance

: FunLike (OneHom M N) M N

Full source

@[to_additive]
instance OneHom.funLike : FunLike (OneHom M N) M N where
  coe := OneHom.toFun
  coe_injective' f g h := by cases f; cases g; congr

Function-Like Structure of Identity-Preserving Homomorphisms

Informal description

For any types $M$ and $N$ each equipped with a distinguished element $1$, the type of identity-preserving homomorphisms $\text{OneHom}(M, N)$ can be treated as a function-like type, meaning its elements can be coerced to functions from $M$ to $N$.

OneHom.oneHomClass instance

: OneHomClass (OneHom M N) M N

Full source

@[to_additive]
instance OneHom.oneHomClass : OneHomClass (OneHom M N) M N where
  map_one := OneHom.map_one'

Identity-Preserving Homomorphisms as a Class

Informal description

For any types $M$ and $N$ each equipped with a distinguished element $1$, the type of identity-preserving homomorphisms $\text{OneHom}(M, N)$ forms a class of homomorphisms that preserve the identity element.

map_one theorem

[OneHomClass F M N] (f : F) : f 1 = 1

Full source

/-- See note [low priority simp lemmas] -/
@[to_additive (attr := simp low)]
theorem map_one [OneHomClass F M N] (f : F) : f 1 = 1 :=
  OneHomClass.map_one f

Identity Preservation under Homomorphisms

Informal description

For any homomorphism $f$ in a type $F$ that preserves the identity element (i.e., $F$ is a `OneHomClass`), the image of the identity element $1$ under $f$ is again $1$, i.e., $f(1) = 1$.

map_comp_one theorem

[OneHomClass F M N] (f : F) : f ∘ (1 : ι → M) = 1

Full source

@[to_additive] lemma map_comp_one [OneHomClass F M N] (f : F) : f ∘ (1 : ι → M) = 1 := by simp

Composition with Constant One Function Preserves Identity

Informal description

For any homomorphism $f$ in a type $F$ that preserves the identity element (i.e., $F$ is a `OneHomClass`), the composition of $f$ with the constant function $1 : \iota \to M$ is equal to the constant function $1 : \iota \to N$. In other words, $(f \circ 1)(x) = 1$ for all $x \in \iota$.

Subsingleton.of_oneHomClass theorem

[Subsingleton M] [OneHomClass F M N] : Subsingleton F

Full source

/-- In principle this could be an instance, but in practice it causes performance issues. -/
@[to_additive]
theorem Subsingleton.of_oneHomClass [Subsingleton M] [OneHomClass F M N] :
    Subsingleton F where
  allEq f g := DFunLike.ext _ _ fun x ↦ by simp [Subsingleton.elim x 1]

Subsingleton Property of Identity-Preserving Homomorphisms from a Subsingleton

Informal description

If $M$ is a subsingleton (i.e., has at most one element) and $F$ is a type of identity-preserving homomorphisms from $M$ to $N$, then $F$ is also a subsingleton.

instSubsingletonOneHom instance

[Subsingleton M] : Subsingleton (OneHom M N)

Full source

@[to_additive] instance [Subsingleton M] : Subsingleton (OneHom M N) := .of_oneHomClass

Subsingleton Property of Identity-Preserving Homomorphisms from a Subsingleton

Informal description

If $M$ is a subsingleton (i.e., has at most one element), then the type of identity-preserving homomorphisms from $M$ to $N$ is also a subsingleton.

map_eq_one_iff theorem

[OneHomClass F M N] (f : F) (hf : Function.Injective f) {x : M} : f x = 1 ↔ x = 1

Full source

@[to_additive]
theorem map_eq_one_iff [OneHomClass F M N] (f : F) (hf : Function.Injective f)
    {x : M} :
    f x = 1 ↔ x = 1 := hf.eq_iff' (map_one f)

Injective Homomorphism Preserves Identity: $f(x) = 1 \leftrightarrow x = 1$

Informal description

Let $F$ be a type of homomorphisms between monoids $M$ and $N$ that preserve the identity element (i.e., $f(1) = 1$ for any $f \in F$). For any injective homomorphism $f \in F$ and any element $x \in M$, we have $f(x) = 1$ if and only if $x = 1$.

map_ne_one_iff theorem

 {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S] (f : F) (hf : Function.Injective f) {x : R} :
  f x ≠ 1 ↔ x ≠ 1

Full source

@[to_additive]
theorem map_ne_one_iff {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S] (f : F)
    (hf : Function.Injective f) {x : R} : f x ≠ 1f x ≠ 1 ↔ x ≠ 1 := (map_eq_one_iff f hf).not

Injective Homomorphism Preserves Non-Identity: $f(x) \neq 1 \leftrightarrow x \neq 1$

Informal description

Let $R$ and $S$ be types with distinguished elements $1$, and let $F$ be a type of homomorphisms from $R$ to $S$ that preserve the identity element. For any injective homomorphism $f \in F$ and any element $x \in R$, we have $f(x) \neq 1$ if and only if $x \neq 1$.

ne_one_of_map theorem

{R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S] {f : F} {x : R} (hx : f x ≠ 1) : x ≠ 1

Full source

@[to_additive]
theorem ne_one_of_map {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S]
    {f : F} {x : R} (hx : f x ≠ 1) : x ≠ 1 := ne_of_apply_ne f <| (by rwa [(map_one f)])

Non-Identity Elements are Preserved under Homomorphisms

Informal description

Let $R$ and $S$ be types with distinguished elements $1$, and let $F$ be a type of homomorphisms from $R$ to $S$ that preserve the identity element. For any homomorphism $f \in F$ and any element $x \in R$, if $f(x) \neq 1$, then $x \neq 1$.

OneHomClass.toOneHom definition

[OneHomClass F M N] (f : F) : OneHom M N

Full source

/-- Turn an element of a type `F` satisfying `OneHomClass F M N` into an actual
`OneHom`. This is declared as the default coercion from `F` to `OneHom M N`. -/
@[to_additive (attr := coe)
"Turn an element of a type `F` satisfying `ZeroHomClass F M N` into an actual
`ZeroHom`. This is declared as the default coercion from `F` to `ZeroHom M N`."]
def OneHomClass.toOneHom [OneHomClass F M N] (f : F) : OneHom M N where
  toFun := f
  map_one' := map_one f

Conversion from OneHomClass to OneHom

Informal description

Given a type `F` satisfying `OneHomClass F M N`, this function converts an element `f : F` into an actual `OneHom M N` by extracting the underlying function and its property of preserving the identity element (i.e., `f(1) = 1`).

instCoeTCOneHomOfOneHomClass instance

[OneHomClass F M N] : CoeTC F (OneHom M N)

Full source

/-- Any type satisfying `OneHomClass` can be cast into `OneHom` via `OneHomClass.toOneHom`. -/
@[to_additive "Any type satisfying `ZeroHomClass` can be cast into `ZeroHom` via
`ZeroHomClass.toZeroHom`. "]
instance [OneHomClass F M N] : CoeTC F (OneHom M N) :=
  ⟨OneHomClass.toOneHom⟩

Coercion from `OneHomClass` to `OneHom`

Informal description

For any type $F$ satisfying `OneHomClass F M N`, there is a canonical coercion from $F$ to `OneHom M N`, which maps each element $f \in F$ to the corresponding identity-preserving homomorphism from $M$ to $N$.

OneHom.coe_coe theorem

[OneHomClass F M N] (f : F) : ((f : OneHom M N) : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem OneHom.coe_coe [OneHomClass F M N] (f : F) :
    ((f : OneHom M N) : M → N) = f := rfl

Coercion Consistency for Identity-Preserving Homomorphisms

Informal description

For any type `F` that is an instance of `OneHomClass F M N`, and for any element `f : F`, the function obtained by first coercing `f` to a `OneHom M N` and then to a function `M → N` is equal to `f` itself.

MulHom structure

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

Full source

/-- `M →ₙ* N` is the type of functions `M → N` that preserve multiplication. The `ₙ` in the notation
stands for "non-unital" because it is intended to match the notation for `NonUnitalAlgHom` and
`NonUnitalRingHom`, so a `MulHom` is a non-unital monoid hom.

When possible, instead of parametrizing results over `(f : M →ₙ* N)`,
you should parametrize over `(F : Type*) [MulHomClass F M N] (f : F)`.
When you extend this structure, make sure to extend `MulHomClass`.
-/
@[to_additive]
structure MulHom (M : Type*) (N : Type*) [Mul M] [Mul N] where
  /-- The underlying function -/
  protected toFun : M → N
  /-- The proposition that the function preserves multiplication -/
  protected map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

Non-unital multiplicative homomorphism

Informal description

The structure `MulHom M N` represents the type of functions from a multiplicative structure `M` to another multiplicative structure `N` that preserve multiplication. The notation `→ₙ*` emphasizes that these are non-unital homomorphisms, meaning they do not necessarily preserve the multiplicative identity.

term_→ₙ*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M →ₙ* N` denotes the type of multiplication-preserving maps from `M` to `N`. -/
infixr:25 " →ₙ* " => MulHom

Multiplication-preserving maps notation

Informal description

The notation `M →ₙ* N` represents the type of multiplication-preserving maps from a multiplicative structure `M` to another multiplicative structure `N`.

MulHomClass structure

(F : Type*) (M N : outParam Type*) [Mul M] [Mul N] [FunLike F M N]

Full source

/-- `MulHomClass F M N` states that `F` is a type of multiplication-preserving homomorphisms.

You should declare an instance of this typeclass when you extend `MulHom`.
-/
@[to_additive]
class MulHomClass (F : Type*) (M N : outParam Type*) [Mul M] [Mul N] [FunLike F M N] : Prop where
  /-- The proposition that the function preserves multiplication -/
  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

Class of Multiplication-Preserving Homomorphisms

Informal description

The class `MulHomClass F M N` indicates that `F` is a type of homomorphisms between multiplicative structures `M` and `N` that preserve multiplication. Specifically, for any `f : F` and any elements `x, y ∈ M`, the homomorphism satisfies `f (x * y) = f x * f y`.

MulHom.funLike instance

: FunLike (M →ₙ* N) M N

Full source

@[to_additive]
instance MulHom.funLike : FunLike (M →ₙ* N) M N where
  coe := MulHom.toFun
  coe_injective' f g h := by cases f; cases g; congr

Injective Coercion of Non-unital Multiplicative Homomorphisms to Functions

Informal description

For any multiplicative structures $M$ and $N$, the type $M \toₙ* N$ of non-unital multiplicative homomorphisms from $M$ to $N$ can be coerced to a function from $M$ to $N$. This coercion is injective, meaning that if two homomorphisms $f$ and $g$ in $M \toₙ* N$ satisfy $f(x) = g(x)$ for all $x \in M$, then $f = g$.

MulHom.mulHomClass instance

: MulHomClass (M →ₙ* N) M N

Full source

/-- `MulHom` is a type of multiplication-preserving homomorphisms -/
@[to_additive "`AddHom` is a type of addition-preserving homomorphisms"]
instance MulHom.mulHomClass : MulHomClass (M →ₙ* N) M N where
  map_mul := MulHom.map_mul'

Non-unital Multiplicative Homomorphisms Preserve Multiplication

Informal description

For any multiplicative structures $M$ and $N$, the type $M \toₙ* N$ of non-unital multiplicative homomorphisms from $M$ to $N$ forms a `MulHomClass`. This means that every homomorphism $f \in M \toₙ* N$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M$.

map_mul theorem

[MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y

Full source

/-- See note [low priority simp lemmas] -/
@[to_additive (attr := simp low)]
theorem map_mul [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y :=
  MulHomClass.map_mul f x y

Multiplication-Preserving Property of Homomorphisms

Informal description

For any multiplicative structures $M$ and $N$, and any homomorphism $f \colon M \to N$ in the class `MulHomClass`, the function $f$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M$.

map_comp_mul theorem

[MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h) = f ∘ g * f ∘ h

Full source

@[to_additive (attr := simp)]
lemma map_comp_mul [MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h) = f ∘ g * f ∘ h := by
  ext; simp

Composition of Homomorphism with Pointwise Product

Informal description

For any multiplicative structures $M$ and $N$, and any homomorphism $f \colon M \to N$ in the class `MulHomClass`, the composition of $f$ with the pointwise product of two functions $g, h \colon \iota \to M$ equals the pointwise product of the compositions $f \circ g$ and $f \circ h$. That is, for all index types $\iota$ and functions $g, h \colon \iota \to M$, we have: $$ f \circ (g \cdot h) = (f \circ g) \cdot (f \circ h) $$ where $\cdot$ denotes pointwise multiplication.

MulHomClass.toMulHom definition

[MulHomClass F M N] (f : F) : M →ₙ* N

Full source

/-- Turn an element of a type `F` satisfying `MulHomClass F M N` into an actual
`MulHom`. This is declared as the default coercion from `F` to `M →ₙ* N`. -/
@[to_additive (attr := coe)
"Turn an element of a type `F` satisfying `AddHomClass F M N` into an actual
`AddHom`. This is declared as the default coercion from `F` to `M →ₙ+ N`."]
def MulHomClass.toMulHom [MulHomClass F M N] (f : F) : M →ₙ* N where
  toFun := f
  map_mul' := map_mul f

Coercion from multiplication-preserving homomorphism class to concrete multiplicative homomorphism

Informal description

Given a type `F` satisfying `MulHomClass F M N` (i.e., elements of `F` are multiplication-preserving homomorphisms between multiplicative structures `M` and `N`), the function converts an element `f : F` into an actual `MulHom` (non-unital multiplicative homomorphism) from `M` to `N`. This is the default coercion from `F` to `M →ₙ* N`. The resulting homomorphism has: - Underlying function `f` itself - The property that it preserves multiplication: `f (x * y) = f x * f y` for all `x, y ∈ M`

instCoeTCMulHomOfMulHomClass instance

[MulHomClass F M N] : CoeTC F (M →ₙ* N)

Full source

/-- Any type satisfying `MulHomClass` can be cast into `MulHom` via `MulHomClass.toMulHom`. -/
@[to_additive "Any type satisfying `AddHomClass` can be cast into `AddHom` via
`AddHomClass.toAddHom`."]
instance [MulHomClass F M N] : CoeTC F (M →ₙ* N) :=
  ⟨MulHomClass.toMulHom⟩

Canonical Coercion from `MulHomClass` to Concrete Multiplicative Homomorphism

Informal description

For any type $F$ that satisfies `MulHomClass F M N` (i.e., elements of $F$ are multiplication-preserving homomorphisms between multiplicative structures $M$ and $N$), there is a canonical way to coerce an element $f \in F$ into a concrete multiplicative homomorphism $M \to N$ (denoted $M \toₙ* N$), where the underlying function is $f$ itself and it preserves multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in M$.

MulHom.coe_coe theorem

[MulHomClass F M N] (f : F) : ((f : MulHom M N) : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem MulHom.coe_coe [MulHomClass F M N] (f : F) : ((f : MulHom M N) : M → N) = f := rfl

Double Coercion of Multiplication-Preserving Homomorphisms Preserves Function

Informal description

For any type `F` that is a class of multiplication-preserving homomorphisms between multiplicative structures `M` and `N`, and for any homomorphism `f : F`, the underlying function of `f` when coerced to a `MulHom` and then to a plain function is equal to `f` itself. In other words, the double coercion `(f : MulHom M N) : M → N` yields the original function `f`.

MonoidHom structure

(M : Type*) (N : Type*) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

Full source

/-- `M →* N` is the type of functions `M → N` that preserve the `Monoid` structure.
`MonoidHom` is also used for group homomorphisms.

When possible, instead of parametrizing results over `(f : M →* N)`,
you should parametrize over `(F : Type*) [MonoidHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `MonoidHomClass`.
-/
@[to_additive]
structure MonoidHom (M : Type*) (N : Type*) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

Monoid Homomorphism

Informal description

The structure representing bundled homomorphisms between monoids (or groups), i.e., functions $ f \colon M \to N $ that preserve the monoid structure (multiplication and identity). This is also used for group homomorphisms.

term_→*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M →* N` denotes the type of monoid homomorphisms from `M` to `N`. -/
infixr:25 " →* " => MonoidHom

Monoid homomorphism notation

Informal description

The notation `M →* N` denotes the type of monoid homomorphisms from `M$ to $N$, i.e., functions that preserve the multiplicative structure and the identity element.

MonoidHomClass structure

(F : Type*) (M N : outParam Type*) [MulOneClass M] [MulOneClass N]
  [FunLike F M N] : Prop
  extends MulHomClass F M N, OneHomClass F M N

Full source

/-- `MonoidHomClass F M N` states that `F` is a type of `Monoid`-preserving homomorphisms.
You should also extend this typeclass when you extend `MonoidHom`. -/
@[to_additive]
class MonoidHomClass (F : Type*) (M N : outParam Type*) [MulOneClass M] [MulOneClass N]
  [FunLike F M N] : Prop
  extends MulHomClass F M N, OneHomClass F M N

Monoid Homomorphism Class

Informal description

The class `MonoidHomClass F M N` states that `F` is a type of homomorphisms between monoids `M` and `N` that preserve the multiplicative structure (including the identity element). This class extends both `MulHomClass` (preservation of multiplication) and `OneHomClass` (preservation of the identity element).

MonoidHom.instFunLike instance

: FunLike (M →* N) M N

Full source

@[to_additive]
instance MonoidHom.instFunLike : FunLike (M →* N) M N where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective'
    exact h

Monoid Homomorphisms as Functions

Informal description

For any two monoids $M$ and $N$, the type of monoid homomorphisms $M \to^* N$ can be treated as a function-like type, meaning there is a canonical way to interpret a monoid homomorphism as a function from $M$ to $N$.

MonoidHom.instMonoidHomClass instance

: MonoidHomClass (M →* N) M N

Full source

@[to_additive]
instance MonoidHom.instMonoidHomClass : MonoidHomClass (M →* N) M N where
  map_mul := MonoidHom.map_mul'
  map_one f := f.toOneHom.map_one'

Monoid Homomorphisms as a Monoid Homomorphism Class

Informal description

For any two monoids $M$ and $N$, the type of monoid homomorphisms $M \to^* N$ forms a `MonoidHomClass`, meaning these homomorphisms preserve both the multiplicative structure and the identity element.

instSubsingletonMonoidHom instance

[Subsingleton M] : Subsingleton (M →* N)

Full source

@[to_additive] instance [Subsingleton M] : Subsingleton (M →* N) := .of_oneHomClass

Subsingleton Property of Monoid Homomorphisms from a Subsingleton Monoid

Informal description

For any monoid $M$ that is a subsingleton (i.e., has at most one element) and any monoid $N$, the type of monoid homomorphisms from $M$ to $N$ is also a subsingleton.

MonoidHomClass.toMonoidHom definition

[MonoidHomClass F M N] (f : F) : M →* N

Full source

/-- Turn an element of a type `F` satisfying `MonoidHomClass F M N` into an actual
`MonoidHom`. This is declared as the default coercion from `F` to `M →* N`. -/
@[to_additive (attr := coe)
"Turn an element of a type `F` satisfying `AddMonoidHomClass F M N` into an
actual `MonoidHom`. This is declared as the default coercion from `F` to `M →+ N`."]
def MonoidHomClass.toMonoidHom [MonoidHomClass F M N] (f : F) : M →* N :=
  { (f : M →ₙ* N), (f : OneHom M N) with }

Conversion from Monoid Homomorphism Class to Monoid Homomorphism

Informal description

Given a type `F` satisfying `MonoidHomClass F M N`, the function converts an element `f : F` into an actual monoid homomorphism from `M` to `N`, preserving both the multiplicative structure and the identity element.

instCoeTCMonoidHomOfMonoidHomClass instance

[MonoidHomClass F M N] : CoeTC F (M →* N)

Full source

/-- Any type satisfying `MonoidHomClass` can be cast into `MonoidHom` via
`MonoidHomClass.toMonoidHom`. -/
@[to_additive "Any type satisfying `AddMonoidHomClass` can be cast into `AddMonoidHom` via
`AddMonoidHomClass.toAddMonoidHom`."]
instance [MonoidHomClass F M N] : CoeTC F (M →* N) :=
  ⟨MonoidHomClass.toMonoidHom⟩

Canonical Coercion from Monoid Homomorphism Class to Monoid Homomorphism

Informal description

For any type $F$ satisfying `MonoidHomClass F M N`, there is a canonical coercion from $F$ to the type of monoid homomorphisms $M \to^* N$.

MonoidHom.coe_coe theorem

[MonoidHomClass F M N] (f : F) : ((f : M →* N) : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.coe_coe [MonoidHomClass F M N] (f : F) : ((f : M →* N) : M → N) = f := rfl

Coercion of Monoid Homomorphism to Function is Identity

Informal description

For any monoid homomorphism $f \colon M \to N$ in a type $F$ satisfying `MonoidHomClass F M N`, the underlying function of $f$ when coerced to a monoid homomorphism is equal to $f$ itself.

map_mul_eq_one theorem

[MonoidHomClass F M N] (f : F) {a b : M} (h : a * b = 1) : f a * f b = 1

Full source

@[to_additive]
theorem map_mul_eq_one [MonoidHomClass F M N] (f : F) {a b : M} (h : a * b = 1) :
    f a * f b = 1 := by
  rw [← map_mul, h, map_one]

Monoid homomorphisms preserve inverses: $f(a) * f(b) = 1$ when $a * b = 1$

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any elements $a, b \in M$ such that $a * b = 1_M$, we have $f(a) * f(b) = 1_N$.

map_div' theorem

 [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H] (f : F) (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (a b : G) :
  f (a / b) = f a / f b

Full source

@[to_additive]
theorem map_div' [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H]
    (f : F) (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (a b : G) : f (a / b) = f a / f b := by
  rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]

Division-Preserving Property of Homomorphisms in DivInvMonoids

Informal description

Let $G$ and $H$ be divison-inverse monoids, and let $F$ be a type of homomorphisms from $G$ to $H$ that preserve multiplication. For any homomorphism $f \colon G \to H$ in $F$ satisfying $f(a^{-1}) = (f(a))^{-1}$ for all $a \in G$, and for any elements $a, b \in G$, we have $f(a / b) = f(a) / f(b)$.

map_comp_div' theorem

 [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H] (f : F) (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (g h : ι → G) :
  f ∘ (g / h) = f ∘ g / f ∘ h

Full source

@[to_additive]
lemma map_comp_div' [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H] (f : F)
    (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (g h : ι → G) : f ∘ (g / h) = f ∘ g / f ∘ h := by
  ext; simp [map_div' f hf]

Composition with Pointwise Division Preserved by Homomorphism

Informal description

Let $G$ and $H$ be division-inverse monoids, and let $F$ be a type of homomorphisms from $G$ to $H$ that preserve multiplication. For any homomorphism $f \colon G \to H$ in $F$ satisfying $f(a^{-1}) = (f(a))^{-1}$ for all $a \in G$, and for any functions $g, h \colon \iota \to G$, the composition of $f$ with the pointwise division $g / h$ equals the pointwise division of $f \circ g$ and $f \circ h$, i.e., $$ f \circ (g / h) = (f \circ g) / (f \circ h). $$

map_inv theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a : G) : f a⁻¹ = (f a)⁻¹

Full source

/-- Group homomorphisms preserve inverse.

See note [low priority simp lemmas] -/
@[to_additive (attr := simp low) "Additive group homomorphisms preserve negation."]
theorem map_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H]
    (f : F) (a : G) : f a⁻¹ = (f a)⁻¹ :=
  eq_inv_of_mul_eq_one_left <| map_mul_eq_one f <| inv_mul_cancel _

Monoid homomorphisms preserve inverses: $f(a^{-1}) = (f(a))^{-1}$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any element $a \in G$, the image of the inverse $f(a^{-1})$ is equal to the inverse of the image $(f(a))^{-1}$.

map_comp_inv theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) : f ∘ g⁻¹ = (f ∘ g)⁻¹

Full source

@[to_additive (attr := simp)]
lemma map_comp_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) :
    f ∘ g⁻¹ = (f ∘ g)⁻¹ := by ext; simp

Composition with Pointwise Inverse Preserved by Monoid Homomorphism

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any function $g \colon \iota \to G$, the composition of $f$ with the pointwise inverse $g^{-1}$ equals the pointwise inverse of $f \circ g$, i.e., $$ f \circ g^{-1} = (f \circ g)^{-1}. $$

map_mul_inv theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a b : G) : f (a * b⁻¹) = f a * (f b)⁻¹

Full source

/-- Group homomorphisms preserve division. -/
@[to_additive "Additive group homomorphisms preserve subtraction."]
theorem map_mul_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a b : G) :
    f (a * b⁻¹) = f a * (f b)⁻¹ := by rw [map_mul, map_inv]

Homomorphism preserves multiplication by inverse: $f(a \cdot b^{-1}) = f(a) \cdot f(b)^{-1}$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any elements $a, b \in G$, the homomorphism preserves the operation of multiplying by an inverse, i.e., $f(a \cdot b^{-1}) = f(a) \cdot (f(b))^{-1}$.

map_comp_mul_inv theorem

 [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) : f ∘ (g * h⁻¹) = f ∘ g * (f ∘ h)⁻¹

Full source

@[to_additive]
lemma map_comp_mul_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) :
    f ∘ (g * h⁻¹) = f ∘ g * (f ∘ h)⁻¹ := by simp

Homomorphism preserves composition with pointwise product and inverse

Informal description

Let $G$ be a group and $H$ a division monoid. For any monoid homomorphism $f \colon G \to H$ and any functions $g, h \colon \iota \to G$, the composition of $f$ with the pointwise product $g \cdot h^{-1}$ equals the pointwise product of $f \circ g$ and $(f \circ h)^{-1}$. That is, $$ f \circ (g \cdot h^{-1}) = (f \circ g) \cdot (f \circ h)^{-1}. $$

map_div theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) : ∀ a b, f (a / b) = f a / f b

Full source

/-- Group homomorphisms preserve division.

See note [low priority simp lemmas] -/
@[to_additive (attr := simp low) "Additive group homomorphisms preserve subtraction."]
theorem map_div [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) :
    ∀ a b, f (a / b) = f a / f b := map_div' _ <| map_inv f

Monoid homomorphisms preserve division: $f(a / b) = f(a) / f(b)$

Informal description

Let $G$ be a group and $H$ a division monoid. For any monoid homomorphism $f \colon G \to H$ and any elements $a, b \in G$, the homomorphism $f$ preserves division, i.e., $f(a / b) = f(a) / f(b)$.

map_comp_div theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) : f ∘ (g / h) = f ∘ g / f ∘ h

Full source

@[to_additive (attr := simp)]
lemma map_comp_div [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) :
    f ∘ (g / h) = f ∘ g / f ∘ h := by ext; simp

Homomorphism Preserves Composition with Pointwise Division: $f \circ (g / h) = (f \circ g) / (f \circ h)$

Informal description

Let $G$ be a group and $H$ a division monoid. For any monoid homomorphism $f \colon G \to H$ and any functions $g, h \colon \iota \to G$, the composition of $f$ with the pointwise division $g / h$ equals the pointwise division of $f \circ g$ and $f \circ h$. That is, $$ f \circ (g / h) = (f \circ g) / (f \circ h). $$

map_pow theorem

[Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) : ∀ n : ℕ, f (a ^ n) = f a ^ n

Full source

/-- See note [low priority simp lemmas] -/
@[to_additive (attr := simp low) (reorder := 9 10)]
theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) :
    ∀ n : ℕ, f (a ^ n) = f a ^ n
  | 0 => by rw [pow_zero, pow_zero, map_one]
  | n + 1 => by rw [pow_succ, pow_succ, map_mul, map_pow f a n]

Power Preservation under Monoid Homomorphisms

Informal description

Let $G$ and $H$ be monoids, and let $F$ be a type of homomorphisms from $G$ to $H$ that preserve the monoid structure. For any homomorphism $f \in F$ and any element $a \in G$, the image of $a^n$ under $f$ equals the $n$-th power of $f(a)$ for all natural numbers $n$, i.e., $f(a^n) = (f(a))^n$.

map_comp_pow theorem

[Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ) : f ∘ (g ^ n) = f ∘ g ^ n

Full source

@[to_additive (attr := simp)]
lemma map_comp_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ) :
    f ∘ (g ^ n) = f ∘ g ^ n := by ext; simp

Composition with Power Preserved under Monoid Homomorphism: $f \circ (g^n) = (f \circ g)^n$

Informal description

Let $G$ and $H$ be monoids, and let $F$ be a type of homomorphisms from $G$ to $H$ that preserve the monoid structure. For any homomorphism $f \in F$ and any function $g : \iota \to G$, the composition of $f$ with the $n$-th power of $g$ equals the $n$-th power of the composition of $f$ with $g$, i.e., $f \circ (g^n) = (f \circ g)^n$ for all natural numbers $n$.

map_zpow' theorem

 [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (a : G) :
  ∀ n : ℤ, f (a ^ n) = f a ^ n

Full source

@[to_additive]
theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H]
    (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (a : G) : ∀ n : ℤ, f (a ^ n) = f a ^ n
  | (n : ℕ) => by rw [zpow_natCast, map_pow, zpow_natCast]
  | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]

Integer Power Preservation under Monoid Homomorphisms with Inverse Condition

Informal description

Let $G$ and $H$ be div-inverse monoids, and let $F$ be a type of homomorphisms from $G$ to $H$ that preserve the monoid structure. For any homomorphism $f \in F$ satisfying $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G$, and for any element $a \in G$, the image of $a^n$ under $f$ equals the $n$-th power of $f(a)$ for all integers $n$, i.e., $f(a^n) = (f(a))^n$.

map_comp_zpow' theorem

 [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (g : ι → G) (n : ℤ) :
  f ∘ (g ^ n) = f ∘ g ^ n

Full source

@[to_additive (attr := simp)]
lemma map_comp_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F)
    (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (g : ι → G) (n : ℤ) : f ∘ (g ^ n) = f ∘ g ^ n := by
  ext; simp [map_zpow' f hf]

Composition with Integer Power Preserved under Monoid Homomorphism with Inverse Condition: $f \circ (g^n) = (f \circ g)^n$

Informal description

Let $G$ and $H$ be div-inverse monoids, and let $F$ be a type of homomorphisms from $G$ to $H$ that preserve the monoid structure. For any homomorphism $f \in F$ satisfying $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G$, and for any function $g : \iota \to G$, the composition of $f$ with the $n$-th power of $g$ equals the $n$-th power of the composition of $f$ with $g$, i.e., $f \circ (g^n) = (f \circ g)^n$ for all integers $n$.

map_zpow theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : G) (n : ℤ) : f (g ^ n) = f g ^ n

Full source

/-- Group homomorphisms preserve integer power.

See note [low priority simp lemmas] -/
@[to_additive (attr := simp low) (reorder := 9 10)
"Additive group homomorphisms preserve integer scaling."]
theorem map_zpow [Group G] [DivisionMonoid H] [MonoidHomClass F G H]
    (f : F) (g : G) (n : ℤ) : f (g ^ n) = f g ^ n := map_zpow' f (map_inv f) g n

Monoid Homomorphisms Preserve Integer Powers: $f(g^n) = f(g)^n$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any element $g \in G$, the image of $g^n$ under $f$ equals the $n$-th power of $f(g)$ for all integers $n$, i.e., $f(g^n) = (f(g))^n$.

map_comp_zpow theorem

[Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℤ) : f ∘ (g ^ n) = f ∘ g ^ n

Full source

@[to_additive]
lemma map_comp_zpow [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G)
    (n : ℤ) : f ∘ (g ^ n) = f ∘ g ^ n := by simp

Monoid homomorphism preserves composition with integer powers: $f \circ (g^n) = (f \circ g)^n$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any function $g \colon \iota \to G$, the composition of $f$ with the $n$-th power of $g$ equals the $n$-th power of the composition of $f$ with $g$, i.e., $f \circ (g^n) = (f \circ g)^n$ for all integers $n$.

MonoidHom.coeToOneHom instance

[MulOneClass M] [MulOneClass N] : Coe (M →* N) (OneHom M N)

Full source

/-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property. -/
@[to_additive "`AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property"]
instance MonoidHom.coeToOneHom [MulOneClass M] [MulOneClass N] :
  Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩

Monoid Homomorphism as Identity-Preserving Function

Informal description

For any monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, $f$ can be viewed as a function that preserves the identity element, i.e., $f(1) = 1$.

MonoidHom.coeToMulHom instance

[MulOneClass M] [MulOneClass N] : Coe (M →* N) (M →ₙ* N)

Full source

/-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property. -/
@[to_additive "`AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property."]
instance MonoidHom.coeToMulHom [MulOneClass M] [MulOneClass N] :
  Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩

Monoid Homomorphism as Multiplicative Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, $f$ can be viewed as a multiplicative homomorphism (i.e., a function that preserves multiplication but not necessarily the identity element).

OneHom.coe_mk theorem

[One M] [One N] (f : M → N) (h1) : (OneHom.mk f h1 : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem OneHom.coe_mk [One M] [One N] (f : M → N) (h1) : (OneHom.mk f h1 : M → N) = f := rfl

Underlying Function of Constructed Identity-Preserving Homomorphism Equals Original Function

Informal description

For any function $f \colon M \to N$ between types $M$ and $N$ each equipped with a distinguished element $1$, and any proof $h_1$ that $f$ preserves the identity element (i.e., $f(1) = 1$), the underlying function of the identity-preserving homomorphism constructed from $f$ and $h_1$ is equal to $f$ itself.

OneHom.toFun_eq_coe theorem

[One M] [One N] (f : OneHom M N) : f.toFun = f

Full source

@[to_additive (attr := simp)]
theorem OneHom.toFun_eq_coe [One M] [One N] (f : OneHom M N) : f.toFun = f := rfl

Underlying Function of Identity-Preserving Homomorphism

Informal description

For any identity-preserving homomorphism $f$ between types $M$ and $N$ each equipped with a distinguished element $1$, the underlying function of $f$ is equal to $f$ itself when viewed as a function.

MulHom.coe_mk theorem

[Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem MulHom.coe_mk [Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f := rfl

Coercion of Constructed Multiplicative Homomorphism Equals Original Function

Informal description

For any multiplicative structures $M$ and $N$, and a function $f \colon M \to N$ that preserves multiplication (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the coercion of the multiplicative homomorphism constructed from $f$ and its proof of multiplicativity `hmul` is equal to $f$ itself. In other words, the underlying function of the bundled multiplicative homomorphism `MulHom.mk f hmul` is exactly $f$.

MulHom.toFun_eq_coe theorem

[Mul M] [Mul N] (f : M →ₙ* N) : f.toFun = f

Full source

@[to_additive (attr := simp)]
theorem MulHom.toFun_eq_coe [Mul M] [Mul N] (f : M →ₙ* N) : f.toFun = f := rfl

Underlying Function of Multiplicative Homomorphism Equals Itself

Informal description

For any multiplicative structures $M$ and $N$, and any multiplicative homomorphism $f \colon M \to N$, the underlying function of $f$ is equal to $f$ itself when viewed as a function.

MonoidHom.coe_mk theorem

[MulOneClass M] [MulOneClass N] (f hmul) : (MonoidHom.mk f hmul : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.coe_mk [MulOneClass M] [MulOneClass N] (f hmul) :
    (MonoidHom.mk f hmul : M → N) = f := rfl

Coercion of Constructed Monoid Homomorphism Equals Original Function

Informal description

For any monoids $M$ and $N$, and a function $f \colon M \to N$ that preserves multiplication (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the coercion of the monoid homomorphism constructed from $f$ and its proof of multiplicativity `hmul` is equal to $f$ itself. In other words, the underlying function of the bundled monoid homomorphism `MonoidHom.mk f hmul` is exactly $f$.

MonoidHom.toOneHom_coe theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) : (f.toOneHom : M → N) = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.toOneHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
    (f.toOneHom : M → N) = f := rfl

Underlying Function of Identity-Preserving Homomorphism Equals Original Monoid Homomorphism

Informal description

For any monoids $M$ and $N$, and a monoid homomorphism $f \colon M \to N$, the underlying function of the identity-preserving homomorphism $f.\text{toOneHom}$ is equal to $f$ itself.

MonoidHom.toMulHom_coe theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) : f.toMulHom.toFun = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.toMulHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
    f.toMulHom.toFun = f := rfl

Underlying Function of Multiplicative Homomorphism Equals Monoid Homomorphism

Informal description

For any monoids $M$ and $N$ and a monoid homomorphism $f \colon M \to N$, the underlying function of the multiplicative homomorphism $f.\text{toMulHom}$ is equal to $f$ itself.

MonoidHom.toFun_eq_coe theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) : f.toFun = f

Full source

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

Underlying Function of Monoid Homomorphism Equals Itself

Informal description

For any monoids $M$ and $N$, and a monoid homomorphism $f \colon M \to N$, the underlying function of $f$ (accessed via `f.toFun`) is equal to $f$ itself when viewed as a function.

OneHom.ext theorem

[One M] [One N] ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[to_additive (attr := ext)]
theorem OneHom.ext [One M] [One N] ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

Extensionality of Identity-Preserving Homomorphisms

Informal description

Let $M$ and $N$ be types each equipped with a distinguished element $1$. For any two identity-preserving homomorphisms $f, g \colon M \to N$, if $f(x) = g(x)$ for all $x \in M$, then $f = g$.

MulHom.ext theorem

[Mul M] [Mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[to_additive (attr := ext)]
theorem MulHom.ext [Mul M] [Mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

Extensionality of Non-unital Multiplicative Homomorphisms

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f, g \colon M \to N$ be non-unital multiplicative homomorphisms. If $f(x) = g(x)$ for all $x \in M$, then $f = g$.

MonoidHom.ext theorem

[MulOneClass M] [MulOneClass N] ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[to_additive (attr := ext)]
theorem MonoidHom.ext [MulOneClass M] [MulOneClass N] ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

Extensionality of Monoid Homomorphisms

Informal description

Let $M$ and $N$ be monoids (or groups), and let $f, g \colon M \to N$ be monoid homomorphisms. If $f(x) = g(x)$ for all $x \in M$, then $f = g$.

MonoidHom.mk' definition

(f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G

Full source

/-- Makes a group homomorphism from a proof that the map preserves multiplication. -/
@[to_additive (attr := simps -fullyApplied)
  "Makes an additive group homomorphism from a proof that the map preserves addition."]
def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G where
  toFun := f
  map_mul' := map_mul
  map_one' := by rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]

Group homomorphism from multiplication-preserving function

Informal description

Given a function $ f \colon M \to G $ between groups that preserves multiplication (i.e., $ f(a * b) = f(a) * f(b) $ for all $ a, b \in M $), this definition constructs a group homomorphism from $ M $ to $ G $. The preservation of the identity element is automatically derived from the preservation of multiplication.

OneHom.mk_coe theorem

[One M] [One N] (f : OneHom M N) (h1) : OneHom.mk f h1 = f

Full source

@[to_additive (attr := simp)]
theorem OneHom.mk_coe [One M] [One N] (f : OneHom M N) (h1) : OneHom.mk f h1 = f :=
  OneHom.ext fun _ => rfl

Construction of Identity-Preserving Homomorphism Yields Original Function

Informal description

Let $M$ and $N$ be types each equipped with a distinguished element $1$. Given an identity-preserving homomorphism $f \colon M \to N$ and a proof $h1$ that $f(1) = 1$, the construction $\text{OneHom.mk}(f, h1)$ yields $f$ itself.

MulHom.mk_coe theorem

[Mul M] [Mul N] (f : M →ₙ* N) (hmul) : MulHom.mk f hmul = f

Full source

@[to_additive (attr := simp)]
theorem MulHom.mk_coe [Mul M] [Mul N] (f : M →ₙ* N) (hmul) : MulHom.mk f hmul = f :=
  MulHom.ext fun _ => rfl

Constructor Equality for Non-unital Multiplicative Homomorphisms

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f \colon M \to N$ be a non-unital multiplicative homomorphism. For any proof `hmul` that $f$ preserves multiplication, the construction `MulHom.mk f hmul` is equal to $f$ itself.

MonoidHom.mk_coe theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) (hmul) : MonoidHom.mk f hmul = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.mk_coe [MulOneClass M] [MulOneClass N] (f : M →* N) (hmul) :
    MonoidHom.mk f hmul = f := MonoidHom.ext fun _ => rfl

Constructor Equality for Monoid Homomorphisms

Informal description

Let $M$ and $N$ be monoids (or groups). For any monoid homomorphism $f \colon M \to N$ and any proof `hmul` that $f$ preserves multiplication, the construction $\text{MonoidHom.mk}(f, \text{hmul})$ yields $f$ itself.

OneHom.copy definition

[One M] [One N] (f : OneHom M N) (f' : M → N) (h : f' = f) : OneHom M N

Full source

/-- Copy of a `OneHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive
  "Copy of a `ZeroHom` with a new `toFun` equal to the old one. Useful to fix
  definitional equalities."]
protected def OneHom.copy [One M] [One N] (f : OneHom M N) (f' : M → N) (h : f' = f) :
    OneHom M N where
  toFun := f'
  map_one' := h.symm ▸ f.map_one'

Copy of an identity-preserving homomorphism with a new function

Informal description

Given an identity-preserving homomorphism $f \colon M \to N$ between types with distinguished elements $1$, and a function $f' \colon M \to N$ that is definitionally equal to $f$, the function `OneHom.copy` constructs a new identity-preserving homomorphism with the underlying function $f'$ that preserves the identity element $1$. This is useful for fixing definitional equalities while maintaining the homomorphism structure.

OneHom.coe_copy theorem

{_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) : (f.copy f' h) = f'

Full source

@[to_additive (attr := simp)]
theorem OneHom.coe_copy {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
    (f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Identity-Preserving Homomorphism

Informal description

Let $M$ and $N$ be types equipped with distinguished elements $1$, and let $f \colon M \to N$ be an identity-preserving homomorphism. For any function $f' \colon M \to N$ such that $f' = f$, the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

OneHom.coe_copy_eq theorem

{_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) : f.copy f' h = f

Full source

@[to_additive]
theorem OneHom.coe_copy_eq {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
    f.copy f' h = f :=
  DFunLike.ext' h

Equality of Copied Identity-Preserving Homomorphism with Original

Informal description

Let $M$ and $N$ be types each equipped with a distinguished element $1$, and let $f \colon M \to N$ be an identity-preserving homomorphism. For any function $f' \colon M \to N$ such that $f' = f$, the copied homomorphism $f.copy\ f'\ h$ is equal to $f$.

MulHom.copy definition

[Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = f) : M →ₙ* N

Full source

/-- Copy of a `MulHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive
  "Copy of an `AddHom` with a new `toFun` equal to the old one. Useful to fix
  definitional equalities."]
protected def MulHom.copy [Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
    M →ₙ* N where
  toFun := f'
  map_mul' := h.symm ▸ f.map_mul'

Copy of a non-unital multiplicative homomorphism with a new function

Informal description

Given a non-unital multiplicative homomorphism $f : M \toₙ* N$ between multiplicative structures $M$ and $N$, and a function $f' : M \to N$ that is definitionally equal to $f$, the function `MulHom.copy` constructs a new homomorphism from $f'$ that behaves identically to $f$ with respect to multiplication. This is useful for fixing definitional equalities when working with homomorphisms.

MulHom.coe_copy theorem

{_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) : (f.copy f' h) = f'

Full source

@[to_additive (attr := simp)]
theorem MulHom.coe_copy {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
    (f.copy f' h) = f' :=
  rfl

Coercion of Copied Non-unital Multiplicative Homomorphism Equals Original Function

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f : M \toₙ* N$ be a non-unital multiplicative homomorphism. Given a function $f' : M \to N$ such that $f' = f$, the coercion of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

MulHom.coe_copy_eq theorem

{_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) : f.copy f' h = f

Full source

@[to_additive]
theorem MulHom.coe_copy_eq {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
    f.copy f' h = f :=
  DFunLike.ext' h

Equality of Copied Non-unital Multiplicative Homomorphism with Original

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f : M \toₙ* N$ be a non-unital multiplicative homomorphism. Given a function $f' : M \to N$ such that $f' = f$, the copied homomorphism $f.copy\ f'\ h$ is equal to $f$.

MonoidHom.copy definition

[MulOneClass M] [MulOneClass N] (f : M →* N) (f' : M → N) (h : f' = f) : M →* N

Full source

/-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
@[to_additive
  "Copy of an `AddMonoidHom` with a new `toFun` equal to the old one. Useful to fix
  definitional equalities."]
protected def MonoidHom.copy [MulOneClass M] [MulOneClass N] (f : M →* N) (f' : M → N)
    (h : f' = f) : M →* N :=
  { f.toOneHom.copy f' h, f.toMulHom.copy f' h with }

Copy of a monoid homomorphism with a new function

Informal description

Given a monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, and a function $f' \colon M \to N$ that is definitionally equal to $f$, the function `MonoidHom.copy` constructs a new monoid homomorphism with the underlying function $f'$ that preserves both the multiplicative and identity structures. This is useful for fixing definitional equalities while maintaining the homomorphism structure.

MonoidHom.coe_copy theorem

{_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N) (h : f' = f) : (f.copy f' h) = f'

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.coe_copy {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
    (h : f' = f) : (f.copy f' h) = f' :=
  rfl

Equality of Copied Monoid Homomorphism's Underlying Function

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. Given a function $f' \colon M \to N$ such that $f' = f$, the underlying function of the copied homomorphism $f.\text{copy}\ f'\ h$ is equal to $f'$.

MonoidHom.copy_eq theorem

{_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N) (h : f' = f) : f.copy f' h = f

Full source

@[to_additive]
theorem MonoidHom.copy_eq {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
    (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Monoid Homomorphism Preserves Original

Informal description

For any monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, and any function $f' \colon M \to N$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$.

OneHom.map_one theorem

[One M] [One N] (f : OneHom M N) : f 1 = 1

Full source

@[to_additive]
protected theorem OneHom.map_one [One M] [One N] (f : OneHom M N) : f 1 = 1 :=
  f.map_one'

Identity-preserving homomorphism property: $f(1) = 1$

Informal description

For any identity-preserving homomorphism $f \colon M \to N$ between types $M$ and $N$ each equipped with a distinguished element $1$, we have $f(1) = 1$.

MonoidHom.map_one theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) : f 1 = 1

Full source

/-- If `f` is a monoid homomorphism then `f 1 = 1`. -/
@[to_additive "If `f` is an additive monoid homomorphism then `f 0 = 0`."]
protected theorem MonoidHom.map_one [MulOneClass M] [MulOneClass N] (f : M →* N) : f 1 = 1 :=
  f.map_one'

Monoid Homomorphism Preserves Identity: $f(1) = 1$

Informal description

For any monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, the identity element is preserved, i.e., $f(1) = 1$.

MulHom.map_mul theorem

[Mul M] [Mul N] (f : M →ₙ* N) (a b : M) : f (a * b) = f a * f b

Full source

@[to_additive]
protected theorem MulHom.map_mul [Mul M] [Mul N] (f : M →ₙ* N) (a b : M) : f (a * b) = f a * f b :=
  f.map_mul' a b

Multiplicative Homomorphism Property: $f(a * b) = f(a) * f(b)$

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f : M \toₙ* N$ be a non-unital multiplicative homomorphism. Then for any elements $a, b \in M$, the homomorphism $f$ satisfies $f(a * b) = f(a) * f(b)$.

MonoidHom.map_mul theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) (a b : M) : f (a * b) = f a * f b

Full source

/-- If `f` is a monoid homomorphism then `f (a * b) = f a * f b`. -/
@[to_additive "If `f` is an additive monoid homomorphism then `f (a + b) = f a + f b`."]
protected theorem MonoidHom.map_mul [MulOneClass M] [MulOneClass N] (f : M →* N) (a b : M) :
    f (a * b) = f a * f b := f.map_mul' a b

Monoid Homomorphism Preserves Multiplication: $f(a \cdot b) = f(a) \cdot f(b)$

Informal description

Let $M$ and $N$ be monoids and let $f \colon M \to N$ be a monoid homomorphism. Then for any elements $a, b \in M$, the homomorphism $f$ satisfies $f(a \cdot b) = f(a) \cdot f(b)$.

MonoidHom.map_exists_right_inv theorem

(f : F) {x : M} (hx : ∃ y, x * y = 1) : ∃ y, f x * y = 1

Full source

/-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a right inverse,
then `f x` has a right inverse too. For elements invertible on both sides see `IsUnit.map`. -/
@[to_additive
  "Given an AddMonoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
  a right inverse, then `f x` has a right inverse too."]
theorem map_exists_right_inv (f : F) {x : M} (hx : ∃ y, x * y = 1) : ∃ y, f x * y = 1 :=
  let ⟨y, hy⟩ := hx
  ⟨f y, map_mul_eq_one f hy⟩

Monoid homomorphisms preserve right inverses: $f(x \cdot y = 1) \Rightarrow \exists z, f(x) \cdot z = 1$

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any element $x \in M$ that has a right inverse (i.e., there exists $y \in M$ such that $x \cdot y = 1$), the image $f(x)$ also has a right inverse in $N$ (i.e., there exists $z \in N$ such that $f(x) \cdot z = 1$).

MonoidHom.map_exists_left_inv theorem

(f : F) {x : M} (hx : ∃ y, y * x = 1) : ∃ y, y * f x = 1

Full source

/-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a left inverse,
then `f x` has a left inverse too. For elements invertible on both sides see `IsUnit.map`. -/
@[to_additive
  "Given an AddMonoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
  a left inverse, then `f x` has a left inverse too. For elements invertible on both sides see
  `IsAddUnit.map`."]
theorem map_exists_left_inv (f : F) {x : M} (hx : ∃ y, y * x = 1) : ∃ y, y * f x = 1 :=
  let ⟨y, hy⟩ := hx
  ⟨f y, map_mul_eq_one f hy⟩

Monoid homomorphisms preserve left invertibility: $f(x)$ has a left inverse when $x$ does

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any element $x \in M$ that has a left inverse (i.e., there exists $y \in M$ such that $y * x = 1$), the image $f(x)$ also has a left inverse in $N$ (i.e., there exists $y' \in N$ such that $y' * f(x) = 1$).

OneHom.id definition

(M : Type*) [One M] : OneHom M M

Full source

/-- The identity map from a type with 1 to itself. -/
@[to_additive (attr := simps) "The identity map from a type with zero to itself."]
def OneHom.id (M : Type*) [One M] : OneHom M M where
  toFun x := x
  map_one' := rfl

Identity-preserving homomorphism on a type with one

Informal description

The identity map from a type $M$ with a distinguished element $1$ to itself, which preserves the identity element.

MulHom.id definition

(M : Type*) [Mul M] : M →ₙ* M

Full source

/-- The identity map from a type with multiplication to itself. -/
@[to_additive (attr := simps) "The identity map from a type with addition to itself."]
def MulHom.id (M : Type*) [Mul M] : M →ₙ* M where
  toFun x := x
  map_mul' _ _ := rfl

Identity multiplicative homomorphism

Informal description

The identity map from a multiplicative structure $M$ to itself, which preserves multiplication.

MonoidHom.id definition

(M : Type*) [MulOneClass M] : M →* M

Full source

/-- The identity map from a monoid to itself. -/
@[to_additive (attr := simps) "The identity map from an additive monoid to itself."]
def MonoidHom.id (M : Type*) [MulOneClass M] : M →* M where
  toFun x := x
  map_one' := rfl
  map_mul' _ _ := rfl

Identity monoid homomorphism

Informal description

The identity homomorphism from a monoid $ M $ to itself, which maps every element $ x \in M $ to itself, preserves the multiplicative identity $ 1 $, and preserves multiplication.

OneHom.coe_id theorem

{M : Type*} [One M] : (OneHom.id M : M → M) = _root_.id

Full source

@[to_additive (attr := simp)]
lemma OneHom.coe_id {M : Type*} [One M] : (OneHom.id M : M → M) = _root_.id := rfl

Identity-preserving homomorphism as identity function

Informal description

For any type $M$ equipped with a distinguished element $1$, the underlying function of the identity-preserving homomorphism $\mathrm{id}_M \colon M \to M$ is equal to the identity function on $M$.

MulHom.coe_id theorem

{M : Type*} [Mul M] : (MulHom.id M : M → M) = _root_.id

Full source

@[to_additive (attr := simp)]
lemma MulHom.coe_id {M : Type*} [Mul M] : (MulHom.id M : M → M) = _root_.id := rfl

Identity Multiplicative Homomorphism as Identity Function

Informal description

For any multiplicative structure $M$, the underlying function of the identity multiplicative homomorphism $\text{id}_M \colon M \to M$ is equal to the identity function on $M$.

MonoidHom.coe_id theorem

{M : Type*} [MulOneClass M] : (MonoidHom.id M : M → M) = _root_.id

Full source

@[to_additive (attr := simp)]
lemma MonoidHom.coe_id {M : Type*} [MulOneClass M] : (MonoidHom.id M : M → M) = _root_.id := rfl

Identity Monoid Homomorphism as Identity Function

Informal description

For any monoid $M$, the underlying function of the identity monoid homomorphism $\mathrm{id}_M \colon M \to M$ is equal to the identity function on $M$.

OneHom.comp definition

[One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) : OneHom M P

Full source

/-- Composition of `OneHom`s as a `OneHom`. -/
@[to_additive "Composition of `ZeroHom`s as a `ZeroHom`."]
def OneHom.comp [One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) : OneHom M P where
  toFun := hnp ∘ hmn
  map_one' := by simp

Composition of identity-preserving homomorphisms

Informal description

The composition of two identity-preserving homomorphisms $ hnp \colon N \to P $ and $ hmn \colon M \to N $ is an identity-preserving homomorphism $ M \to P $ defined by $(hnp \circ hmn)(x) = hnp(hmn(x))$ for all $x \in M$, which preserves the identity element $1$.

MulHom.comp definition

[Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P

Full source

/-- Composition of `MulHom`s as a `MulHom`. -/
@[to_additive "Composition of `AddHom`s as an `AddHom`."]
def MulHom.comp [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P where
  toFun := hnp ∘ hmn
  map_mul' x y := by simp

Composition of non-unital multiplicative homomorphisms

Informal description

Given multiplicative structures $M$, $N$, and $P$, the composition of two non-unital multiplicative homomorphisms $hnp : N \toₙ* P$ and $hmn : M \toₙ* N$ is a non-unital multiplicative homomorphism $M \toₙ* P$ defined by $(hnp \circ hmn)(x) = hnp(hmn(x))$ for all $x \in M$.

MonoidHom.comp definition

[MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) : M →* P

Full source

/-- Composition of monoid morphisms as a monoid morphism. -/
@[to_additive "Composition of additive monoid morphisms as an additive monoid morphism."]
def MonoidHom.comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) :
    M →* P where
  toFun := hnp ∘ hmn
  map_one' := by simp
  map_mul' := by simp

Composition of monoid homomorphisms

Informal description

Given monoids $ M $, $ N $, and $ P $, the composition of two monoid homomorphisms $ hnp \colon N \to^* P $ and $ hmn \colon M \to^* N $ is a monoid homomorphism $ M \to^* P $ defined by $ (hnp \circ hmn)(x) = hnp(hmn(x)) $ for all $ x \in M $. This composition preserves the multiplicative identity and the multiplication operation.

OneHom.coe_comp theorem

[One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) : ↑(g.comp f) = g ∘ f

Full source

@[to_additive (attr := simp)]
theorem OneHom.coe_comp [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) :
    ↑(g.comp f) = g ∘ f := rfl

Composition of Identity-Preserving Homomorphisms as Functions

Informal description

For any types $M$, $N$, and $P$ each equipped with a distinguished element $1$, and for any identity-preserving homomorphisms $g \colon N \to P$ and $f \colon M \to N$, the composition $g \circ f$ as functions is equal to the underlying function of the composed homomorphism $g \circ f$ (i.e., $\overline{g \circ f} = g \circ f$).

MulHom.coe_comp theorem

[Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) : ↑(g.comp f) = g ∘ f

Full source

@[to_additive (attr := simp)]
theorem MulHom.coe_comp [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
    ↑(g.comp f) = g ∘ f := rfl

Composition of Non-unital Multiplicative Homomorphisms as Function Composition

Informal description

For multiplicative structures $M$, $N$, and $P$, and non-unital multiplicative homomorphisms $g \colon N \toₙ* P$ and $f \colon M \toₙ* N$, the underlying function of the composition $g \circ f$ is equal to the pointwise composition of the underlying functions, i.e., $\overline{g \circ f} = g \circ f$.

MonoidHom.coe_comp theorem

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

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.coe_comp [MulOneClass M] [MulOneClass N] [MulOneClass P]
    (g : N →* P) (f : M →* N) : ↑(g.comp f) = g ∘ f := rfl

Composition of Monoid Homomorphisms as Function Composition

Informal description

For monoids $M$, $N$, and $P$, and monoid homomorphisms $g \colon N \to^* P$ and $f \colon M \to^* N$, the underlying function of the composition $g \circ f$ is equal to the pointwise composition of the underlying functions, i.e., $\overline{g \circ f} = g \circ f$.

OneHom.comp_apply theorem

[One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) (x : M) : g.comp f x = g (f x)

Full source

@[to_additive]
theorem OneHom.comp_apply [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) (x : M) :
    g.comp f x = g (f x) := rfl

Evaluation of Composition of Identity-Preserving Homomorphisms

Informal description

For types $M$, $N$, and $P$ each equipped with a distinguished element $1$, given identity-preserving homomorphisms $g \colon N \to P$ and $f \colon M \to N$, the composition $g \circ f$ evaluated at any $x \in M$ satisfies $(g \circ f)(x) = g(f(x))$.

MulHom.comp_apply theorem

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

Full source

@[to_additive]
theorem MulHom.comp_apply [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) (x : M) :
    g.comp f x = g (f x) := rfl

Evaluation of Composition of Non-unital Multiplicative Homomorphisms

Informal description

For multiplicative structures $M$, $N$, and $P$, given non-unital multiplicative homomorphisms $g \colon N \toₙ* P$ and $f \colon M \toₙ* N$, the composition $g \circ f$ evaluated at any $x \in M$ satisfies $(g \circ f)(x) = g(f(x))$.

MonoidHom.comp_apply theorem

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

Full source

@[to_additive]
theorem MonoidHom.comp_apply [MulOneClass M] [MulOneClass N] [MulOneClass P]
    (g : N →* P) (f : M →* N) (x : M) : g.comp f x = g (f x) := rfl

Composition of Monoid Homomorphisms Preserves Evaluation

Informal description

For monoids $M$, $N$, and $P$, given monoid homomorphisms $g \colon N \to^* P$ and $f \colon M \to^* N$, the composition $g \circ f$ evaluated at any $x \in M$ satisfies $(g \circ f)(x) = g(f(x))$.

OneHom.comp_assoc theorem

 {Q : Type*} [One M] [One N] [One P] [One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q) :
  (h.comp g).comp f = h.comp (g.comp f)

Full source

/-- Composition of monoid homomorphisms is associative. -/
@[to_additive "Composition of additive monoid homomorphisms is associative."]
theorem OneHom.comp_assoc {Q : Type*} [One M] [One N] [One P] [One Q]
    (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q) :
    (h.comp g).comp f = h.comp (g.comp f) := rfl

Associativity of Composition for Identity-Preserving Homomorphisms

Informal description

For types $M$, $N$, $P$, and $Q$ each equipped with a distinguished element $1$, and given identity-preserving homomorphisms $f \colon M \to N$, $g \colon N \to P$, and $h \colon P \to Q$, the composition of homomorphisms is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

MulHom.comp_assoc theorem

 {Q : Type*} [Mul M] [Mul N] [Mul P] [Mul Q] (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :
  (h.comp g).comp f = h.comp (g.comp f)

Full source

@[to_additive]
theorem MulHom.comp_assoc {Q : Type*} [Mul M] [Mul N] [Mul P] [Mul Q]
    (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) : (h.comp g).comp f = h.comp (g.comp f) := rfl

Associativity of Composition for Non-Unital Multiplicative Homomorphisms

Informal description

For multiplicative structures $M$, $N$, $P$, and $Q$, and given non-unital multiplicative homomorphisms $f \colon M \to N$, $g \colon N \to P$, and $h \colon P \to Q$, the composition of homomorphisms is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

MonoidHom.comp_assoc theorem

 {Q : Type*} [MulOneClass M] [MulOneClass N] [MulOneClass P] [MulOneClass Q] (f : M →* N) (g : N →* P) (h : P →* Q) :
  (h.comp g).comp f = h.comp (g.comp f)

Full source

@[to_additive]
theorem MonoidHom.comp_assoc {Q : Type*} [MulOneClass M] [MulOneClass N] [MulOneClass P]
    [MulOneClass Q] (f : M →* N) (g : N →* P) (h : P →* Q) :
    (h.comp g).comp f = h.comp (g.comp f) := rfl

Associativity of Monoid Homomorphism Composition

Informal description

For monoids $M$, $N$, $P$, and $Q$, and monoid homomorphisms $f \colon M \to N$, $g \colon N \to P$, and $h \colon P \to Q$, the composition of homomorphisms is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

OneHom.cancel_right theorem

 [One M] [One N] [One P] {g₁ g₂ : OneHom N P} {f : OneHom M N} (hf : Function.Surjective f) :
  g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[to_additive]
theorem OneHom.cancel_right [One M] [One N] [One P] {g₁ g₂ : OneHom N P} {f : OneHom M N}
    (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => OneHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

Right Cancellation Property for Identity-Preserving Homomorphisms

Informal description

Let $M$, $N$, and $P$ be types each equipped with a distinguished element $1$. Given two identity-preserving homomorphisms $g_1, g_2 \colon N \to P$ and a surjective identity-preserving homomorphism $f \colon M \to N$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

MulHom.cancel_right theorem

 [Mul M] [Mul N] [Mul P] {g₁ g₂ : N →ₙ* P} {f : M →ₙ* N} (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[to_additive]
theorem MulHom.cancel_right [Mul M] [Mul N] [Mul P] {g₁ g₂ : N →ₙ* P} {f : M →ₙ* N}
    (hf : Function.Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => MulHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

Right Cancellation Property for Non-unital Multiplicative Homomorphisms

Informal description

Let $M$, $N$, and $P$ be multiplicative structures, and let $f \colon M \to N$ be a surjective non-unital multiplicative homomorphism. For any two non-unital multiplicative homomorphisms $g_1, g_2 \colon N \to P$, we have $g_1 \circ f = g_2 \circ f$ if and only if $g_1 = g_2$.

MonoidHom.cancel_right theorem

 [MulOneClass M] [MulOneClass N] [MulOneClass P] {g₁ g₂ : N →* P} {f : M →* N} (hf : Function.Surjective f) :
  g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[to_additive]
theorem MonoidHom.cancel_right [MulOneClass M] [MulOneClass N] [MulOneClass P]
    {g₁ g₂ : N →* P} {f : M →* N} (hf : Function.Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => MonoidHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

Right Cancellation Property for Monoid Homomorphisms under Surjective Maps

Informal description

Let $M$, $N$, and $P$ be monoids (or groups), and let $f \colon M \to N$ be a surjective monoid homomorphism. For any two monoid homomorphisms $g_1, g_2 \colon N \to P$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

OneHom.cancel_left theorem

 [One M] [One N] [One P] {g : OneHom N P} {f₁ f₂ : OneHom M N} (hg : Function.Injective g) :
  g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[to_additive]
theorem OneHom.cancel_left [One M] [One N] [One P] {g : OneHom N P} {f₁ f₂ : OneHom M N}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => OneHom.ext fun x => hg <| by rw [← OneHom.comp_apply, h, OneHom.comp_apply],
    fun h => h ▸ rfl⟩

Left Cancellation Property for Composition of Identity-Preserving Homomorphisms

Informal description

Let $M$, $N$, and $P$ be types each equipped with a distinguished element $1$. Given an injective identity-preserving homomorphism $g \colon N \to P$ and two identity-preserving homomorphisms $f_1, f_2 \colon M \to N$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

MulHom.cancel_left theorem

 [Mul M] [Mul N] [Mul P] {g : N →ₙ* P} {f₁ f₂ : M →ₙ* N} (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[to_additive]
theorem MulHom.cancel_left [Mul M] [Mul N] [Mul P] {g : N →ₙ* P} {f₁ f₂ : M →ₙ* N}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => MulHom.ext fun x => hg <| by rw [← MulHom.comp_apply, h, MulHom.comp_apply],
    fun h => h ▸ rfl⟩

Left Cancellation Property for Composition of Non-unital Multiplicative Homomorphisms

Informal description

Let $M$, $N$, and $P$ be multiplicative structures, and let $g \colon N \to P$ be an injective non-unital multiplicative homomorphism. For any two non-unital multiplicative homomorphisms $f_1, f_2 \colon M \to N$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

MonoidHom.cancel_left theorem

 [MulOneClass M] [MulOneClass N] [MulOneClass P] {g : N →* P} {f₁ f₂ : M →* N} (hg : Function.Injective g) :
  g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[to_additive]
theorem MonoidHom.cancel_left [MulOneClass M] [MulOneClass N] [MulOneClass P]
    {g : N →* P} {f₁ f₂ : M →* N} (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => MonoidHom.ext fun x => hg <| by rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply],
    fun h => h ▸ rfl⟩

Left Cancellation Property for Monoid Homomorphisms

Informal description

Let $M$, $N$, and $P$ be monoids, and let $g \colon N \to^* P$ be an injective monoid homomorphism. For any two monoid homomorphisms $f_1, f_2 \colon M \to^* N$, the composition $g \circ f_1$ equals $g \circ f_2$ if and only if $f_1 = f_2$.

MonoidHom.toOneHom_injective theorem

[MulOneClass M] [MulOneClass N] : Function.Injective (MonoidHom.toOneHom : (M →* N) → OneHom M N)

Full source

@[to_additive]
theorem MonoidHom.toOneHom_injective [MulOneClass M] [MulOneClass N] :
    Function.Injective (MonoidHom.toOneHom : (M →* N) → OneHom M N) :=
  Function.Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Monoid Homomorphism to Identity-Preserving Homomorphism Map

Informal description

For any two monoids $M$ and $N$, the canonical map from the type of monoid homomorphisms $M \to^* N$ to the type of identity-preserving homomorphisms $\text{OneHom}(M, N)$ is injective. In other words, if two monoid homomorphisms $f, g \colon M \to N$ induce the same identity-preserving homomorphism via $\text{MonoidHom.toOneHom}$, then $f = g$.

MonoidHom.toMulHom_injective theorem

[MulOneClass M] [MulOneClass N] : Function.Injective (MonoidHom.toMulHom : (M →* N) → M →ₙ* N)

Full source

@[to_additive]
theorem MonoidHom.toMulHom_injective [MulOneClass M] [MulOneClass N] :
    Function.Injective (MonoidHom.toMulHom : (M →* N) → M →ₙ* N) :=
  Function.Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Monoid Homomorphism to Non-unital Multiplicative Homomorphism Map

Informal description

For any two monoids $M$ and $N$ (with multiplication and identity operations), the canonical map from the type of monoid homomorphisms $M \to^* N$ to the type of non-unital multiplicative homomorphisms $M \toₙ* N$ is injective. That is, if two monoid homomorphisms induce the same non-unital multiplicative homomorphism, then they are equal.

OneHom.comp_id theorem

[One M] [One N] (f : OneHom M N) : f.comp (OneHom.id M) = f

Full source

@[to_additive (attr := simp)]
theorem OneHom.comp_id [One M] [One N] (f : OneHom M N) : f.comp (OneHom.id M) = f :=
  OneHom.ext fun _ => rfl

Identity Law for Composition of Identity-Preserving Homomorphisms

Informal description

For any identity-preserving homomorphism $f \colon M \to N$ between types $M$ and $N$ each equipped with a distinguished element $1$, the composition of $f$ with the identity homomorphism on $M$ is equal to $f$ itself, i.e., $f \circ \text{id}_M = f$.

MulHom.comp_id theorem

[Mul M] [Mul N] (f : M →ₙ* N) : f.comp (MulHom.id M) = f

Full source

@[to_additive (attr := simp)]
theorem MulHom.comp_id [Mul M] [Mul N] (f : M →ₙ* N) : f.comp (MulHom.id M) = f :=
  MulHom.ext fun _ => rfl

Right Identity Property of Non-unital Multiplicative Homomorphism Composition

Informal description

For any multiplicative structures $M$ and $N$, and any non-unital multiplicative homomorphism $f \colon M \to N$, the composition of $f$ with the identity homomorphism on $M$ equals $f$ itself, i.e., $f \circ \text{id}_M = f$.

MonoidHom.comp_id theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) : f.comp (MonoidHom.id M) = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.comp_id [MulOneClass M] [MulOneClass N] (f : M →* N) :
    f.comp (MonoidHom.id M) = f := MonoidHom.ext fun _ => rfl

Right identity law for monoid homomorphism composition

Informal description

For any monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, the composition of $f$ with the identity homomorphism on $M$ equals $f$, i.e., $f \circ \text{id}_M = f$.

OneHom.id_comp theorem

[One M] [One N] (f : OneHom M N) : (OneHom.id N).comp f = f

Full source

@[to_additive (attr := simp)]
theorem OneHom.id_comp [One M] [One N] (f : OneHom M N) : (OneHom.id N).comp f = f :=
  OneHom.ext fun _ => rfl

Identity Homomorphism Composition with Identity Preserves Homomorphism

Informal description

For any identity-preserving homomorphism $f \colon M \to N$ between types $M$ and $N$ each equipped with a distinguished element $1$, the composition of the identity homomorphism on $N$ with $f$ is equal to $f$, i.e., $\text{id}_N \circ f = f$.

MulHom.id_comp theorem

[Mul M] [Mul N] (f : M →ₙ* N) : (MulHom.id N).comp f = f

Full source

@[to_additive (attr := simp)]
theorem MulHom.id_comp [Mul M] [Mul N] (f : M →ₙ* N) : (MulHom.id N).comp f = f :=
  MulHom.ext fun _ => rfl

Identity Homomorphism Acts as Left Identity Under Composition

Informal description

For any multiplicative structures $M$ and $N$, and any non-unital multiplicative homomorphism $f \colon M \to N$, the composition of the identity homomorphism on $N$ with $f$ equals $f$ itself. In other words, $\text{id}_N \circ f = f$.

MonoidHom.id_comp theorem

[MulOneClass M] [MulOneClass N] (f : M →* N) : (MonoidHom.id N).comp f = f

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.id_comp [MulOneClass M] [MulOneClass N] (f : M →* N) :
    (MonoidHom.id N).comp f = f := MonoidHom.ext fun _ => rfl

Identity Monoid Homomorphism is Left Neutral Element for Composition

Informal description

For any monoid homomorphism $f \colon M \to N$ between monoids $M$ and $N$, the composition of the identity homomorphism on $N$ with $f$ is equal to $f$ itself, i.e., $\text{id}_N \circ f = f$.

MonoidHom.map_pow theorem

[Monoid M] [Monoid N] (f : M →* N) (a : M) (n : ℕ) : f (a ^ n) = f a ^ n

Full source

@[to_additive]
protected theorem MonoidHom.map_pow [Monoid M] [Monoid N] (f : M →* N) (a : M) (n : ℕ) :
    f (a ^ n) = f a ^ n := map_pow f a n

Power Preservation under Monoid Homomorphisms: $f(a^n) = f(a)^n$

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. Then for any element $a \in M$ and any natural number $n$, we have $f(a^n) = (f(a))^n$.

MonoidHom.map_zpow' theorem

 [DivInvMonoid M] [DivInvMonoid N] (f : M →* N) (hf : ∀ x, f x⁻¹ = (f x)⁻¹) (a : M) (n : ℤ) : f (a ^ n) = f a ^ n

Full source

@[to_additive]
protected theorem MonoidHom.map_zpow' [DivInvMonoid M] [DivInvMonoid N] (f : M →* N)
    (hf : ∀ x, f x⁻¹ = (f x)⁻¹) (a : M) (n : ℤ) :
    f (a ^ n) = f a ^ n := map_zpow' f hf a n

Integer power preservation under monoid homomorphisms with inverse condition: $f(a^n) = f(a)^n$

Informal description

Let $M$ and $N$ be div-inverse monoids, and let $f \colon M \to N$ be a monoid homomorphism. If $f$ satisfies $f(x^{-1}) = (f(x))^{-1}$ for all $x \in M$, then for any $a \in M$ and any integer $n \in \mathbb{Z}$, we have $f(a^n) = (f(a))^n$.

OneHom.inverse definition

[One M] [One N] (f : OneHom M N) (g : N → M) (h₁ : Function.LeftInverse g f) : OneHom N M

Full source

/-- Makes a `OneHom` inverse from the bijective inverse of a `OneHom` -/
@[to_additive (attr := simps)
  "Make a `ZeroHom` inverse from the bijective inverse of a `ZeroHom`"]
def OneHom.inverse [One M] [One N]
    (f : OneHom M N) (g : N → M)
    (h₁ : Function.LeftInverse g f) :
  OneHom N M :=
  { toFun := g,
    map_one' := by rw [← f.map_one, h₁] }

Inverse of a one-preserving homomorphism

Informal description

Given a one-preserving homomorphism $f \colon M \to N$ between types with distinguished elements $1_M$ and $1_N$, and a function $g \colon N \to M$ that is a left inverse of $f$ (i.e., $g \circ f = \text{id}_M$), the function $g$ can be equipped with a structure of a one-preserving homomorphism from $N$ to $M$. Specifically, $g$ satisfies $g(1_N) = 1_M$.

MulHom.inverse definition

 [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : N →ₙ* M

Full source

/-- Makes a multiplicative inverse from a bijection which preserves multiplication. -/
@[to_additive (attr := simps)
  "Makes an additive inverse from a bijection which preserves addition."]
def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M)
    (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : N →ₙ* M where
  toFun := g
  map_mul' x y :=
    calc
      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
      _ = g (f (g x * g y)) := by rw [f.map_mul]
      _ = g x * g y := h₁ _

Inverse of a multiplicative homomorphism

Informal description

Given two multiplicative structures $M$ and $N$, a non-unital multiplicative homomorphism $f : M \to N$, and a function $g : N \to M$ that is both a left and right inverse of $f$, the function $g$ can be equipped with a multiplicative homomorphism structure from $N$ to $M$. This means $g$ preserves multiplication, i.e., $g(x * y) = g(x) * g(y)$ for all $x, y \in N$.

Function.Surjective.mul_comm theorem

 [Mul M] [Mul N] {f : M →ₙ* N} (is_surj : Function.Surjective f) (is_comm : Std.Commutative (· * · : M → M → M)) :
  Std.Commutative (· * · : N → N → N)

Full source

/-- If `M` and `N` have multiplications, `f : M →ₙ* N` is a surjective multiplicative map,
and `M` is commutative, then `N` is commutative. -/
@[to_additive
"If `M` and `N` have additions, `f : M →ₙ+ N` is a surjective additive map,
and `M` is commutative, then `N` is commutative."]
theorem Function.Surjective.mul_comm [Mul M] [Mul N] {f : M →ₙ* N}
    (is_surj : Function.Surjective f) (is_comm : Std.Commutative (· * · : M → M → M)) :
    Std.Commutative (· * · : N → N → N) where
  comm := fun a b ↦ by
    obtain ⟨a', ha'⟩ := is_surj a
    obtain ⟨b', hb'⟩ := is_surj b
    simp only [← ha', ← hb', ← map_mul]
    rw [is_comm.comm]

Surjective multiplicative homomorphism preserves commutativity

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f \colon M \to N$ be a surjective multiplicative homomorphism. If the multiplication operation on $M$ is commutative, then the multiplication operation on $N$ is also commutative.

MonoidHom.inverse definition

 {A B : Type*} [Monoid A] [Monoid B] (f : A →* B) (g : B → A) (h₁ : Function.LeftInverse g f)
  (h₂ : Function.RightInverse g f) : B →* A

Full source

/-- The inverse of a bijective `MonoidHom` is a `MonoidHom`. -/
@[to_additive (attr := simps)
  "The inverse of a bijective `AddMonoidHom` is an `AddMonoidHom`."]
def MonoidHom.inverse {A B : Type*} [Monoid A] [Monoid B] (f : A →* B) (g : B → A)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : B →* A :=
  { (f : OneHom A B).inverse g h₁,
    (f : A →ₙ* B).inverse g h₁ h₂ with toFun := g }

Inverse of a bijective monoid homomorphism

Informal description

Given two monoids $ A $ and $ B $, a monoid homomorphism $ f \colon A \to B $, and a function $ g \colon B \to A $ that is both a left and right inverse of $ f $, the function $ g $ can be equipped with a monoid homomorphism structure from $ B $ to $ A $. Specifically, $ g $ preserves the multiplicative identity and multiplication, i.e., $ g(1_B) = 1_A $ and $ g(x * y) = g(x) * g(y) $ for all $ x, y \in B $.

Monoid.End definition

Full source

/-- The monoid of endomorphisms. -/
@[to_additive "The monoid of endomorphisms.", to_additive_dont_translate]
protected def End := M →* M

Monoid of endomorphisms

Informal description

The monoid of endomorphisms of a monoid $ M $, consisting of all monoid homomorphisms from $ M $ to itself.

Monoid.End.instFunLike instance

: FunLike (Monoid.End M) M M

Full source

@[to_additive]
instance instFunLike : FunLike (Monoid.End M) M M := MonoidHom.instFunLike

Monoid Endomorphisms as Functions

Informal description

For any monoid $M$, the type of monoid endomorphisms $\text{End}(M)$ can be treated as a function-like type, meaning there is a canonical way to interpret an endomorphism as a function from $M$ to itself.

Monoid.End.instMonoidHomClass instance

: MonoidHomClass (Monoid.End M) M M

Full source

@[to_additive]
instance instMonoidHomClass : MonoidHomClass (Monoid.End M) M M := MonoidHom.instMonoidHomClass

Monoid Endomorphisms as Monoid Homomorphisms

Informal description

For any monoid $M$, the monoid of endomorphisms $\text{End}(M)$ forms a `MonoidHomClass`, meaning that its elements preserve both the multiplicative structure and the identity element of $M$.

Monoid.End.instOne instance

: One (Monoid.End M)

Full source

@[to_additive instOne]
instance instOne : One (Monoid.End M) where one := .id _

Identity Element in the Monoid of Endomorphisms

Informal description

The monoid of endomorphisms $\text{End}(M)$ of a monoid $M$ has a distinguished identity element, given by the identity homomorphism.

Monoid.End.instMul instance

: Mul (Monoid.End M)

Full source

@[to_additive instMul]
instance instMul : Mul (Monoid.End M) where mul := .comp

Monoid of Endomorphisms under Composition

Informal description

The set of monoid endomorphisms on a monoid $M$ forms a multiplicative monoid under composition.

Monoid.End.instMonoid instance

: Monoid (Monoid.End M)

Full source

@[to_additive instMonoid]
instance instMonoid : Monoid (Monoid.End M) where
  mul := MonoidHom.comp
  one := MonoidHom.id M
  mul_assoc _ _ _ := MonoidHom.comp_assoc _ _ _
  mul_one := MonoidHom.comp_id
  one_mul := MonoidHom.id_comp
  npow n f := (npowRec n f).copy f^[n] <| by induction n <;> simp [npowRec, *] <;> rfl
  npow_succ _ _ := DFunLike.coe_injective <| Function.iterate_succ _ _

Monoid Structure on Endomorphisms of a Monoid

Informal description

The set of monoid endomorphisms $\text{End}(M)$ of a monoid $M$ forms a monoid under composition, with the identity homomorphism as the neutral element.

Monoid.End.instInhabited instance

: Inhabited (Monoid.End M)

Full source

@[to_additive]
instance : Inhabited (Monoid.End M) := ⟨1⟩

Inhabitedness of the Monoid of Endomorphisms

Informal description

The monoid of endomorphisms $\text{End}(M)$ of a monoid $M$ is always inhabited, with the identity homomorphism as a distinguished element.

Monoid.End.coe_pow theorem

(f : Monoid.End M) (n : ℕ) : (↑(f ^ n) : M → M) = f^[n]

Full source

@[to_additive (attr := simp, norm_cast) coe_pow]
lemma coe_pow (f : Monoid.End M) (n : ℕ) : (↑(f ^ n) : M → M) = f^[n] := rfl

Iteration of Monoid Endomorphism Corresponds to Exponentiation in Endomorphism Monoid

Informal description

For any monoid endomorphism $f \in \text{End}(M)$ and natural number $n$, the function corresponding to the $n$-th power of $f$ in the endomorphism monoid is equal to the $n$-th iterate of $f$, i.e., $(f^n)(x) = f^[n](x)$ for all $x \in M$.

Monoid.End.coe_one theorem

: ((1 : Monoid.End M) : M → M) = id

Full source

@[to_additive (attr := simp) coe_one]
theorem coe_one : ((1 : Monoid.End M) : M → M) = id := rfl

Identity Endomorphism as Identity Function

Informal description

The identity endomorphism of a monoid $M$, when viewed as a function from $M$ to itself, is equal to the identity function $\text{id}$.

Monoid.End.coe_mul theorem

(f g) : ((f * g : Monoid.End M) : M → M) = f ∘ g

Full source

@[to_additive (attr := simp) coe_mul]
theorem coe_mul (f g) : ((f * g : Monoid.End M) : M → M) = f ∘ g := rfl

Composition of Monoid Endomorphisms Corresponds to Multiplication in Endomorphism Monoid

Informal description

For any monoid $M$ and endomorphisms $f, g \in \text{End}(M)$, the composition of $f$ and $g$ as functions equals the function corresponding to their product in the endomorphism monoid, i.e., $(f * g)(x) = f(g(x))$ for all $x \in M$.

instOneOneHom instance

[One M] [One N] : One (OneHom M N)

Full source

/-- `1` is the homomorphism sending all elements to `1`. -/
@[to_additive "`0` is the homomorphism sending all elements to `0`."]
instance [One M] [One N] : One (OneHom M N) := ⟨⟨fun _ => 1, rfl⟩⟩

Constant One Identity-Preserving Homomorphism

Informal description

For any types $M$ and $N$ each equipped with a distinguished element $1$, there is a constant identity-preserving homomorphism from $M$ to $N$ that sends every element to $1$.

instOneMulHom instance

[Mul M] [MulOneClass N] : One (M →ₙ* N)

Full source

/-- `1` is the multiplicative homomorphism sending all elements to `1`. -/
@[to_additive "`0` is the additive homomorphism sending all elements to `0`"]
instance [Mul M] [MulOneClass N] : One (M →ₙ* N) :=
  ⟨⟨fun _ => 1, fun _ _ => (one_mul 1).symm⟩⟩

Constant One Multiplicative Homomorphism

Informal description

For any multiplicative structure $M$ and any multiplicative monoid $N$, there is a constant multiplicative homomorphism from $M$ to $N$ that sends every element to $1$.

instOneMonoidHom instance

[MulOneClass M] [MulOneClass N] : One (M →* N)

Full source

/-- `1` is the monoid homomorphism sending all elements to `1`. -/
@[to_additive "`0` is the additive monoid homomorphism sending all elements to `0`."]
instance [MulOneClass M] [MulOneClass N] : One (M →* N) :=
  ⟨⟨⟨fun _ => 1, rfl⟩, fun _ _ => (one_mul 1).symm⟩⟩

Constant One Monoid Homomorphism

Informal description

For any monoids $M$ and $N$ (with multiplication and identity elements), there is a constant monoid homomorphism from $M$ to $N$ that sends every element to the identity element $1$ of $N$.

OneHom.one_apply theorem

[One M] [One N] (x : M) : (1 : OneHom M N) x = 1

Full source

@[to_additive (attr := simp)]
theorem OneHom.one_apply [One M] [One N] (x : M) : (1 : OneHom M N) x = 1 := rfl

Constant One Homomorphism Evaluates to One

Informal description

For any types $M$ and $N$ each equipped with a distinguished element $1$, the constant identity-preserving homomorphism $1 \colon \text{OneHom}(M, N)$ satisfies $1(x) = 1$ for all $x \in M$.

MonoidHom.one_apply theorem

[MulOneClass M] [MulOneClass N] (x : M) : (1 : M →* N) x = 1

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.one_apply [MulOneClass M] [MulOneClass N] (x : M) : (1 : M →* N) x = 1 := rfl

Constant Monoid Homomorphism Evaluates to Identity

Informal description

For any monoids $M$ and $N$ (with multiplication and identity elements), the constant monoid homomorphism $1 \colon M \to^* N$ satisfies $1(x) = 1$ for all $x \in M$, where the first $1$ denotes the constant homomorphism and the second $1$ denotes the identity element of $N$.

OneHom.one_comp theorem

[One M] [One N] [One P] (f : OneHom M N) : (1 : OneHom N P).comp f = 1

Full source

@[to_additive (attr := simp)]
theorem OneHom.one_comp [One M] [One N] [One P] (f : OneHom M N) :
    (1 : OneHom N P).comp f = 1 := rfl

Composition with Constant One Homomorphism Yields Constant One Homomorphism

Informal description

For any types $M$, $N$, and $P$ each equipped with a distinguished element $1$, and for any identity-preserving homomorphism $f \colon M \to N$, the composition of the constant one homomorphism $1 \colon N \to P$ with $f$ equals the constant one homomorphism $1 \colon M \to P$. That is, $1 \circ f = 1$.

OneHom.comp_one theorem

[One M] [One N] [One P] (f : OneHom N P) : f.comp (1 : OneHom M N) = 1

Full source

@[to_additive (attr := simp)]
theorem OneHom.comp_one [One M] [One N] [One P] (f : OneHom N P) : f.comp (1 : OneHom M N) = 1 := by
  ext
  simp only [OneHom.map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]

Composition with Constant One Homomorphism Yields Constant One Homomorphism

Informal description

For any types $M$, $N$, and $P$ each equipped with a distinguished element $1$, and for any identity-preserving homomorphism $f \colon N \to P$, the composition of $f$ with the constant one homomorphism $1 \colon M \to N$ equals the constant one homomorphism $1 \colon M \to P$. That is, $f \circ 1 = 1$.

instInhabitedOneHom instance

[One M] [One N] : Inhabited (OneHom M N)

Full source

@[to_additive]
instance [One M] [One N] : Inhabited (OneHom M N) := ⟨1⟩

Inhabited Type of Identity-Preserving Homomorphisms

Informal description

For any types $M$ and $N$ each equipped with a distinguished element $1$, the type of identity-preserving homomorphisms from $M$ to $N$ is inhabited.

instInhabitedMulHom instance

[Mul M] [MulOneClass N] : Inhabited (M →ₙ* N)

Full source

@[to_additive]
instance [Mul M] [MulOneClass N] : Inhabited (M →ₙ* N) := ⟨1⟩

Inhabited Type of Non-Unital Multiplicative Homomorphisms

Informal description

For any multiplicative structure $M$ and any multiplicative monoid $N$, the type of multiplicative homomorphisms $M \to_{\text{ₙ}*} N$ is inhabited.

instInhabitedMonoidHom instance

[MulOneClass M] [MulOneClass N] : Inhabited (M →* N)

Full source

@[to_additive]
instance [MulOneClass M] [MulOneClass N] : Inhabited (M →* N) := ⟨1⟩

Inhabited Type of Monoid Homomorphisms

Informal description

For any monoids $M$ and $N$ (with multiplication and identity elements), the type of monoid homomorphisms from $M$ to $N$ is inhabited.

MonoidHom.one_comp theorem

[MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) : (1 : N →* P).comp f = 1

Full source

@[to_additive (attr := simp)]
theorem one_comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) :
    (1 : N →* P).comp f = 1 := rfl

Composition with Constant One Homomorphism Yields Constant One Homomorphism

Informal description

Let $M$, $N$, and $P$ be monoids (with multiplication and identity elements). For any monoid homomorphism $f \colon M \to N$, the composition of the constant one homomorphism $1 \colon N \to P$ with $f$ equals the constant one homomorphism $1 \colon M \to P$. In other words, $(1 \circ f)(x) = 1$ for all $x \in M$.

MonoidHom.comp_one theorem

[MulOneClass M] [MulOneClass N] [MulOneClass P] (f : N →* P) : f.comp (1 : M →* N) = 1

Full source

@[to_additive (attr := simp)]
theorem comp_one [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : N →* P) :
    f.comp (1 : M →* N) = 1 := by
  ext
  simp only [map_one, coe_comp, Function.comp_apply, one_apply]

Composition with Constant One Homomorphism Yields Constant One Homomorphism

Informal description

Let $M$, $N$, and $P$ be monoids (with multiplication and identity elements). For any monoid homomorphism $f \colon N \to P$, the composition of $f$ with the constant one homomorphism $1 \colon M \to N$ equals the constant one homomorphism $1 \colon M \to P$. In other words, $(f \circ 1)(x) = 1$ for all $x \in M$.

MonoidHom.map_inv theorem

[Group α] [DivisionMonoid β] (f : α →* β) (a : α) : f a⁻¹ = (f a)⁻¹

Full source

/-- Group homomorphisms preserve inverse. -/
@[to_additive "Additive group homomorphisms preserve negation."]
protected theorem map_inv [Group α] [DivisionMonoid β] (f : α →* β) (a : α) : f a⁻¹ = (f a)⁻¹ :=
  map_inv f _

Monoid homomorphisms preserve inverses: $f(a^{-1}) = (f(a))^{-1}$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any element $a \in G$, the image of the inverse $f(a^{-1})$ is equal to the inverse of the image $(f(a))^{-1}$.

MonoidHom.map_zpow theorem

[Group α] [DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ) : f (g ^ n) = f g ^ n

Full source

/-- Group homomorphisms preserve integer power. -/
@[to_additive "Additive group homomorphisms preserve integer scaling."]
protected theorem map_zpow [Group α] [DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ) :
    f (g ^ n) = f g ^ n := map_zpow f g n

Monoid homomorphisms preserve integer powers: $f(g^n) = f(g)^n$

Informal description

Let $G$ be a group and $H$ be a division monoid. For any monoid homomorphism $f \colon G \to H$ and any element $g \in G$, the image of $g^n$ under $f$ equals the $n$-th power of $f(g)$ for all integers $n$, i.e., $f(g^n) = (f(g))^n$.

MonoidHom.map_div theorem

[Group α] [DivisionMonoid β] (f : α →* β) (g h : α) : f (g / h) = f g / f h

Full source

/-- Group homomorphisms preserve division. -/
@[to_additive "Additive group homomorphisms preserve subtraction."]
protected theorem map_div [Group α] [DivisionMonoid β] (f : α →* β) (g h : α) :
    f (g / h) = f g / f h := map_div f g h

Monoid homomorphisms preserve division: $f(g / h) = f(g) / f(h)$

Informal description

Let $\alpha$ be a group and $\beta$ be a division monoid. For any monoid homomorphism $f \colon \alpha \to \beta$ and any elements $g, h \in \alpha$, the homomorphism $f$ preserves division, i.e., $f(g / h) = f(g) / f(h)$.

MonoidHom.map_mul_inv theorem

[Group α] [DivisionMonoid β] (f : α →* β) (g h : α) : f (g * h⁻¹) = f g * (f h)⁻¹

Full source

/-- Group homomorphisms preserve division. -/
@[to_additive "Additive group homomorphisms preserve subtraction."]
protected theorem map_mul_inv [Group α] [DivisionMonoid β] (f : α →* β) (g h : α) :
    f (g * h⁻¹) = f g * (f h)⁻¹ := by simp

Monoid homomorphism preserves multiplication and inversion: $f(g * h^{-1}) = f(g) * f(h)^{-1}$

Informal description

Let $\alpha$ be a group and $\beta$ be a division monoid. For any monoid homomorphism $f \colon \alpha \to \beta$ and any elements $g, h \in \alpha$, the homomorphism $f$ satisfies $f(g * h^{-1}) = f(g) * (f(h))^{-1}$.

iterate_map_mul theorem

 {M F : Type*} [Mul M] [FunLike F M M] [MulHomClass F M M] (f : F) (n : ℕ) (x y : M) : f^[n] (x * y) = f^[n] x * f^[n] y

Full source

@[to_additive (attr := simp)]
lemma iterate_map_mul {M F : Type*} [Mul M] [FunLike F M M] [MulHomClass F M M]
    (f : F) (n : ℕ) (x y : M) :
    f^[n] (x * y) = f^[n] x * f^[n] y :=
  Function.Semiconj₂.iterate (map_mul f) n x y

Iterated Homomorphism Preserves Multiplication: $f^n(x \cdot y) = f^n(x) \cdot f^n(y)$

Informal description

Let $M$ be a multiplicative structure and $F$ a type of homomorphisms from $M$ to itself that preserve multiplication. For any homomorphism $f \colon M \to M$ in $F$ and any natural number $n$, the $n$-th iterate of $f$ preserves multiplication, i.e., $f^n(x \cdot y) = f^n(x) \cdot f^n(y)$ for all $x, y \in M$.

iterate_map_one theorem

{M F : Type*} [One M] [FunLike F M M] [OneHomClass F M M] (f : F) (n : ℕ) : f^[n] 1 = 1

Full source

@[to_additive (attr := simp)]
lemma iterate_map_one {M F : Type*} [One M] [FunLike F M M] [OneHomClass F M M]
    (f : F) (n : ℕ) :
    f^[n] 1 = 1 :=
  iterate_fixed (map_one f) n

Iterated Homomorphism Preserves Identity: $f^{[n]}(1) = 1$

Informal description

For any type $M$ with a distinguished element $1$, any type $F$ of homomorphisms preserving $1$ (i.e., $F$ is a `OneHomClass`), and any homomorphism $f \colon F$, the $n$-th iterate of $f$ applied to $1$ equals $1$, i.e., $f^{[n]}(1) = 1$ for all natural numbers $n$.

iterate_map_inv theorem

 {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) : f^[n] x⁻¹ = (f^[n] x)⁻¹

Full source

@[to_additive (attr := simp)]
lemma iterate_map_inv {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M]
    (f : F) (n : ℕ) (x : M) :
    f^[n] x⁻¹ = (f^[n] x)⁻¹ :=
  Commute.iterate_left (map_inv f) n x

Iterated Monoid Homomorphism Preserves Inverses: $f^{[n]}(x^{-1}) = (f^{[n]}(x))^{-1}$

Informal description

Let $M$ be a group and $F$ a type of homomorphisms from $M$ to itself that preserve the monoid structure. For any homomorphism $f \colon M \to M$ in $F$, any natural number $n$, and any element $x \in M$, the $n$-th iterate of $f$ applied to the inverse $x^{-1}$ equals the inverse of the $n$-th iterate of $f$ applied to $x$, i.e., $$ f^{[n]}(x^{-1}) = (f^{[n]}(x))^{-1}. $$

iterate_map_div theorem

 {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x y : M) :
  f^[n] (x / y) = f^[n] x / f^[n] y

Full source

@[to_additive (attr := simp)]
lemma iterate_map_div {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M]
    (f : F) (n : ℕ) (x y : M) :
    f^[n] (x / y) = f^[n] x / f^[n] y :=
  Semiconj₂.iterate (map_div f) n x y

Iterated Monoid Homomorphism Preserves Division: $f^{[n]}(x / y) = f^{[n]}(x) / f^{[n]}(y)$

Informal description

Let $M$ be a group and $F$ a type of homomorphisms from $M$ to itself that preserve the monoid structure. For any homomorphism $f \colon M \to M$ in $F$, any natural number $n$, and any elements $x, y \in M$, the $n$-th iterate of $f$ preserves division, i.e., $$ f^{[n]}(x / y) = f^{[n]}(x) / f^{[n]}(y). $$

iterate_map_pow theorem

 {M F : Type*} [Monoid M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (k : ℕ) :
  f^[n] (x ^ k) = f^[n] x ^ k

Full source

@[to_additive (attr := simp)]
lemma iterate_map_pow {M F : Type*} [Monoid M] [FunLike F M M] [MonoidHomClass F M M]
    (f : F) (n : ℕ) (x : M) (k : ℕ) :
    f^[n] (x ^ k) = f^[n] x ^ k :=
  Commute.iterate_left (map_pow f · k) n x

Iterated Monoid Homomorphism Preserves Powers: $f^{[n]}(x^k) = (f^{[n]}(x))^k$

Informal description

Let $M$ be a monoid and $F$ a type of homomorphisms from $M$ to itself that preserve the monoid structure. For any homomorphism $f \in F$, any natural number $n$, any element $x \in M$, and any natural number $k$, the $n$-th iterate of $f$ applied to $x^k$ equals the $k$-th power of the $n$-th iterate of $f$ applied to $x$, i.e., $$ f^{[n]}(x^k) = (f^{[n]}(x))^k. $$

iterate_map_zpow theorem

 {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (k : ℤ) :
  f^[n] (x ^ k) = f^[n] x ^ k

Full source

@[to_additive (attr := simp)]
lemma iterate_map_zpow {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M]
    (f : F) (n : ℕ) (x : M) (k : ℤ) :
    f^[n] (x ^ k) = f^[n] x ^ k :=
  Commute.iterate_left (map_zpow f · k) n x

Iterated Monoid Homomorphism Preserves Integer Powers: $f^{[n]}(x^k) = (f^{[n]}(x))^k$

Informal description

Let $M$ be a group and $F$ a type of homomorphisms from $M$ to itself that preserve the monoid structure. For any homomorphism $f \colon M \to M$ in $F$, any natural number $n$, and any element $x \in M$, the $n$-th iterate of $f$ preserves integer powers, i.e., $$ f^{[n]}(x^k) = (f^{[n]}(x))^k $$ for any integer $k$.

Mathlib.Algebra.Group.Hom.Defs

Notations

Implementation notes

Tags