checking a subgroup of Int is generated by an element

Stream: Is there code for X?

[Scott Morrison]

Do we have the ingredients for

import Mathlib

theorem AddSubgroup.eq_zmultiples_int (G : AddSubgroup ℤ) (k : ℕ) (w : k ≠ 0) :
    G = .zmultiples (k : ℤ) ↔
      ((k : ℤ) ∈ G ∧ ∀ q ∈ Nat.primeFactors k, (k / q : Int) ∉ G) :=
  sorry

or does it need to be done by hand?

[Jireh Loreaux]

ugh... that was more work than I was hoping. There was certainly some missing API in various places. I proved it instead for Ideal.span (k : ℤ) so that I could use that ℤ is a PID (it would have been possible and not too terrible to do without this, but I thought it was easiest), and then got the subgroup result from docs#AddSubgroup.toIntSubmodule.

The main issue boils down to a Nat result: if j ∣ k and j < k, then there is some p ∈ k.primeFactors so that j | k / p.

import Mathlib

@[simp]
lemma AddSubgroup.toIntSubmodule_zmultiples (k : ℕ) :
    (AddSubgroup.toIntSubmodule (.zmultiples (k : ℤ))) = Ideal.span {(k : ℤ)} := by
  ext n
  show n ∈ AddSubgroup.zmultiples (k : ℤ) ↔ _
  rw [Ideal.mem_span_singleton, Int.mem_zmultiples_iff]

lemma Nat.one_lt_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) : 1 < n :=
  match n with
  | 0 => by simp at h
  | 1 => by simp at h
  | n + 2 => n.one_lt_succ_succ

lemma Nat.one_lt_div_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) :
    1 < n / m := by
  have hm := Nat.pos_of_mem_properDivisors h
  apply lt_of_mul_lt_mul_right ?_ hm.le
  obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
  simpa [Nat.div_mul_cancel h_dvd] using h_lt

lemma Nat.mem_properDivisors_iff_exists {m n : ℕ} (hn : n ≠ 0) :
    m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k := by
  constructor
  · exact fun h ↦
      ⟨n / m, one_lt_div_of_mem_properDivisors h, by
        rw [mul_comm]; exact (Nat.div_mul_cancel (mem_properDivisors.mp h).1).symm⟩
  · rintro ⟨k, hk, h⟩
    refine mem_properDivisors.mpr ⟨⟨k, h⟩, ?_⟩
    calc
      m = m * 1 := (mul_one m).symm
      _ < m * k := by
        gcongr
        exact Nat.pos_of_ne_zero fun hm ↦ hn <| by simpa [hm] using h
      _ = n     := h.symm

lemma Nat.nonempty_primeFactors {n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n := by
  rw [←not_iff_not]
  simp only [Finset.not_nonempty_iff_eq_empty, primeFactors_eq_empty, not_lt]
  match n with
  | 0 => simp
  | 1 => simp
  | n + 2 => simp

theorem eq_ideal_span_int (I : Ideal ℤ) (k : ℕ) (w : k ≠ 0) :
    I = Ideal.span {(k : ℤ)} ↔
      (k : ℤ) ∈ I ∧ ∀ q ∈ Nat.primeFactors k, (k / q : Int) ∉ I := by
  have : ∃ j : ℕ, Ideal.span {(j : ℤ)} = I :=
    ⟨(Submodule.IsPrincipal.generator I).natAbs, by rw [Int.span_natAbs, I.span_singleton_generator]⟩
  obtain ⟨j, rfl⟩ := this
  constructor
  · intro h
    rw [h]
    refine ⟨Ideal.mem_span_singleton_self (k : ℤ), fun q hq ↦ ?_⟩
    rw [Ideal.mem_span_singleton]
    norm_cast
    have hq' : 1 < q := (Nat.prime_of_mem_primeFactors hq).one_lt
    have : k / q < k := Nat.div_lt_self (Nat.pos_of_ne_zero w) hq'
    intro hk
    apply Nat.le_of_dvd at hk
    · exact irrefl k (hk.trans_lt this)
    · have := Nat.div_dvd_of_dvd <| Nat.dvd_of_mem_primeFactors hq
      exact Nat.pos_of_dvd_of_pos this (Nat.zero_lt_of_lt ‹_›)
  · rintro ⟨hk, h⟩
    simp_rw [Ideal.mem_span_singleton] at h hk
    norm_cast at h hk
    simp only [Ideal.span_singleton_eq_span_singleton, Int.associated_iff_natAbs, Int.natAbs_cast]
    apply eq_of_le_of_not_lt (Nat.le_of_dvd (Nat.pos_of_ne_zero w) hk) fun hj ↦ ?_
    have hj' : j ∈ k.properDivisors := by simpa only [Nat.mem_properDivisors] using ⟨hk, hj⟩
    obtain ⟨m, hm_one, hm⟩ := (Nat.mem_properDivisors_iff_exists w).mp hj'
    obtain ⟨p, hp⟩ := Nat.nonempty_primeFactors.mpr hm_one |>.bex
    have hp' := Nat.primeFactors_mono ⟨j, mul_comm j m ▸ hm⟩ w hp
    apply h p hp'
    use m / p
    apply Nat.mul_right_cancel (Nat.pos_of_mem_primeFactors hp)
    rwa [mul_assoc, Nat.div_mul_cancel (Nat.dvd_of_mem_primeFactors hp),
      Nat.div_mul_cancel (Nat.dvd_of_mem_primeFactors hp')]

theorem eq_zmultiples_int (G : AddSubgroup ℤ) (k : ℕ) (w : k ≠ 0) :
    G = .zmultiples (k : ℤ) ↔
      ((k : ℤ) ∈ G ∧ ∀ q ∈ Nat.primeFactors k, (k / q : Int) ∉ G) := by
  rw [← (AddSubgroup.toIntSubmodule (M := ℤ)).injective.eq_iff]
  rw [AddSubgroup.toIntSubmodule_zmultiples]
  simp_rw [←SetLike.mem_coe, ← AddSubgroup.coe_toIntSubmodule, SetLike.mem_coe]
  exact eq_ideal_span_int _ k w

[Jireh Loreaux]

@Scott Morrison let me know what you think. If there was some simpler argument you were hoping for, I'd be interested. Otherwise I'll PR bits of this in a day or two.

[Scott Morrison]

No, that was the argument I had in mind. Thank you so much for this!

[Scott Morrison]

It's very useful that this could be done so quickly: Rob and I are talking to some CAS people about verifying algorithms modulo CAS black boxes, and this came up in the toy problem we're investigating. I'll be able to use this code in our working group in 20 minutes. :-)

[Yongyi Chen]

I was able to do this without translating to ideals.

import Mathlib

theorem Int.dvd_div_iff {a b c : ℤ} (hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b := by
  rw [← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs, natAbs_mul, natAbs_ediv _ _ hbc]
  exact Nat.dvd_div_iff (natAbs_dvd_natAbs.mpr hbc)

theorem AddSubgroup.eq_zmultiples_int (G : AddSubgroup ℤ) (k : ℕ) (knz : k ≠ 0) : G = .zmultiples (k : ℤ) ↔ ((k : ℤ) ∈ G ∧ ∀ q ∈ Nat.primeFactors k, (k / q : Int) ∉ G) := by
  obtain ⟨n, rfl⟩ := Int.subgroup_cyclic G
  rw [← zmultiples_eq_closure]
  by_cases nz : n = 0
  · subst nz
    simp_all only [ne_eq, zmultiples_zero_eq_bot, mem_bot, Nat.cast_eq_zero, Nat.mem_primeFactors, Nat.isUnit_iff, not_false_eq_true, and_true, and_imp, false_and, iff_false]
    rw [← ne_eq, ne_comm, zmultiples_ne_bot]
    exact Int.ofNat_ne_zero.mpr knz
  constructor
  · intro h
    simp_all only [ne_eq, mem_zmultiples, Nat.mem_primeFactors, Nat.isUnit_iff, not_false_eq_true, and_true, and_imp, true_and]
    rintro q pq ⟨a, rfl⟩ ⟨b, hb⟩
    have : q ≠ 1 := by exact Nat.Prime.ne_one pq
    simp_all only [mul_eq_zero, not_or, Nat.cast_mul, smul_eq_mul, ← mul_assoc, ne_eq, Nat.cast_eq_zero, not_false_eq_true, Int.mul_ediv_cancel_left, mul_eq_right₀, Int.mul_eq_one_iff_eq_one_or_neg_one, Nat.cast_eq_one, and_false, false_or, neg_mul, one_mul]
    exact nomatch q
  · rintro ⟨⟨m, hm⟩, h⟩
    ext x
    simp_all only [ne_eq, Nat.mem_primeFactors, Nat.isUnit_iff, not_false_eq_true, and_true, Int.mem_zmultiples_iff, and_imp, smul_eq_mul, ← Int.ofNat_dvd, ← hm, Int.dvd_div_iff, mul_dvd_mul_iff_right nz]
    constructor
    · rintro ⟨a, rfl⟩
      rw [mul_comm]
      apply mul_dvd_mul_left
      suffices IsUnit m by exact IsUnit.dvd this
      rw [Int.isUnit_iff]
      contrapose! h
      simp_rw [← Int.natAbs_dvd_natAbs, Int.natAbs_mul]
      have : m.natAbs ≠ 1 := by
        intro hm
        simp_all only [Int.natAbs_eq_iff, ne_eq, Nat.cast_one, or_self]
      use m.natAbs.minFac, m.natAbs.minFac_prime this
      constructor
      · apply dvd_mul_of_dvd_left <| Nat.minFac_dvd _
      · apply Nat.minFac_dvd
    · exact dvd_of_mul_left_dvd

[Junyan Xu]

Different idea, by observing the similarity between the statement and addOrderOf_eq_of_nsmul_and_div_prime_nsmul.

import Mathlib

theorem AddSubgroup.mem_iff_nsmul_eq_zero (G : AddSubgroup ℤ) {k : ℕ} : (k : ℤ) ∈ G ↔ k • ((1 : ℤ) : ℤ ⧸ G) = 0 := by
  rw [← QuotientAddGroup.mk_nsmul, nsmul_one, QuotientAddGroup.eq_zero_iff]

theorem AddSubgroup.mem_iff_zsmul_eq_zero (G : AddSubgroup ℤ) {k : ℤ} : k ∈ G ↔ k • ((1 : ℤ) : ℤ ⧸ G) = 0 := by
  rw [← QuotientAddGroup.mk_zsmul, zsmul_one, QuotientAddGroup.eq_zero_iff]; rfl

theorem AddSubgroup.eq_zmultiples_addOrderOf (G : AddSubgroup ℤ) : G = .zmultiples (addOrderOf ((1 : ℤ) : ℤ ⧸ G)) := by
  ext x; rw [G.mem_iff_zsmul_eq_zero, Int.mem_zmultiples_iff, addOrderOf_dvd_iff_zsmul_eq_zero]

theorem AddSubgroup.zmultiples_inj : Function.Injective fun n : ℕ ↦ AddSubgroup.zmultiples (n : ℤ) := fun n m h ↦ by
  dsimp only at h
  have hn := mem_zmultiples (n : ℤ)
  have hm := mem_zmultiples (m : ℤ)
  rw [h] at hn
  rw [← h] at hm
  rw [Int.mem_zmultiples_iff, Int.coe_nat_dvd] at hn hm
  exact Nat.dvd_antisymm hm hn

theorem QuotientAddGroup.zmultiples_addOrderOf_one (k : ℕ) : addOrderOf ((1 : ℤ) : ℤ ⧸ AddSubgroup.zmultiples (k : ℤ)) = k :=
  AddSubgroup.zmultiples_inj <| by simp_rw [← AddSubgroup.eq_zmultiples_addOrderOf]

theorem AddSubgroup.eq_zmultiples_int (G : AddSubgroup ℤ) (k : ℕ) (w : k ≠ 0) :
    G = .zmultiples (k : ℤ) ↔
      ((k : ℤ) ∈ G ∧ ∀ q ∈ Nat.primeFactors k, (k / q : ℤ) ∉ G) := by
  simp_rw [← Int.coe_nat_div, G.mem_iff_nsmul_eq_zero, Nat.mem_primeFactors, and_imp, imp_iff_right w]
  rw [← Nat.pos_iff_ne_zero] at w
  constructor
  · have := QuotientAddGroup.zmultiples_addOrderOf_one k
    rintro rfl; refine ⟨?_, fun q hq hqk hkq ↦ ?_⟩
    · convert addOrderOf_nsmul_eq_zero _; rw [this]
    apply hq.ne_one
    rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_right w, one_mul]
    rwa [← addOrderOf_dvd_iff_nsmul_eq_zero, this, Nat.dvd_div_iff hqk] at hkq
  intro h
  rw [← addOrderOf_eq_of_nsmul_and_div_prime_nsmul w h.1 h.2, ← G.eq_zmultiples_addOrderOf]