English
There is a bijection between ℕ × factoredNumbers s and factoredNumbers (insert p s) given by (e,m) ↦ p^e · m when p ∉ s and p is prime.
Русский
Существует биекция между ℕ × factoredNumbers(s) и factoredNumbers(insert p s) при условии, что p простое и p ∉ s.
LaTeX
$$ℕ × factoredNumbers(s) ≃ factoredNumbers(insert p s)$$
Lean4
/-- We establish the bijection from `ℕ × factoredNumbers s` to `factoredNumbers (s ∪ {p})`
given by `(e, n) ↦ p^e * n` when `p ∉ s` is a prime. See `Nat.factoredNumbers_insert` for
when `p` is not prime. -/
def equivProdNatFactoredNumbers {s : Finset ℕ} {p : ℕ} (hp : p.Prime) (hs : p ∉ s) :
ℕ × factoredNumbers s ≃ factoredNumbers (insert p s)
where
toFun := fun ⟨e, n⟩ ↦ ⟨p ^ e * n, pow_mul_mem_factoredNumbers hp e n.2⟩
invFun := fun ⟨m, _⟩ ↦ (m.factorization p, ⟨(m.primeFactorsList.filter (· ∈ s)).prod, prod_mem_factoredNumbers ..⟩)
left_inv := by
rintro ⟨e, m, hm₀, hm⟩
simp (etaStruct := .all) only [Prod.mk.injEq, Subtype.mk.injEq]
constructor
· rw [factorization_mul (pos_iff_ne_zero.mp <| Nat.pow_pos hp.pos) hm₀]
simp only [factorization_pow, Finsupp.coe_add, Finsupp.coe_smul, nsmul_eq_mul, Pi.natCast_def, cast_id,
Pi.add_apply, Pi.mul_apply, hp.factorization_self, mul_one, add_eq_left]
rw [← primeFactorsList_count_eq, count_eq_zero]
exact fun H ↦ hs (hm p H)
· nth_rewrite 2 [← prod_primeFactorsList hm₀]
refine prod_eq <| (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_
rw [filter_append, hp.primeFactorsList_pow,
filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs], nil_append,
filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
right_inv := by
rintro ⟨m, hm₀, hm⟩
simp only [Subtype.mk.injEq]
rw [← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]
nth_rewrite 3 [← prod_primeFactorsList hm₀]
have : m.primeFactorsList.filter (· = p) = m.primeFactorsList.filter (· ∉ s) :=
by
refine (filter_congr fun q hq ↦ ?_).symm
simp only [decide_not]
rcases Finset.mem_insert.mp <| hm _ hq with h | h
· simp only [h, hs, decide_false, Bool.not_false, decide_true]
· simp only [h, decide_true, Bool.not_true, false_eq_decide_iff]
exact fun H ↦ hs <| H ▸ h
refine prod_eq <| (filter_eq p).symm ▸ this ▸ perm_append_comm.trans ?_
simp only [decide_not]
exact filter_append_perm (· ∈ s) (primeFactorsList m)
