Coprimeness of products from pairwise coprimeness

Stream: Is there code for X?

[Pierre-Alexandre Bazin]

`import ring_theory.coprime.lemmas
open_locale big_operators

variables {R : Type} {I : Type} [comm_semiring R] {p : I → R} [decidable_eq I] {s : finset I}

lemma exists_sum_eq_one_iff_pairwise_coprime' :
(∃ μ : I → R, ∑ i in s, μ i * ∏ j in s \ {i}, p j = 1) ↔ pairwise (is_coprime on λ i : s, p i) :=
sorry`

I'm working on the classification of finitely generated modules over a PID and at some point I needed this lemma. It looks like it hasn't been proven yet and I'm not planning to work on it soon - so does anyone want to try proving it ?

(Note that is_coprime a b is defined as the existence of a relation a * u + b * v = 1 so this should be true even with a comm_semiring R. A way to prove i could be to do the product of all the relations is_coprime (p i) (p j) as _ = 1 and then develop the product - this gives a sum of 2^(s.card*(s.card-1)/2) terms that are all multiples of a ∏ j in s \ {i}, p j)

[Patrick Massot]

See explanations at #backticks

[Pierre-Alexandre Bazin]

Bumping as this got buried

[Eric Rodriguez]

import ring_theory.coprime.lemmas
open_locale big_operators

section subsingleton

variables {R : Type*} [comm_semiring R] [subsingleton R] {x y : R}

@[nontriviality, simp] lemma is_coprime_subsingleton : is_coprime = λ x y : R, true :=
by { funext, simp }

end subsingleton

variables {R : Type*} {I : Type*} [comm_semiring R] {p : I → R} [decidable_eq I] {s : finset I}

lemma exists_sum_eq_one_iff_pairwise_coprime' :
  (∃ μ : I → R, ∑ i in s, μ i * ∏ j in s \ {i}, p j = 1) ↔ pairwise (is_coprime on λ i : s, p i) :=
begin
  casesI subsingleton_or_nontrivial R,
  { simp only [eq_iff_true_of_subsingleton, exists_const, is_coprime_subsingleton, true_iff],
    tauto },
  induction s using finset.induction_on with a s has ih,
  { simp [pairwise],sorry },
  induction s using finset.induction_on with a s has ih,
  { simp [pairwise], }
end

doesn't hold for subsets of size < 2. do you just want to deal with that using 2 ≤ fintype.card s?

[Eric Rodriguez]

aa there's no card_induction for finsets :(

[Kyle Miller]

Would induction h : s.card be that induction principle?

[Eric Rodriguez]

hmm, I'm trying this and it's not working:

lemma exists_sum_eq_one_iff_pairwise_coprime' (h : 2 ≤ s.card) :
  (∃ μ : I → R, ∑ i in s, μ i * ∏ j in s \ {i}, p j = 1) ↔ pairwise (is_coprime on λ i : s, p i) :=
begin
  casesI subsingleton_or_nontrivial R,
  { simp only [eq_iff_true_of_subsingleton, exists_const, is_coprime_subsingleton, true_iff],
    tauto },
  refine nat.le_induction _ _ _ h,
end

[Eric Rodriguez]

I feel like there's some trick, like adding a variable n and making it so that n = s.card

[Eric Rodriguez]

ah, yeah, that's it:

lemma exists_sum_eq_one_iff_pairwise_coprime' (h : 2 ≤ s.card) :
  (∃ μ : I → R, ∑ i in s, μ i * ∏ j in s \ {i}, p j = 1) ↔ pairwise (is_coprime on λ i : s, p i) :=
begin
  casesI subsingleton_or_nontrivial R,
  { simp only [eq_iff_true_of_subsingleton, exists_const, is_coprime_subsingleton, true_iff],
    tauto },
  set n := s.card with hn,
  clear_value n,
  revert hn,
  apply n.le_induction _ _ h,
end

[Eric Rodriguez]

can we get induction to do this automatically?

[Eric Rodriguez]

(also, this isn't as nice as that would be - I'd want something like prove something for all finsets of card 2, and then get given s such that it holds and then I have to prove it for insert k s. but it's workable)

[Pierre-Alexandre Bazin]

Thanks ! I'll look at this.

I don't mind much having it only for size >= 2, as size 0 is false (I noticed it earlier but it looks like I accidentally deleted the hypothesis) and size 1 is trivial. Maybe we could do a lemma with just s nonempty as prerequisite by treating size 1 separately ?

[Eric Rodriguez]

oh, I'm dumb, yes size 1 holds too. there's a nonempty induction principle too, which is nice

[Kyle Miller]

Eric Rodriguez said:

can we get induction to do this automatically?

I'm not sure you can use nat.le_induction with induction, but if you were able to, then the h : syntax is what does that automatically.

[Eric Rodriguez]

I don't have any more time for this today, but this should be roughly half of the work done, hopefully the rest is routine:

import ring_theory.coprime.lemmas
open_locale big_operators

section subsingleton

variables {R : Type*} [comm_semiring R] [subsingleton R] {x y : R}

@[nontriviality, simp] lemma is_coprime_subsingleton : is_coprime = λ x y : R, true :=
by { funext, simp }

end subsingleton

section finset

lemma pairwise_insert {α} {s : finset α} {a : α} (h : a ∉ s) (r : α → α → Prop) :
  pairwise (r on λ a : s.cons a h, a) ↔ pairwise (r on λ a : s, a) ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a :=
sorry

end finset

variables {R : Type*} {I : Type*} [comm_semiring R] {p : I → R} [decidable_eq I] {s : finset I}

lemma exists_sum_eq_one_iff_pairwise_coprime' (h : s.nonempty) :
  (∃ μ : I → R, ∑ i in s, μ i * ∏ j in s \ {i}, p j = 1) ↔ pairwise (is_coprime on λ i : s, p i) :=
begin
  casesI subsingleton_or_nontrivial R,
  { simp only [eq_iff_true_of_subsingleton, exists_const, is_coprime_subsingleton, true_iff],
    tauto },
  refine h.cons_induction _ _; clear' s h,
  { simp only [pairwise, finset.sum_singleton, finset.sdiff_self, finset.prod_empty, mul_one,
               exists_apply_eq_apply, ne.def, true_iff],
    rintro a ⟨i, hi⟩ ⟨j, hj⟩ h,
    rw finset.mem_singleton at hi hj,
    simpa [hi, hj] using h },
  intros a s has h ih,
  have : ∀ s : finset I,
        (is_coprime on λ i : s, p i) = ((λ x y, is_coprime (p x) (p y)) on λ i : s, i),
  { simp [function.on_fun] },
  rw [this, pairwise_insert, ←this],
end

[Eric Rodriguez]

(note that there's a set.pairwise_insert so it should be easy to prove pairwise_insert from that. also, it should probably be called pairwise_cons! maybe both should exist)