-- Divisor sums over a coprime product: through the bijection
-- (d, e) ↦ d · e from divisors(a) × divisors(b) onto divisors(a · b)
-- (NumberTheory/DivisorSum), a sum over the divisors of a · b is the sum
-- over such pairs
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Combinatorics.CoprimeDivisors
import DivisorSums

-- The weight (d, e) ↦ w(d · e) on pairs of divisors.
defgraph pairedWeights (a b : Nat) (w : Set) (q ∈ divisors(a) × divisors(b)) :
    ℤ := w(divisorMul(a, b)(q))
requires nonzeroA : a ≠ 0
requires nonzeroB : b ≠ 0
requires weights : w : ℕ → ℤ
proof
  have function := divisorMul.function at a, b with nonzeroA, nonzeroB
  have image := FunctionBetween.apply_closed with function, member
  have naturals := divisors.subset_naturals at a * b
  have imageMember := naturals with divisorMul(a, b)(q), image
  exact FunctionBetween.apply_closed with weights, imageMember

-- A sum over the divisors of a coprime product a · b is the sum of
-- w(d · e) over the pairs of divisors d ∣ a, e ∣ b.
theorem divisorSum.mul_coprime (a b : Nat, w : Set)
  requires nonzeroA : a ≠ 0
  requires nonzeroB : b ≠ 0
  requires coprime : gcd(a, b) = 1
  requires weights : w : ℕ → ℤ
  shows divisorSum(a * b, w) =
    integerSetSum(divisors(a) × divisors(b), pairedWeights(a, b, w))
proof
  have finiteA := divisors.finite at a
  have finiteB := divisors.finite at b
  have finite := Finite.product with finiteA, finiteB
  have paired := pairedWeights.function at a, b, w with nonzeroA, nonzeroB,
    weights
  have bijective := divisorMul.bijective with nonzeroA, nonzeroB, coprime
  have selfSubset := Subset.reflexive at divisors(a) × divisors(b)
  have naturals := divisors.subset_naturals at a * b
  have values : ∀ q ∈ divisors(a) × divisors(b),
      pairedWeights(a, b, w)(q) = w(divisorMul(a, b)(q))
    intros q hq
    exact pairedWeights.value at a, b, w, q with nonzeroA, nonzeroB, weights,
      hq
  have sum := integerSetSum.reindex at divisors(a) × divisors(b),
    divisors(a * b), divisors(a) × divisors(b), ℕ, pairedWeights(a, b, w), w,
      divisorMul(a, b) with finite, paired, weights, selfSubset, naturals,
        bijective, values
  symm
  simp [divisorSum]