Documentation

Mathlib.Algebra.Group.Nat.Hom

Extensionality of monoid homs from ℕ #

source
theorem ext_nat' {A : Type u_3} {F : Type u_5} [FunLike F ℕ A] [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) :
f = g
source
theorem AddMonoidHom.ext_nat {A : Type u_3} [AddMonoid A] {f g : ℕ →+ A} :
f 1 = g 1 → f = g
source
def multiplesHom (M : Type u_2) [AddMonoid M] :
M ≃ (ℕ →+ M)

Additive homomorphisms from ℕ are defined by the image of 1.

Equations
  • multiplesHom M = { toFun := fun (x : M) => { toFun := fun (n : ℕ) => n • x, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun (f : ℕ →+ M) => f 1, left_inv := ⋯, right_inv := ⋯ }
Instances For
    source
    @[simp]
    theorem multiplesHom_apply {M : Type u_2} [AddMonoid M] (x : M) (n : ℕ) :
    ((multiplesHom M) x) n = n • x
    source
    @[simp]
    theorem multiplesHom_symm_apply {M : Type u_2} [AddMonoid M] (f : ℕ →+ M) :
    (multiplesHom M).symm f = f 1
    source
    theorem AddMonoidHom.apply_nat {M : Type u_2} [AddMonoid M] (f : ℕ →+ M) (n : ℕ) :
    f n = n • f 1
    source
    def powersHom (M : Type u_2) [Monoid M] :
    M ≃ (Multiplicative ℕ →* M)

    Monoid homomorphisms from Multiplicative ℕ are defined by the image of Multiplicative.ofAdd 1.

    Equations
    Instances For
      source
      @[simp]
      theorem powersHom_apply {M : Type u_2} [Monoid M] (x : M) (n : Multiplicative ℕ) :
      ((powersHom M) x) n = x ^ Multiplicative.toAdd n
      source
      @[simp]
      theorem powersHom_symm_apply {M : Type u_2} [Monoid M] (f : Multiplicative ℕ →* M) :
      (powersHom M).symm f = f (Multiplicative.ofAdd 1)
      source
      theorem MonoidHom.apply_mnat {M : Type u_2} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) :
      f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
      source
      theorem MonoidHom.ext_mnat {M : Type u_2} [Monoid M] ⦃f g : Multiplicative ℕ →* M⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
      f = g
      source
      def multiplesAddHom (M : Type u_2) [AddCommMonoid M] :
      M ≃+ (ℕ →+ M)

      If M is commutative, multiplesHom is an additive equivalence.

      Equations
      Instances For
        source
        @[simp]
        theorem multiplesAddHom_apply {M : Type u_2} [AddCommMonoid M] (x : M) (n : ℕ) :
        ((multiplesAddHom M) x) n = n • x
        source
        @[simp]
        theorem multiplesAddHom_symm_apply {M : Type u_2} [AddCommMonoid M] (f : ℕ →+ M) :
        (multiplesAddHom M).symm f = f 1
        source
        def powersMulHom (M : Type u_2) [CommMonoid M] :
        M ≃* (Multiplicative ℕ →* M)

        If M is commutative, powersHom is a multiplicative equivalence.

        Equations
        Instances For
          source
          @[simp]
          theorem powersMulHom_apply {M : Type u_2} [CommMonoid M] (x : M) (n : Multiplicative ℕ) :
          ((powersMulHom M) x) n = x ^ Multiplicative.toAdd n
          source
          @[simp]
          theorem powersMulHom_symm_apply {M : Type u_2} [CommMonoid M] (f : Multiplicative ℕ →* M) :
          (powersMulHom M).symm f = f (Multiplicative.ofAdd 1)