Homomorphism from the integers descends to $$\mathbb{Z}/n$$

Stream: Is there code for X?

[Heather Macbeth]

Does mathlib have the construction, given an additive group homomorphism $f:\mathbb{Z}\to A$ with $f(n)=0$, of the induced homomorphism $\widehat f:\mathbb{Z}/n \to A$?

import data.zmod.basic

variables {A : Type*} [add_group A]

example {f : ℤ →+ A} {n : ℕ} (hf : f n = 0) : (zmod n) →+ A := sorry

[Anatole Dedecker]

I can't find anything like that. I would have guessed it would be easy using a ring_equiv between zmod n and ideal.quotient (ideal.span ({n} : set ℤ)), but it turns out we don't have it either... (https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60.28ideal.2Espan.20.7Bd.7D.29.2Equotient.60.20is.20.60zmod.20d.60/near/241950260)

[Eric Wieser]

I'm surprised there's not a zmod.lift with that definition

[Anne Baanen]

I will need the equiv soon, so I'll see if I can define it and zmod.lift today.

[Eric Rodriguez]

Anne, this isn't much but I was going to work on it too, and I already made the ℤ-version of it, so here's a tiny tiny part:

import ring_theory.ideal.basic
import ring_theory.int.basic
import data.zmod.basic

example (a : ℤ) : zmod a.nat_abs ≃+* ideal.quotient (ideal.span ({a} : set ℤ)) :=
begin
  have : ideal.span {a} = ideal.span ({a.nat_abs} : set ℤ),
  { rw ideal.span_singleton_eq_span_singleton,
    exact int.associated_nat_abs _ },
  rw this,
  exact <ℕ-version> _,
end

[Anne Baanen]

Thank you very much! I just finished the add_equiv part:

section lift

open quotient_add_group
open zmod

variables (n : ℕ) {A R : Type*} [add_group A] [ring R]

lemma zmod.coe_add_eq_sub_n_or_self (a b : zmod n) :
  (↑(a + b) : ℤ) = if (n : ℤ) ≤ a + b then a + b - n else a + b :=
begin
  cases n,
  { simp },
  simp only [coe_coe, fin.coe_add, int.coe_nat_add, int.coe_nat_succ, int.nat_cast_eq_coe_nat],
  split_ifs with h,
  { have h' := int.coe_nat_lt.mp h,
    rw [nat.mod_eq_sub_mod h', nat.mod_eq_of_lt, int.coe_nat_sub h',
        int.coe_nat_add, int.coe_nat_succ],
    exact (nat.sub_lt_right_iff_lt_add h').mpr (nat.add_lt_add a.2 b.2) },
  { rw [nat.mod_eq_of_lt (int.coe_nat_lt.mp (lt_of_not_ge h)), int.coe_nat_add] }
end

/-- The map from `zmod n` induced by `f : ℤ →+ A` that maps `n` to `0`. -/
@[simps] def zmod.lift (f : ℤ →+ A) (hf : f n = 0) : zmod n →+ A :=
{ to_fun := f ∘ coe,
  map_add' := λ a b,
    by { rw [function.comp_app, zmod.coe_add_eq_sub_n_or_self],
         split_ifs; simp only [hf, add_monoid_hom.map_add, add_monoid_hom.map_sub, sub_zero] },
  map_zero' := by simp }

@[simp] lemma mem_gmultiples_iff_dvd {a b : ℤ} : a ∈ add_subgroup.gmultiples b ↔ b ∣ a :=
begin
  split,
  { rintro ⟨c, rfl⟩, exact dvd_mul_left _ _ },
  { rintro ⟨c, rfl⟩, rw mul_comm, exact add_subgroup.gsmul_mem _ mem_gmultiples _ },
end

/-- `ℤ` modulo multiples of `n : ℕ` is `zmod n`. -/
def quotient_gmultiples_equiv_zmod :
  quotient (add_subgroup.gmultiples (n : ℤ)) ≃+ zmod n :=
{ to_fun := quotient_add_group.lift _ (int.cast_add_hom _)
    (λ x hx, show int.cast_add_hom (zmod n) x = 0,
      from (int_coe_zmod_eq_zero_iff_dvd _ _).mpr (mem_gmultiples_iff_dvd.mp hx)),
  inv_fun := mk' (add_subgroup.gmultiples (n : ℤ)) ∘ coe,
  left_inv := λ x, quot.induction_on x (λ x, eq_iff_sub_mem.mpr $
    by rw [lift_quot_mk, int.coe_cast_add_hom, mem_gmultiples_iff_dvd,
           ← int_coe_zmod_eq_zero_iff_dvd, int.cast_sub, int_cast_zmod_cast, sub_self]),
  right_inv := λ x,
    by rw [function.comp_app, quotient_add_group.mk'_apply, lift_mk, int.coe_cast_add_hom,
           int_cast_zmod_cast],
  .. quotient_add_group.lift _ _ _ }

end lift

[Anne Baanen]

So it only remains to connect gmultiples n to ideal.span {n} and then add the mul parts of the equiv.

[Eric Wieser]

coe_add_eq_sub_... looks like something we will already have proved for fin?

[Anne Baanen]

I tried grepping for various permutations of coe, add, sub and mod with no luck, any idea where to look?

[Eric Wieser]

I think it's not there after all

[Eric Wieser]

coe_add_eq_ite is probably a better name

[Anne Baanen]

I have the add_equivs and ring_equivs finished too, without needing a lift. Should I keep coe_add_eq_ite if I don't need it anymore?

[Eric Wieser]

I think it's a nice lemma to have anyway, although maybe we should state it in terms of nat instead of int and make it be about fin

[Eric Wieser]

To match docs#fin.coe_add

[Anne Baanen]

The specialization to ℤ and zmod is not completely trivial so I'll keep that one too: since zmod 0 = ℤ not fin 0 you need to push around a few casts.

[Anne Baanen]

Final question: I needed a few small imports (ring_theory.int.basic and group_theory.quotient_group), those should be fine to add to data.zmod.basic, right?

[Eric Wieser]

I'm wary of doing that without first moving fin.comm_ring somewhere more fundamental

[Anne Baanen]

OK, then they'll live in a new file :+1:

[Eric Wieser]

section universal_property looks like it was intended to contain this new lift, but I can't work out which of the definitions actually in that section is being considered the universal property

[Eric Wieser]

(deleted)

[Anne Baanen]

Taking the composition with docs#zmod.cast_hom is "mathematically" the same thing as applying our new zmod.lift, except that it's phrased for rings with characteristic m rather than groups.

[Anne Baanen]

PR number one finally built on my machine: #7975

[Anne Baanen]

PR number two: #7976

[Patrick Massot]

It would be nice to see if we can hook this and our group presentation API (the required lift also comes from the universal property of the group presentation $\langle a | a^n \rangle$

[Anne Baanen]

Ah yes, that would be a very slick way to do it. I can't find much in mathlib though about presentations / the free group, for example docs#free_group.free_group_unit_equiv_int is just a bijection, not an isomorphism.

[Eric Wieser]

It looks like we already have a proof that any function from free_group is a homomorphism, so making the isomorphism is just a case of remembering to bundle everything

[Eric Wieser]

(eg docs#free_group.map_mul)