Documentation

TauCeti.Data.Nat.Factorization.PrimePowerProd.Basic

Ordered products over a prime factorisation #

n.factorization.prod f multiplies the blocks f p (n.factorization p) over the primes dividing n. Being a Finsupp.prod it asks for a CommMonoid: a Finsupp records no order on its support, so the product is only well defined once the factors commute.

TauCeti.Nat.primePowerProd f n multiplies the same blocks in a fixed order — least prime first — and so asks only for One and Mul. Each step peels Nat.minFac n together with its whole multiplicity, and recurses on ordCompl[n.minFac] n. Both n = 0 and n = 1 give the empty product.

The ordering is not the point; the weakened typeclass is. A monoid that happens to be commutative without carrying a CommMonoid instance — a Hecke ring whose commutativity is a theorem rather than a structure field, say — cannot form n.factorization.prod f at all, and this is what it forms instead. primePowerProd_eq_factorization_prod records that nothing is lost: as soon as a CommMonoid instance is available the two agree.

Neither associativity nor a unit law enters the definition — the bracketing is fixed — so it is stated at One plus Mul, in the same spirit as List.prod, which Lean defines at Mul plus One. mul_one is needed once, to collapse the single block of a prime power. Associativity enters with the multiplicativity on coprime arguments, which is stated in a Monoid under the hypothesis it actually uses — each block of n commutes with the blocks of m at larger primes, the pairs that merging the two increasing sequences has to exchange — so that the monoid of the previous paragraph can use it. Only the Finsupp.prod comparison needs the full CommMonoid.

Main definitions #

Main results #

Implementation notes #

The definition is Nat.recOnPrimePow, which already performs the least-prime-power decomposition this product runs over. That recursor is @[elab_as_elim] and mathlib states no computation rules for it, so the three equations primePowerProd_zero, primePowerProd_one and primePowerProd_of_one_lt are proved by unfolding it and Nat.strongRec once. Everything after them goes through those equations and never through the body again.

Coprime multiplicativity is a strong induction on m * n. The least prime of m * n lies in exactly one of the factors, and the peeling step splits off its block. When it lies in m the induction hypothesis and the peeling step for m already give the answer. When it lies in n its block comes out ahead of the whole of primePowerProd f m; it sits below every prime of m, so the commutation hypothesis moves it past that product — the one place the hypothesis is used — and the peeling step for n reassembles primePowerProd f n.

Provenance #

Adapted from AINTLIB (see References): peelProd and its six companion lemmas, which sit in a Hecke file inside the HeckeRing.GL2.Unified namespace. They are combinatorics about Nat.minFac carrying no Hecke content, so they are lifted here. The source asks Monoid/CommMonoid and writes the recursion out by hand; here the classes are weakened to One plus Mul, the recursion is routed through mathlib's Nat.recOnPrimePow, the coprime multiplicativity is proved in a Monoid from the commutation of the block pairs that merging exchanges instead of being read off the Finsupp.prod comparison, and that comparison is stated for every n rather than only for n ≠ 0. The comparison is private in the source and is exposed here, since it is the statement tying the definition to mathlib's idiom.

References #

source
noncomputable def TauCeti.Nat.primePowerProd {M : Type u_1} [One M] [Mul M] (f : ℕ → ℕ → M) :
ℕ → M

The product of the blocks f p (n.factorization p) over the primes p dividing n, taken in increasing order of p: each step peels off the least prime factor of n together with its whole multiplicity. The empty product 1 is returned at n = 1, and at n = 0 as a junk value — 0 has no factorisation to run over.

Only One M and Mul M are asked, which is the whole point of the definition; see primePowerProd_eq_factorization_prod for the agreement with n.factorization.prod f when M is commutative.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Nat.primePowerProd_zero {M : Type u_1} [One M] [Mul M] (f : ℕ → ℕ → M) :
    primePowerProd f 0 = 1
    source
    @[simp]
    theorem TauCeti.Nat.primePowerProd_one {M : Type u_1} [One M] [Mul M] (f : ℕ → ℕ → M) :
    primePowerProd f 1 = 1
    source
    theorem TauCeti.Nat.primePowerProd_of_one_lt {M : Type u_1} [One M] [Mul M] (f : ℕ → ℕ → M) {n : ℕ} (hn : 1 < n) :
    primePowerProd f n = f n.minFac (n.factorization n.minFac) * primePowerProd f (n / n.minFac ^ n.factorization n.minFac)

    The peeling step: for 1 < n the ordered product splits off the block at n.minFac, leaving the ordered product over ordCompl[n.minFac] n.

    source
    @[simp]
    theorem TauCeti.Nat.primePowerProd_prime_pow {M : Type u_1} [MulOneClass M] (f : ℕ → ℕ → M) {p : ℕ} (hp : Nat.Prime p) {v : ℕ} (hv : v ≠ 0) :
    primePowerProd f (p ^ v) = f p v

    On a prime power the product is a single block: primePowerProd f (p ^ v) = f p v. The hypothesis v ≠ 0 is needed — at v = 0 the left-hand side is the empty product 1 while the right-hand side is f p 0, and nothing forces those to agree.

    source
    @[simp]
    theorem TauCeti.Nat.primePowerProd_prime {M : Type u_1} [MulOneClass M] (f : ℕ → ℕ → M) {p : ℕ} (hp : Nat.Prime p) :
    primePowerProd f p = f p 1

    At a prime the product is the single block f p 1: the case v = 1 of primePowerProd_prime_pow, stated separately because a bare prime is not syntactically a power, so that lemma cannot fire on it.

    source
    theorem Commute.primePowerProd_right {M : Type u_1} [Monoid M] (f : ℕ → ℕ → M) {x : M} {n : ℕ} (h : ∀ p ∈ n.primeFactors, Commute x (f p (n.factorization p))) :
    Commute x (TauCeti.Nat.primePowerProd f n)

    An element commuting with every block of n commutes with their ordered product.

    source
    theorem TauCeti.Nat.primePowerProd_mul_of_coprime {M : Type u_1} [Monoid M] (f : ℕ → ℕ → M) {m n : ℕ} (hmn : m.Coprime n) (hf : ∀ p ∈ m.primeFactors, ∀ q ∈ n.primeFactors, q < p → Commute (f p (m.factorization p)) (f q (n.factorization q))) :
    primePowerProd f (m * n) = primePowerProd f m * primePowerProd f n

    Multiplicativity on coprime arguments. When m and n share no prime, the blocks of m * n are the blocks of m together with those of n, interleaved by size; sorting them into the blocks of m followed by those of n moves each block of n past the blocks of m at larger primes, and those are the only pairs asked to commute. In a CommMonoid it is discharged by fun _ _ _ _ _ ↦ Commute.all _ _.

    source
    @[simp]
    theorem TauCeti.Nat.primePowerProd_eq_factorization_prod {M : Type u_1} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
    primePowerProd f n = n.factorization.prod f

    Once the factors commute the ordering is invisible and the ordered product is the Finsupp.prod over the factorisation. Unconditional in n, so it rewrites without a side goal: at n = 0 both sides are 1, the left as the junk value and the right because Nat.factorization 0 = 0 has empty support.

    source
    theorem TauCeti.Nat.primePowerProd_eq_ordProj_mul_ordCompl {M : Type u_1} [CommMonoid M] (f : ℕ → ℕ → M) (p : ℕ) {m : ℕ} :
    primePowerProd f m = primePowerProd f (p ^ m.factorization p) * primePowerProd f (m / p ^ m.factorization p)

    Splitting the assembly at a prime-power part: primePowerProd f m is its p-block primePowerProd f (p ^ v_p(m)) times the assembly over ordCompl[p] m. At m = 0 all three products are 1; for nonprime p its exponent is zero and the first factor is 1.