Supernatural numbers

A supernatural number, also called a Steinitz number, is a formal product \prod_p p ^ n_p, where p ranges over the rational primes and every exponent n_p is an extended natural number. This file realizes supernatural numbers as exponent functions and equips them with the arithmetic used for orders and indices of profinite groups.

Multiplication adds exponents, divisibility is pointwise comparison, and gcd and lcm are the lattice infimum and supremum. Positive natural numbers embed by their prime factorizations. The finite supernatural numbers are characterized as those with finite support and no infinite exponent.

Main definitions

• Supernatural: supernatural numbers as prime-indexed extended-natural exponent functions.
• Supernatural.ofFun: the supernatural number with prescribed exponent at each prime.
• Supernatural.ofNat: the supernatural number attached to a positive natural number.
• Supernatural.primePower: the supernatural prime power p ^ n, including p ^ infinity.
• Supernatural.primaryPart: the p-primary part of a supernatural number.
• Supernatural.primeToPart: the prime-to-p part of a supernatural number.
• Supernatural.IsNatural: the predicate that a supernatural number comes from ofNat.

References

This is the Supernatural milestone of Layer 1, "supernatural order and index", of the human-authored roadmap TauCetiRoadmap/ProfiniteProPGroups/README.md, which asks for divisibility as pointwise ≤, multiplication as pointwise +, the lattice operations, the embedding of ℕ+ by prime factorization, the "is a natural number" predicate and the p-primary and prime-to-p parts, together with an API checklist of the multiplicativity, injectivity, gcd/lcm and finite-support statements proved below. The type itself is pinned in that roadmap's Suggested.lean as Supernatural := Nat.Primes → ℕ∞.

The definitions and terminology follow Ribes--Zalesskii, Profinite Groups, Section 2.3.

def TauCeti.Supernatural : Type

A supernatural number is a formal product of rational primes with exponents in \mathbb{N}_∞.

This is a separate type, rather than an abbreviation for a function type, because multiplication of supernatural numbers is pointwise addition of exponents, not the pointwise multiplication a function type carries. As for Mathlib's Matrix, the body of the synonym is exposed, since the operations are pointwise operations of the underlying function type and can only be defined, and their pointwise characterizations only stated, with the synonym transparent. The operations and instances themselves are opaque and are used through the pointwise lemmas below; ofFun is the named constructor building a supernatural number from its exponents.

Equations

• TauCeti.Supernatural = (Nat.Primes → ℕ∞)

@[instance_reducible]

instance TauCeti.Supernatural.instCoeFunForallPrimesENat : CoeFun Supernatural fun (x : Supernatural) => Nat.Primes → ℕ∞

Equations

• TauCeti.Supernatural.instCoeFunForallPrimesENat = { coe := id }

theorem TauCeti.Supernatural.ext {m n : Supernatural} (h : ∀ (p : Nat.Primes), m p = n p) : m = n

Two supernatural numbers are equal when all of their prime exponents are equal.

theorem TauCeti.Supernatural.ext_iff {m n : Supernatural} : m = n ↔ ∀ (p : Nat.Primes), m p = n p

def TauCeti.Supernatural.ofFun (f : Nat.Primes → ℕ∞) : Supernatural

The supernatural number with prescribed exponent at each prime.

This is the named constructor for downstream definitions such as profiniteOrder, playing the role that Matrix.of plays for Matrix.

Equations

• TauCeti.Supernatural.ofFun f = f

@[simp]

theorem TauCeti.Supernatural.ofFun_apply (f : Nat.Primes → ℕ∞) (p : Nat.Primes) : ofFun f p = f p

@[instance_reducible]

noncomputable instance TauCeti.Supernatural.instCompleteLattice : CompleteLattice Supernatural

Equations

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

@[instance_reducible]

instance TauCeti.Supernatural.instOne : One Supernatural

Equations

• TauCeti.Supernatural.instOne = { one := fun (x : Nat.Primes) => 0 }

@[instance_reducible]

instance TauCeti.Supernatural.instMul : Mul Supernatural

Equations

• TauCeti.Supernatural.instMul = { mul := fun (m n : TauCeti.Supernatural) (p : Nat.Primes) => m p + n p }

@[instance_reducible]

instance TauCeti.Supernatural.instCommMonoid : CommMonoid Supernatural

Equations

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

@[simp]

theorem TauCeti.Supernatural.one_apply (p : Nat.Primes) : 1 p = 0

Every exponent of the multiplicative unit is zero.

@[simp]

theorem TauCeti.Supernatural.mul_apply (m n : Supernatural) (p : Nat.Primes) : (m * n) p = m p + n p

@[simp]

theorem TauCeti.Supernatural.pow_apply (m : Supernatural) (n : ℕ) (p : Nat.Primes) : (m ^ n) p = n • m p

Raising to a natural power multiplies every exponent by that power.

@[simp]

theorem TauCeti.Supernatural.inf_apply (m n : Supernatural) (p : Nat.Primes) : (m ⊓ n) p = min (m p) (n p)

@[simp]

theorem TauCeti.Supernatural.sup_apply (m n : Supernatural) (p : Nat.Primes) : (m ⊔ n) p = max (m p) (n p)

@[simp]

theorem TauCeti.Supernatural.top_apply (p : Nat.Primes) : ⊤ p = ⊤

Every exponent of the greatest supernatural number is infinite.

@[simp]

theorem TauCeti.Supernatural.bot_apply (p : Nat.Primes) : ⊥ p = 0

Every exponent of the least supernatural number is zero.

@[simp]

theorem TauCeti.Supernatural.iSup_apply {ι : Sort u_1} (m : ι → Supernatural) (p : Nat.Primes) : (⨆ (i : ι), m i) p = ⨆ (i : ι), m i p

Suprema of supernatural numbers are computed exponentwise.

@[simp]

theorem TauCeti.Supernatural.iInf_apply {ι : Sort u_1} (m : ι → Supernatural) (p : Nat.Primes) : (⨅ (i : ι), m i) p = ⨅ (i : ι), m i p

Infima of supernatural numbers are computed exponentwise.

@[simp]

theorem TauCeti.Supernatural.one_eq_bot : 1 = ⊥

The multiplicative unit is also the least supernatural number.

@[simp]

theorem TauCeti.Supernatural.dvd_iff_le {m n : Supernatural} : m ∣ n ↔ m ≤ n

Divisibility of supernatural numbers is comparison of every prime exponent.

theorem TauCeti.Supernatural.le_iff {m n : Supernatural} : m ≤ n ↔ ∀ (p : Nat.Primes), m p ≤ n p

One supernatural number is at most another exactly when each exponent is at most the corresponding exponent of the other.

theorem TauCeti.Supernatural.dvd_iff {m n : Supernatural} : m ∣ n ↔ ∀ (p : Nat.Primes), m p ≤ n p

A supernatural number divides another exactly when each exponent is at most the corresponding exponent of the other.

def TauCeti.Supernatural.exponent (p : Nat.Primes) : Supernatural →o ℕ∞

The exponent of a supernatural number at a given prime.

Equations

• TauCeti.Supernatural.exponent p = Pi.evalOrderHom p

@[simp]

theorem TauCeti.Supernatural.exponent_apply (p : Nat.Primes) (m : Supernatural) : (exponent p) m = m p

def TauCeti.Supernatural.primePower (p : Nat.Primes) (n : ℕ∞) : Supernatural

The supernatural prime power p ^ n; all exponents away from p are zero.

Equations

• TauCeti.Supernatural.primePower p n = Pi.single p n

@[simp]

theorem TauCeti.Supernatural.primePower_apply_self (p : Nat.Primes) (n : ℕ∞) : primePower p n p = n

@[simp]

theorem TauCeti.Supernatural.primePower_apply_of_ne {p q : Nat.Primes} (h : q ≠ p) (n : ℕ∞) : primePower p n q = 0

@[simp]

theorem TauCeti.Supernatural.primePower_zero (p : Nat.Primes) : primePower p 0 = 1

theorem TauCeti.Supernatural.primePower_injective (p : Nat.Primes) : Function.Injective (primePower p)

A prime power determines its exponent: p ^ m = p ^ n forces m = n.

@[simp]

theorem TauCeti.Supernatural.primePower_add (p : Nat.Primes) (m n : ℕ∞) : primePower p (m + n) = primePower p m * primePower p n

A prime power with a sum of exponents is the product of the two prime powers.

theorem TauCeti.Supernatural.primePower_le_iff (p : Nat.Primes) (m : ℕ∞) (n : Supernatural) : primePower p m ≤ n ↔ m ≤ n p

A prime power p ^ m is at most a supernatural number exactly when m is at most its exponent at p.

@[simp]

theorem TauCeti.Supernatural.primePower_le_primePower_iff (p : Nat.Primes) {m n : ℕ∞} : primePower p m ≤ primePower p n ↔ m ≤ n

Two prime powers at the same prime compare as their exponents do.

@[simp]

theorem TauCeti.Supernatural.primePower_lt_primePower_iff (p : Nat.Primes) {m n : ℕ∞} : primePower p m < primePower p n ↔ m < n

Two prime powers at the same prime compare strictly as their exponents do.

@[instance_reducible]

instance TauCeti.Supernatural.instCoePrimes : Coe Nat.Primes Supernatural

A rational prime, regarded as the supernatural number having exponent one at that prime.

Equations

• TauCeti.Supernatural.instCoePrimes = { coe := fun (p : Nat.Primes) => TauCeti.Supernatural.primePower p 1 }

@[simp]

theorem TauCeti.Supernatural.coe_prime_le_iff (p : Nat.Primes) (n : Supernatural) : primePower p 1 ≤ n ↔ n p ≠ 0

A prime is at most a supernatural number exactly when its exponent there is nonzero.

This is the simp-normal form of coe_prime_dvd_iff, since dvd_iff_le rewrites divisibility of supernatural numbers to comparison.

theorem TauCeti.Supernatural.coe_prime_dvd_iff (p : Nat.Primes) (n : Supernatural) : primePower p 1 ∣ n ↔ n p ≠ 0

A prime divides a supernatural number exactly when its exponent there is nonzero.

def TauCeti.Supernatural.primaryPart (p : Nat.Primes) (n : Supernatural) : Supernatural

The p-primary part of a supernatural number.

Equations

• TauCeti.Supernatural.primaryPart p n = TauCeti.Supernatural.primePower p (n p)

@[simp]

theorem TauCeti.Supernatural.primaryPart_apply_self (p : Nat.Primes) (n : Supernatural) : primaryPart p n p = n p

@[simp]

theorem TauCeti.Supernatural.primaryPart_apply_of_ne {p q : Nat.Primes} (h : q ≠ p) (n : Supernatural) : primaryPart p n q = 0

@[simp]

theorem TauCeti.Supernatural.primaryPart_eq_bot_iff {p : Nat.Primes} {n : Supernatural} : primaryPart p n = ⊥ ↔ n p = 0

The p-primary part of a supernatural number is trivial (equal to ⊥ = 1) exactly when p does not divide it.

def TauCeti.Supernatural.primeToPart (p : Nat.Primes) (n : Supernatural) : Supernatural

The prime-to-p part of a supernatural number, obtained by deleting its p-exponent.

Equations

• TauCeti.Supernatural.primeToPart p n = Function.update n p 0

@[simp]

theorem TauCeti.Supernatural.primeToPart_apply_self (p : Nat.Primes) (n : Supernatural) : primeToPart p n p = 0

@[simp]

theorem TauCeti.Supernatural.primeToPart_apply_of_ne {p q : Nat.Primes} (h : q ≠ p) (n : Supernatural) : primeToPart p n q = n q

theorem TauCeti.Supernatural.primaryPart_mul_primeToPart (p : Nat.Primes) (n : Supernatural) : primaryPart p n * primeToPart p n = n

A supernatural number is the product of its p-primary and prime-to-p parts.

def TauCeti.Supernatural.ofNat (n : ℕ+) : Supernatural

The embedding of positive natural numbers into supernatural numbers by prime factorization.

Equations

• TauCeti.Supernatural.ofNat n p = ↑(padicValNat ↑p ↑n)

@[simp]

theorem TauCeti.Supernatural.ofNat_apply (n : ℕ+) (p : Nat.Primes) : ofNat n p = ↑(padicValNat ↑p ↑n)

@[simp]

theorem TauCeti.Supernatural.ofNat_one : ofNat 1 = 1

@[simp]

theorem TauCeti.Supernatural.ofNat_mul (m n : ℕ+) : ofNat (m * n) = ofNat m * ofNat n

The prime factorization embedding turns multiplication of positive natural numbers into multiplication of supernatural numbers, that is, into addition of exponents.

theorem TauCeti.Supernatural.ofNat_injective : Function.Injective ofNat

Prime factorization embeds positive natural numbers injectively into supernatural numbers.

def TauCeti.Supernatural.ofNatMonoidHom : ℕ+ →* Supernatural

The embedding of positive natural numbers as a multiplicative homomorphism.

Equations

• TauCeti.Supernatural.ofNatMonoidHom = { toFun := TauCeti.Supernatural.ofNat, map_one' := TauCeti.Supernatural.ofNat_one, map_mul' := TauCeti.Supernatural.ofNat_mul }

@[simp]

theorem TauCeti.Supernatural.ofNatMonoidHom_apply (n : ℕ+) : ofNatMonoidHom n = ofNat n

@[simp]

theorem TauCeti.Supernatural.ofNat_le_ofNat_iff {m n : ℕ+} : ofNat m ≤ ofNat n ↔ m ∣ n

Divisibility of positive natural numbers agrees with comparison of their supernatural images.

This is the simp-normal form of ofNat_dvd_ofNat_iff, since dvd_iff_le rewrites divisibility of supernatural numbers to comparison.

theorem TauCeti.Supernatural.ofNat_dvd_ofNat_iff {m n : ℕ+} : ofNat m ∣ ofNat n ↔ m ∣ n

Divisibility of positive natural numbers agrees with divisibility of their supernatural images.

@[simp]

theorem TauCeti.Supernatural.ofNat_gcd (m n : ℕ+) : ofNat (m.gcd n) = ofNat m ⊓ ofNat n

The positive-natural embedding takes gcd to the supernatural gcd.

@[simp]

theorem TauCeti.Supernatural.ofNat_lcm (m n : ℕ+) : ofNat (m.lcm n) = ofNat m ⊔ ofNat n

The positive-natural embedding takes lcm to the supernatural lcm.

def TauCeti.Supernatural.IsNatural (n : Supernatural) : Prop

A supernatural number is natural when it lies in the image of ofNat.

Equations

• n.IsNatural = ∃ (m : ℕ+), TauCeti.Supernatural.ofNat m = n

theorem TauCeti.Supernatural.isNatural_def {n : Supernatural} : n.IsNatural ↔ ∃ (m : ℕ+), ofNat m = n

A supernatural number is natural exactly when it is the image under ofNat of a positive natural number. This is IsNatural by definition, and is the form downstream files use, since the body of IsNatural is not exposed.

@[simp]

theorem TauCeti.Supernatural.isNatural_ofNat (n : ℕ+) : (ofNat n).IsNatural

Every positive natural number gives a natural supernatural number.

def TauCeti.Supernatural.support (n : Supernatural) : Set Nat.Primes

The support of a supernatural number is the set of primes having nonzero exponent.

Equations

• n.support = Function.support n

@[simp]

theorem TauCeti.Supernatural.mem_support {n : Supernatural} {p : Nat.Primes} : p ∈ n.support ↔ n p ≠ 0

theorem TauCeti.Supernatural.isNatural_iff {n : Supernatural} : n.IsNatural ↔ n.support.Finite ∧ ∀ (p : Nat.Primes), n p ≠ ⊤

A supernatural number comes from a positive natural number exactly when it has finite support and every exponent is finite.

@[simp]

theorem TauCeti.Supernatural.not_isNatural_primePower_top (p : Nat.Primes) : ¬(primePower p ⊤).IsNatural

A prime power with infinite exponent is not a natural supernatural number.