Homomorphisms out of ℤ/Nℤ and (ℤ/Nℤ)²

For N ≠ 0, a homomorphism ℤ/Nℤ →* G to a group G is determined by the image of 1, which is an element of G killed by N, and every such element arises: ZMod.lift descends its powers to ℤ/Nℤ. Likewise, for a commutative group G, a homomorphism (ℤ/Nℤ)² →* G is determined by the pair of images of (1, 0) and (0, 1), both killed by N. The groups ℤ/Nℤ and (ℤ/Nℤ)² are written multiplicatively, as Multiplicative (ZMod N) and Multiplicative (ZMod N × ZMod N).

Main definitions

• TauCeti.zmodMonoidHomEquiv G: the homomorphisms ℤ/Nℤ →* G are the elements of G killed by N.
• TauCeti.zmodProdMonoidHomEquiv G: the homomorphisms (ℤ/Nℤ)² →* G are the pairs of elements of G killed by N.

Main results

• Multiplicative.mem_zpowers_ofAdd_one: the element 1 generates ℤ/Nℤ.
• TauCeti.zmodMonoidHomEquiv_symm_apply and TauCeti.zmodProdMonoidHomEquiv_symm_apply: the homomorphism of g sends a to g ^ a.val, and that of (g, h) sends (a, b) to g ^ a.val * h ^ b.val.
• TauCeti.injective_zmod_three_prod_iff: a homomorphism (ℤ/3ℤ)² →* G is injective exactly when (1, 0), (0, 1), (1, 1) and (-1, 1) are not in its kernel.

theorem Multiplicative.mem_zpowers_ofAdd_one {N : ℕ} (x : Multiplicative (ZMod N)) : x ∈ Subgroup.zpowers (ofAdd 1)

The standard generator 1 of ℤ/Nℤ, written multiplicatively, generates the group.

noncomputable def TauCeti.zmodMonoidHomEquiv (N : ℕ) [NeZero N] (G : Type u_1) [Group G] : (Multiplicative (ZMod N) →* G) ≃ { g : G // g ^ N = 1 }

Homomorphisms ℤ/Nℤ →* G are the elements of G killed by N, through the image of 1.

@[simp]

theorem TauCeti.coe_zmodMonoidHomEquiv_apply {N : ℕ} [NeZero N] {G : Type u_1} [Group G] (φ : Multiplicative (ZMod N) →* G) : ↑((zmodMonoidHomEquiv N G) φ) = φ (Multiplicative.ofAdd 1)

The element of G of a homomorphism φ : ℤ/Nℤ →* G is φ 1.

theorem TauCeti.zmodMonoidHomEquiv_symm_apply_ofAdd_one {N : ℕ} [NeZero N] {G : Type u_1} [Group G] (g : { g : G // g ^ N = 1 }) : ((zmodMonoidHomEquiv N G).symm g) (Multiplicative.ofAdd 1) = ↑g

The homomorphism associated to an element killed by N sends 1 to that element, including when N = 1.

@[simp]

theorem TauCeti.zmodMonoidHomEquiv_symm_apply {N : ℕ} [NeZero N] {G : Type u_1} [Group G] (g : { g : G // g ^ N = 1 }) (a : ZMod N) : ((zmodMonoidHomEquiv N G).symm g) (Multiplicative.ofAdd a) = ↑g ^ a.val

The homomorphism ℤ/Nℤ →* G of an element g killed by N sends a to g ^ a.val.

noncomputable def TauCeti.zmodProdMonoidHomEquiv (N : ℕ) [NeZero N] (G : Type u_1) [CommGroup G] : (Multiplicative (ZMod N × ZMod N) →* G) ≃ { g : G // g ^ N = 1 } × { g : G // g ^ N = 1 }

Homomorphisms (ℤ/Nℤ)² →* G are the pairs of elements of G killed by N, through the images of (1, 0) and (0, 1).

@[simp]

theorem TauCeti.coe_zmodProdMonoidHomEquiv_apply_fst {N : ℕ} [NeZero N] {G : Type u_1} [CommGroup G] (φ : Multiplicative (ZMod N × ZMod N) →* G) : ↑((zmodProdMonoidHomEquiv N G) φ).1 = φ (Multiplicative.ofAdd (1, 0))

The first element of G of a homomorphism φ : (ℤ/Nℤ)² →* G is φ (1, 0).

@[simp]

theorem TauCeti.coe_zmodProdMonoidHomEquiv_apply_snd {N : ℕ} [NeZero N] {G : Type u_1} [CommGroup G] (φ : Multiplicative (ZMod N × ZMod N) →* G) : ↑((zmodProdMonoidHomEquiv N G) φ).2 = φ (Multiplicative.ofAdd (0, 1))

The second element of G of a homomorphism φ : (ℤ/Nℤ)² →* G is φ (0, 1).

@[simp]

theorem TauCeti.zmodProdMonoidHomEquiv_symm_apply {N : ℕ} [NeZero N] {G : Type u_1} [CommGroup G] (g : { g : G // g ^ N = 1 } × { g : G // g ^ N = 1 }) (a b : ZMod N) : ((zmodProdMonoidHomEquiv N G).symm g) (Multiplicative.ofAdd (a, b)) = ↑g.1 ^ a.val * ↑g.2 ^ b.val

The homomorphism (ℤ/Nℤ)² →* G of a pair (g, h) of elements killed by N sends (a, b) to g ^ a.val * h ^ b.val.

theorem TauCeti.injective_zmod_three_prod_iff {G : Type u_1} [Group G] (ψ : Multiplicative (ZMod 3 × ZMod 3) →* G) : Function.Injective ⇑ψ ↔ ψ (Multiplicative.ofAdd (1, 0)) ≠ 1 ∧ ψ (Multiplicative.ofAdd (0, 1)) ≠ 1 ∧ ψ (Multiplicative.ofAdd (1, 1)) ≠ 1 ∧ ψ (Multiplicative.ofAdd (-1, 1)) ≠ 1

Injectivity on (ℤ/3ℤ)². A homomorphism ψ : (ℤ/3ℤ)² →* G is injective exactly when (1, 0), (0, 1), (1, 1) and (-1, 1) are not in its kernel: every nonzero element of (ℤ/3ℤ)² is one of these four or its negative.