Mathlib.Algebra.Group.Nat.Hom

ext_nat' theorem

[AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g

Full source

lemma ext_nat' [AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
  DFunLike.ext f g <| by
    intro n
    induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn =>
      simp [h, ihn]

Extensionality of Natural Number Additive Monoid Homomorphisms via Value at One

Informal description

Let $A$ be an additive monoid and $F$ be a type of additive monoid homomorphisms from $\mathbb{N}$ to $A$. For any two homomorphisms $f, g \in F$, if $f(1) = g(1)$, then $f = g$.

AddMonoidHom.ext_nat theorem

[AddZeroClass A] {f g : ℕ →+ A} : f 1 = g 1 → f = g

Full source

@[ext]
lemma AddMonoidHom.ext_nat [AddZeroClass A] {f g : ℕℕ →+ A} : f 1 = g 1 → f = g :=
  ext_nat' f g

Extensionality of Additive Monoid Homomorphisms from $\mathbb{N}$ via Value at One

Informal description

Let $A$ be an additive monoid and $f, g \colon \mathbb{N} \to A$ be additive monoid homomorphisms. If $f(1) = g(1)$, then $f = g$.

multiplesHom definition

: M ≃ (ℕ →+ M)

Full source

/-- Additive homomorphisms from `ℕ` are defined by the image of `1`. -/
def multiplesHom : M ≃ (ℕ →+ M) where
  toFun x :=
  { toFun := fun n ↦ n • x
    map_zero' := zero_nsmul x
    map_add' := fun _ _ ↦ add_nsmul _ _ _ }
  invFun f := f 1
  left_inv := one_nsmul
  right_inv f := AddMonoidHom.ext_nat <| one_nsmul (f 1)

Natural Number Multiples Homomorphism Equivalence

Informal description

The equivalence `multiplesHom` establishes a bijection between elements of an additive monoid `M` and additive monoid homomorphisms from `ℕ` to `M`. Specifically: - The forward direction maps an element `x ∈ M` to the homomorphism `n ↦ n • x` (where `•` denotes scalar multiplication) - The inverse direction maps a homomorphism `f : ℕ →+ M` to its value at `1`, i.e., `f(1)` This bijection satisfies: 1. For any `x ∈ M`, applying the inverse to the forward map gives back `x` (`left_inv`) 2. For any homomorphism `f`, applying the forward map to `f(1)` recovers `f` (`right_inv`)

multiplesHom_apply theorem

(x : M) (n : ℕ) : multiplesHom M x n = n • x

Full source

@[simp] lemma multiplesHom_apply (x : M) (n : ℕ) : multiplesHom M x n = n • x := rfl

Evaluation of Natural Number Multiples Homomorphism: $\text{multiplesHom}_M(x)(n) = n \cdot x$

Informal description

For any element $x$ in an additive monoid $M$ and any natural number $n$, the additive monoid homomorphism `multiplesHom M x` evaluated at $n$ equals $n$ times $x$, i.e., $\text{multiplesHom}_M(x)(n) = n \cdot x$.

multiplesHom_symm_apply theorem

(f : ℕ →+ M) : (multiplesHom M).symm f = f 1

Full source

lemma multiplesHom_symm_apply (f : ℕℕ →+ M) : (multiplesHom M).symm f = f 1 := rfl

Inverse of Multiples Homomorphism Evaluates at One: $(\text{multiplesHom}_M)^{-1}(f) = f(1)$

Informal description

For any additive monoid homomorphism $f \colon \mathbb{N} \to M$, the inverse of the `multiplesHom` equivalence evaluated at $f$ is equal to $f(1)$, i.e., $(\text{multiplesHom}_M)^{-1}(f) = f(1)$.

AddMonoidHom.apply_nat theorem

(f : ℕ →+ M) (n : ℕ) : f n = n • f 1

Full source

lemma AddMonoidHom.apply_nat (f : ℕℕ →+ M) (n : ℕ) : f n = n • f 1 := by
  rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]

Additive Monoid Homomorphism Evaluation on Natural Numbers: $f(n) = n \cdot f(1)$

Informal description

For any additive monoid homomorphism $f \colon \mathbb{N} \to M$ and any natural number $n$, the value of $f$ at $n$ is equal to $n$ times the value of $f$ at $1$, i.e., $f(n) = n \cdot f(1)$.

powersHom definition

: M ≃ (Multiplicative ℕ →* M)

Full source

/-- Monoid homomorphisms from `Multiplicative ℕ` are defined by the image
of `Multiplicative.ofAdd 1`. -/
@[to_additive existing]
def powersHom : M ≃ (Multiplicative ℕ →* M) :=
  Additive.ofMul.trans <| (multiplesHom _).trans <| AddMonoidHom.toMultiplicative''

Natural Powers Homomorphism Equivalence

Informal description

The equivalence `powersHom` establishes a bijection between elements of a monoid `M` and monoid homomorphisms from the multiplicative monoid of natural numbers `Multiplicative ℕ` to `M`. Specifically: - The forward direction maps an element `x ∈ M` to the homomorphism `n ↦ x^(n.toAdd)` (where `n.toAdd` converts from multiplicative to additive notation) - The inverse direction maps a homomorphism `f : Multiplicative ℕ →* M` to its value at `Multiplicative.ofAdd 1` (i.e., `f(1)` in multiplicative notation) This bijection satisfies: 1. For any `x ∈ M`, applying the inverse to the forward map gives back `x` 2. For any homomorphism `f`, applying the forward map to `f(1)` recovers `f`

powersHom_apply theorem

(x : M) (n : Multiplicative ℕ) : powersHom M x n = x ^ n.toAdd

Full source

@[to_additive existing (attr := simp)]
lemma powersHom_apply (x : M) (n : Multiplicative ℕ) :
    powersHom M x n = x ^ n.toAdd := rfl

Evaluation of Natural Powers Homomorphism: $\text{powersHom}_M(x)(n) = x^{n_{\text{add}}}$

Informal description

For any element $x$ in a monoid $M$ and any element $n$ in the multiplicative monoid of natural numbers $\mathbb{N}$, the evaluation of the homomorphism `powersHom M x` at $n$ equals $x$ raised to the power of the additive counterpart of $n$, i.e., $\text{powersHom}_M(x)(n) = x^{n_{\text{add}}}$.

powersHom_symm_apply theorem

(f : Multiplicative ℕ →* M) : (powersHom M).symm f = f (Multiplicative.ofAdd 1)

Full source

@[to_additive existing (attr := simp)]
lemma powersHom_symm_apply (f : MultiplicativeMultiplicative ℕ →* M) :
    (powersHom M).symm f = f (Multiplicative.ofAdd 1) := rfl

Inverse of Powers Homomorphism Evaluates at Generator

Informal description

For any monoid homomorphism $f \colon \mathbb{N}^\times \to M$ (where $\mathbb{N}^\times$ denotes the multiplicative monoid of natural numbers), the inverse of the `powersHom` equivalence maps $f$ to its value at the multiplicative generator $1$, i.e., $(powersHom\ M)^{-1}(f) = f(1)$.

MonoidHom.apply_mnat theorem

(f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) : f n = f (Multiplicative.ofAdd 1) ^ n.toAdd

Full source

@[to_additive existing AddMonoidHom.apply_nat]
lemma MonoidHom.apply_mnat (f : MultiplicativeMultiplicative ℕ →* M) (n : Multiplicative ℕ) :
    f n = f (Multiplicative.ofAdd 1) ^ n.toAdd := by
  rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]

Evaluation of Monoid Homomorphisms from $\mathbb{N}^\times$: $f(n) = f(1)^n$

Informal description

For any monoid homomorphism $f \colon \mathbb{N}^\times \to M$ from the multiplicative monoid of natural numbers to a monoid $M$, and for any $n \in \mathbb{N}^\times$, the value of $f$ at $n$ is equal to the value of $f$ at the generator $1$ raised to the power of the additive counterpart of $n$, i.e., $f(n) = f(1)^{n_{\text{add}}}$.

MonoidHom.ext_mnat theorem

⦃f g : Multiplicative ℕ →* M⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

Full source

@[to_additive existing (attr := ext) AddMonoidHom.ext_nat]
lemma MonoidHom.ext_mnat ⦃f g : MultiplicativeMultiplicative ℕ →* M⦄
    (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g :=
  MonoidHom.ext fun n ↦ by rw [f.apply_mnat, g.apply_mnat, h]

Extensionality of Monoid Homomorphisms from $\mathbb{N}^\times$ via Generator Evaluation

Informal description

Let $M$ be a monoid and let $f, g \colon \mathbb{N}^\times \to M$ be monoid homomorphisms from the multiplicative monoid of natural numbers to $M$. If $f(1) = g(1)$, then $f = g$.

multiplesAddHom definition

: M ≃+ (ℕ →+ M)

Full source

/-- If `M` is commutative, `multiplesHom` is an additive equivalence. -/
def multiplesAddHom : M ≃+ (ℕ →+ M) where
  __ := multiplesHom M
  map_add' a b := AddMonoidHom.ext fun n ↦ by simp [nsmul_add]

Additive equivalence between elements and natural number multiples homomorphisms

Informal description

The additive equivalence `multiplesAddHom` establishes a bijection between elements of an additive monoid `M` and additive monoid homomorphisms from `ℕ` to `M`. Specifically: - The forward direction maps an element `x ∈ M` to the homomorphism `n ↦ n • x` (where `•` denotes scalar multiplication) - The inverse direction maps a homomorphism `f : ℕ →+ M` to its value at `1`, i.e., `f(1)` This bijection preserves addition and satisfies: 1. For any `x ∈ M`, applying the inverse to the forward map gives back `x` 2. For any homomorphism `f`, applying the forward map to `f(1)` recovers `f`

multiplesAddHom_apply theorem

(x : M) (n : ℕ) : multiplesAddHom M x n = n • x

Full source

@[simp] lemma multiplesAddHom_apply (x : M) (n : ℕ) : multiplesAddHom M x n = n • x := rfl

Evaluation of natural number multiples homomorphism: $\text{multiplesAddHom}_M(x)(n) = n \cdot x$

Informal description

For any additive monoid $M$, element $x \in M$, and natural number $n \in \mathbb{N}$, the additive monoid homomorphism `multiplesAddHom M x` evaluated at $n$ equals the $n$-th multiple of $x$, i.e., $n \cdot x$.

multiplesAddHom_symm_apply theorem

(f : ℕ →+ M) : (multiplesAddHom M).symm f = f 1

Full source

@[simp] lemma multiplesAddHom_symm_apply (f : ℕℕ →+ M) : (multiplesAddHom M).symm f = f 1 := rfl

Inverse of Multiples Homomorphism Evaluates at One

Informal description

For any additive monoid homomorphism $f \colon \mathbb{N} \to M$, the inverse of the additive equivalence `multiplesAddHom` maps $f$ to its value at $1$, i.e., $(\text{multiplesAddHom}\, M)^{-1}(f) = f(1)$.

powersMulHom definition

: M ≃* (Multiplicative ℕ →* M)

Full source

/-- If `M` is commutative, `powersHom` is a multiplicative equivalence. -/
@[to_additive existing]
def powersMulHom : M ≃* (Multiplicative ℕ →* M) where
  __ := powersHom M
  map_mul' a b := MonoidHom.ext fun n ↦ by simp [mul_pow]

Natural Powers Homomorphism Equivalence

Informal description

The multiplicative equivalence `powersMulHom` establishes a bijection between elements of a monoid `M` and monoid homomorphisms from the multiplicative monoid of natural numbers `Multiplicative ℕ` to `M`. Specifically: - The forward direction maps an element `x ∈ M` to the homomorphism `n ↦ x^(n.toAdd)` (where `n.toAdd` converts from multiplicative to additive notation) - The inverse direction maps a homomorphism `f : Multiplicative ℕ →* M` to its value at `Multiplicative.ofAdd 1` (i.e., `f(1)` in multiplicative notation) This bijection satisfies: 1. For any `x ∈ M`, applying the inverse to the forward map gives back `x` 2. For any homomorphism `f`, applying the forward map to `f(1)` recovers `f`

powersMulHom_apply theorem

(x : M) (n : Multiplicative ℕ) : powersMulHom M x n = x ^ n.toAdd

Full source

@[to_additive existing (attr := simp)]
lemma powersMulHom_apply (x : M) (n : Multiplicative ℕ) : powersMulHom M x n = x ^ n.toAdd := rfl

Evaluation of Powers Homomorphism: $\text{powersMulHom}(x)(n) = x^{n.\text{toAdd}}$

Informal description

For any element $x$ in a monoid $M$ and any element $n$ of the multiplicative monoid of natural numbers $\mathbb{N}^\times$, the evaluation of the monoid homomorphism $\text{powersMulHom}(x)$ at $n$ is equal to $x$ raised to the power of the additive counterpart of $n$, i.e., $\text{powersMulHom}(x)(n) = x^{n.\text{toAdd}}$.

powersMulHom_symm_apply theorem

(f : Multiplicative ℕ →* M) : (powersMulHom M).symm f = f (ofAdd 1)

Full source

@[to_additive existing (attr := simp)]
lemma powersMulHom_symm_apply (f : MultiplicativeMultiplicative ℕ →* M) : (powersMulHom M).symm f = f (ofAdd 1) :=
  rfl

Inverse of Powers Homomorphism Equivalence Evaluates at Generator

Informal description

For any monoid homomorphism $f \colon \mathbb{N}^\times \to M$ from the multiplicative monoid of natural numbers to a monoid $M$, the inverse of the `powersMulHom` equivalence evaluated at $f$ is equal to $f$ evaluated at the multiplicative generator $1$, i.e., $(powersMulHom M)^{-1}(f) = f(1)$.