Exact divisors of a natural number

Q is an exact divisor of N when Q ∣ N and Q is coprime to the complementary divisor N / Q; equivalently, N = Q · M with Q and M sharing no prime. Such a Q collects the full power of each prime it contains, so the exact divisors of N are exactly the products of the maximal prime powers p ^ (N.factorization p), and they form a Boolean algebra under the subsets of N.primeFactors. The notion is also called a unitary or Hall divisor.

The classical notation is Q ‖ N, which cannot be used here: ‖ ‖ is norm notation, and in the same corner of the library p ^ r ‖ n means exact p-adic divisibility — that r is the full exponent of p, a statement about the pair (p, r) rather than about the single number p ^ r. The notation introduced instead is Q ∥ N, with the parallel bars ∥ in place of the double vertical line ‖; it is scoped, so it never competes with the ∥ of AffineSubspace.Parallel.

Main definitions

• TauCeti.Nat.IsExactDivisor: the predicate itself.
• TauCeti.Nat.ExactDivisor: the exact divisors of a fixed N, bundled as a commutative group whose multiplication is symmetric difference.
• TauCeti.Nat.prodPrimePow: the exact divisor ∏ p ∈ s, p ^ v_p(N) cut out by a set s of primes of N.
• TauCeti.Nat.ExactDivisor.primeFactorsEquiv: the identification of the exact divisors of N with the subsets of N.primeFactors.

Notation

• Q ∥ N for TauCeti.Nat.IsExactDivisor Q N, in the TauCeti.ExactDivisor scope.

Main results

• TauCeti.Nat.isExactDivisor_iff: the predicate unfolded to its two conditions.
• TauCeti.Nat.IsExactDivisor.div: for N ≠ 0 the complementary divisor N / Q is exact too.
• TauCeti.Nat.IsExactDivisor.ne_zero: an exact divisor is nonzero. There is no exact divisor 0, because Nat.Coprime 0 0 is false.
• TauCeti.Nat.isExactDivisor_one, TauCeti.Nat.isExactDivisor_self: 1 and (for N ≠ 0) N itself.
• TauCeti.Nat.IsExactDivisor.mul: coprime exact divisors multiply to an exact divisor, so the exact divisors of N are closed under coprime products.
• TauCeti.Nat.isExactDivisor_iff_factorization: exactness read on the factorization — at every prime the exponent of Q is either 0 or the full exponent of N.
• TauCeti.Nat.IsExactDivisor.gcd, TauCeti.Nat.IsExactDivisor.div_gcd, TauCeti.Nat.IsExactDivisor.coprime_div_gcd: the Boolean-algebra structure, in the form the Atkin–Lehner group law needs — gcd Q R and Q / gcd Q R are again exact divisors, and the second is coprime to R.
• TauCeti.Nat.IsExactDivisor.mul_div_gcd_sq: Q * R / gcd (Q, R) ^ 2 — the symmetric difference of Q and R — is an exact divisor too.
• TauCeti.Nat.ExactDivisor.val_mul: multiplication in the bundled group has underlying value Q * R / gcd (Q, R) ^ 2.
• TauCeti.Nat.isExactDivisor_prodPrimePow, TauCeti.Nat.primeFactors_prodPrimePow, TauCeti.Nat.IsExactDivisor.prodPrimePow_primeFactors: a subset of N.primeFactors cuts out an exact divisor with exactly those prime factors, and every exact divisor arises this way — the prime-power generation of the family, bundled as TauCeti.Nat.ExactDivisor.primeFactorsEquiv.
• TauCeti.Nat.isExactDivisor_primePow: the maximal prime powers p ^ v_p(N) are exact divisors.
• TauCeti.Nat.coprime_primePow_prodPrimePow: p ^ v_p(N) is prime to ∏ q ∈ s, q ^ v_q(N) for p ∉ s.

structure TauCeti.Nat.IsExactDivisor (Q N : ℕ) : Prop

Q is an exact divisor of N: it divides N and is coprime to the complementary divisor N / Q. Written Q ‖ N in the literature and Q ∥ N here; see the module docstring for the change of bars.

• dvd : Q ∣ N

  An exact divisor is a divisor.

• coprime : Q.Coprime (N / Q)

  An exact divisor is coprime to its complementary divisor.

def TauCeti.ExactDivisor.«term_∥_» : Lean.TrailingParserDescr

Q is an exact divisor of N: it divides N and is coprime to the complementary divisor N / Q. Written Q ‖ N in the literature and Q ∥ N here; see the module docstring for the change of bars.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Nat.IsExactDivisor.ne_zero {N Q : ℕ} (h : IsExactDivisor Q N) : Q ≠ 0

An exact divisor is nonzero. 0 is only a divisor of 0, whose complementary divisor is again 0, and Nat.Coprime 0 0 is false.

theorem TauCeti.Nat.IsExactDivisor.pos {N Q : ℕ} (h : IsExactDivisor Q N) : 0 < Q

An exact divisor is positive.

@[simp]

theorem TauCeti.Nat.isExactDivisor_iff {N Q : ℕ} : IsExactDivisor Q N ↔ Q ∣ N ∧ Q.Coprime (N / Q)

The defining conditions of an exact divisor, as a rewrite rule.

theorem TauCeti.Nat.IsExactDivisor.div {N Q : ℕ} (h : IsExactDivisor Q N) (hN : N ≠ 0) : IsExactDivisor (N / Q) N

The complementary divisor is exact. For N ≠ 0, N / Q is again an exact divisor of N, whose own complement is Q again (Nat.div_div_self). At N = 0 this fails: 1 is an exact divisor of 0, but 0 / 1 = 0 is not.

theorem TauCeti.Nat.isExactDivisor_one {N : ℕ} : IsExactDivisor 1 N

1 is an exact divisor of every N.

theorem TauCeti.Nat.isExactDivisor_self {N : ℕ} (hN : N ≠ 0) : IsExactDivisor N N

A nonzero N is an exact divisor of itself: the complementary divisor is 1. This is the case of the Fricke operator inside the Atkin–Lehner family.

theorem TauCeti.Nat.IsExactDivisor.mul {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (hQR : Q.Coprime R) : IsExactDivisor (Q * R) N

Coprime exact divisors multiply. The exact divisors of N are therefore closed under coprime products, which is how the family generated by the maximal prime powers of N is built up.

The Boolean-algebra structure

theorem TauCeti.Nat.isExactDivisor_zero_iff {Q : ℕ} : IsExactDivisor Q 0 ↔ Q = 1

The only exact divisor of 0 is 1. The complementary divisor of Q in 0 is 0 again, and Nat.Coprime Q 0 says Q = 1. This is what lets the closure properties below carry no N ≠ 0 hypothesis.

theorem TauCeti.Nat.isExactDivisor_iff_factorization {N Q : ℕ} (hN : N ≠ 0) : IsExactDivisor Q N ↔ Q ∣ N ∧ ∀ (p : ℕ), Q.factorization p = 0 ∨ Q.factorization p = N.factorization p

Exactness, read on the factorization. For N ≠ 0, a divisor Q of N is exact exactly when at every prime its exponent is either 0 or the full exponent of N. In this form the closure properties below become statements about the exponents of gcd and of a quotient, namely about min and truncated subtraction.

theorem TauCeti.Nat.IsExactDivisor.gcd {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) : IsExactDivisor (Q.gcd R) N

Exact divisors are closed under gcd. At each prime the exponent of gcd Q R is the minimum of two exponents each of which is 0 or the full exponent of N.

theorem TauCeti.Nat.IsExactDivisor.div_gcd {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) : IsExactDivisor (Q / Q.gcd R) N

The quotient of an exact divisor by a gcd with another one is exact. At each prime the exponent of Q / gcd Q R is 0 unless Q carries the full exponent of N there and R carries none, in which case it is again that full exponent.

theorem TauCeti.Nat.IsExactDivisor.coprime_div_gcd {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) : (Q / Q.gcd R).Coprime R

Q / gcd Q R is coprime to R. A prime dividing the quotient carries the full exponent of N in Q and none of it in R; this is the step where the exactness of both divisors is used, and it fails for divisors in general (Q = 4, R = 2).

theorem TauCeti.Nat.IsExactDivisor.mul_div_gcd_sq {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) : IsExactDivisor (Q * R / Q.gcd R ^ 2) N

The symmetric difference of two exact divisors is exact. Q * R / gcd (Q, R) ^ 2 is the product of the coprime exact divisors Q / gcd (Q, R) and R / gcd (Q, R); under the identification of exact divisors with subsets of N.primeFactors it is the symmetric difference, which is why it is the composition law of the Atkin–Lehner family.

Exact divisors from sets of primes

def TauCeti.Nat.prodPrimePow (N : ℕ) (s : Finset ℕ) : ℕ

The exact divisor of N supported on a set of primes: the product ∏ p ∈ s, p ^ v_p(N) of the maximal prime powers of N at the primes of s. For s ⊆ N.primeFactors this is the exact divisor of N whose prime factors are exactly s (TauCeti.Nat.isExactDivisor_prodPrimePow, TauCeti.Nat.primeFactors_prodPrimePow), and every exact divisor arises this way (TauCeti.Nat.IsExactDivisor.prodPrimePow_primeFactors).

Equations

• TauCeti.Nat.prodPrimePow N s = ∏ p ∈ s, p ^ N.factorization p

@[simp]

theorem TauCeti.Nat.prodPrimePow_empty {N : ℕ} : prodPrimePow N ∅ = 1

The empty set cuts out the exact divisor 1.

@[simp]

theorem TauCeti.Nat.prodPrimePow_insert {N : ℕ} {s : Finset ℕ} {q : ℕ} (hq : q ∉ s) : prodPrimePow N (insert q s) = q ^ N.factorization q * prodPrimePow N s

Adjoining a prime multiplies by its maximal power: ∏ p ∈ insert q s, p ^ v_p(N) is q ^ v_q(N) times the product over s, for q ∉ s.

theorem TauCeti.Nat.factorization_prodPrimePow {N : ℕ} {s : Finset ℕ} (hs : s ⊆ N.primeFactors) (q : ℕ) : (prodPrimePow N s).factorization q = if q ∈ s then N.factorization q else 0

The exponents of ∏ p ∈ s, p ^ v_p(N): the full exponent of N at the primes of s, and 0 elsewhere.

theorem TauCeti.Nat.isExactDivisor_prodPrimePow {N : ℕ} {s : Finset ℕ} : IsExactDivisor (prodPrimePow N s) N

A finite set cuts out an exact divisor. Indices outside N.primeFactors have exponent zero and contribute 1, while the remaining product consists of maximal prime powers of N.

theorem TauCeti.Nat.primeFactors_prodPrimePow {N : ℕ} {s : Finset ℕ} (hs : s ⊆ N.primeFactors) : (prodPrimePow N s).primeFactors = s

The prime factors of ∏ p ∈ s, p ^ v_p(N) are s, so distinct subsets of N.primeFactors cut out distinct exact divisors.

theorem TauCeti.Nat.isExactDivisor_primePow {N p : ℕ} : IsExactDivisor (p ^ N.factorization p) N

The maximal prime powers are exact divisors. This also holds when the exponent is zero, in which case the power is 1. These generate the family: every exact divisor is a product of them (TauCeti.Nat.IsExactDivisor.prodPrimePow_primeFactors).

theorem TauCeti.Nat.coprime_primePow_prodPrimePow {N : ℕ} {s : Finset ℕ} {p : ℕ} (hps : p ∉ s) : (p ^ N.factorization p).Coprime (prodPrimePow N s)

A maximal prime power is prime to the product over the other primes: p ^ v_p(N) is coprime to ∏ q ∈ s, q ^ v_q(N) for p ∉ s.

theorem TauCeti.Nat.IsExactDivisor.primeFactors_subset {N Q : ℕ} (h : IsExactDivisor Q N) : Q.primeFactors ⊆ N.primeFactors

An exact divisor of N only involves primes of N.

theorem TauCeti.Nat.IsExactDivisor.prodPrimePow_primeFactors {N Q : ℕ} (h : IsExactDivisor Q N) : prodPrimePow N Q.primeFactors = Q

Every exact divisor is the product of the maximal prime powers it contains: the exponents of an exact divisor are those of N at the primes dividing it. This is the prime-power generation of the Atkin–Lehner family.

The exact-divisor group

structure TauCeti.Nat.ExactDivisor (N : ℕ) : Type

The exact divisors of N, bundled as a group. Multiplication is symmetric difference: the value of Q * R is Q R / gcd(Q, R)². Every element is its own inverse, and the identity is the exact divisor 1.

• val : ℕ

  The underlying natural-number divisor.

• property : IsExactDivisor self.val N

  The underlying value is an exact divisor of N.

theorem TauCeti.Nat.ExactDivisor.ext {N : ℕ} {Q R : ExactDivisor N} (h : Q.val = R.val) : Q = R

Two exact divisors are equal when their underlying natural numbers are equal.

theorem TauCeti.Nat.ExactDivisor.ext_iff {N : ℕ} {Q R : ExactDivisor N} : Q = R ↔ Q.val = R.val

@[instance_reducible]

instance TauCeti.Nat.ExactDivisor.instCoeOutNat {N : ℕ} : CoeOut (ExactDivisor N) ℕ

Equations

• TauCeti.Nat.ExactDivisor.instCoeOutNat = { coe := TauCeti.Nat.ExactDivisor.val }

@[instance_reducible]

instance TauCeti.Nat.ExactDivisor.instOne {N : ℕ} : One (ExactDivisor N)

Equations

• TauCeti.Nat.ExactDivisor.instOne = { one := { val := 1, property := ⋯ } }

@[instance_reducible]

instance TauCeti.Nat.ExactDivisor.instMul {N : ℕ} : Mul (ExactDivisor N)

Multiplication of exact divisors is symmetric difference, with underlying value Q * R / gcd(Q, R) ^ 2.

Equations

• TauCeti.Nat.ExactDivisor.instMul = { mul := fun (Q R : TauCeti.Nat.ExactDivisor N) => { val := Q.val * R.val / Q.val.gcd R.val ^ 2, property := ⋯ } }

@[instance_reducible]

instance TauCeti.Nat.ExactDivisor.instInv {N : ℕ} : Inv (ExactDivisor N)

Inversion is the identity because every exact divisor is self-inverse under symmetric difference.

Equations

• TauCeti.Nat.ExactDivisor.instInv = { inv := id }

@[simp]

theorem TauCeti.Nat.ExactDivisor.val_one {N : ℕ} : val 1 = 1

The identity exact divisor has underlying value 1.

@[simp]

theorem TauCeti.Nat.ExactDivisor.val_mul {N : ℕ} (Q R : ExactDivisor N) : (Q * R).val = Q.val * R.val / Q.val.gcd R.val ^ 2

Multiplication of exact divisors is symmetric difference: its underlying value is Q R / gcd(Q, R)².

@[simp]

theorem TauCeti.Nat.ExactDivisor.val_inv {N : ℕ} (Q : ExactDivisor N) : Q⁻¹.val = Q.val

Every exact divisor is its own inverse.

theorem TauCeti.Nat.ExactDivisor.primeFactors_injective {N : ℕ} : Function.Injective fun (Q : ExactDivisor N) => Q.val.primeFactors

An exact divisor of N is determined by the set of primes dividing it.

theorem TauCeti.Nat.ExactDivisor.primeFactors_mul {N : ℕ} (Q R : ExactDivisor N) : (Q * R).val.primeFactors = symmDiff Q.val.primeFactors R.val.primeFactors

Prime factors turn exact-divisor multiplication into symmetric difference.

@[instance_reducible]

instance TauCeti.Nat.ExactDivisor.instCommGroup {N : ℕ} : CommGroup (ExactDivisor N)

Exact divisors form a Boolean commutative group under symmetric-difference multiplication; the identity is 1 and every element is its own inverse.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.Nat.ExactDivisor.primeFactorsEquiv (N : ℕ) : ExactDivisor N ≃ { s : Finset ℕ // s ⊆ N.primeFactors }

The exact divisors of N are exactly the subsets of N.primeFactors. An exact divisor goes to the set of primes dividing it, and a subset s comes back as the product ∏ p ∈ s, p ^ v_p(N) of maximal prime powers. Since primeFactors_mul carries multiplication to symmetric difference and val_inv makes every element its own inverse, this identifies the group of exact divisors with the Boolean group of subsets of N.primeFactors — abstractly (ℤ/2) ^ ω(N), generated by the maximal prime powers p ^ v_p(N).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Nat.ExactDivisor.coe_primeFactorsEquiv {N : ℕ} (Q : ExactDivisor N) : ↑((primeFactorsEquiv N) Q) = Q.val.primeFactors

primeFactorsEquiv sends an exact divisor to its set of prime factors.

@[simp]

theorem TauCeti.Nat.ExactDivisor.val_primeFactorsEquiv_symm {N : ℕ} (s : { s : Finset ℕ // s ⊆ N.primeFactors }) : ((primeFactorsEquiv N).symm s).val = prodPrimePow N ↑s

primeFactorsEquiv recovers an exact divisor from a set of primes as a product of maximal prime powers.