This file records the elementary rational factorization needed for the principal-idele calculation over ℚ. At a fixed rational prime p, removing the p-power from x : ℚˣ leaves the sign of x times the finite product of the powers of all primes different from p.
The last declarations package rational p-adic units as units of ℤ_[p] and identify the reduction of a natural unit modulo p ^ k.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocityinstance (p : Nat.Primes) : Fact p.1.PrimeA finite set containing every prime occurring in the numerator or denominator of x, as well as the distinguished prime p.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalPrimeFactorizationSupport
(x : ℚˣ) (p : Nat.Primes) : Finset ℕSurrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem mem_rationalPrimeFactorizationSupport
(x : ℚˣ) (p : Nat.Primes) :
p.1 ∈ rationalPrimeFactorizationSupport x pThe rational p-adic unit part of x: multiply x by the inverse of its p-power.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalPrimeUnit (x : ℚˣ) (p : Nat.Primes) : ℚˣSurrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalPrimeUnit_val (x : ℚˣ) (p : Nat.Primes) :
(rationalPrimeUnit x p : ℚ) =
(p.1 : ℚ) ^ (-padicValRat p.1 (x : ℚ)) * (x : ℚ)Removing the p-power from a nonzero rational number leaves p-adic valuation zero.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicValRat_rationalPrimeUnit
(x : ℚˣ) (p : Nat.Primes) :
padicValRat p.1 (rationalPrimeUnit x p : ℚ) = 0The ordinary prime factorization of a nonzero rational number, over the finite support chosen by rationalPrimeFactorizationSupport.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rational_factorization_over_support
(x : ℚˣ) (p : Nat.Primes) :
(x : ℚ) =
(((x : ℚ).num.sign : ℤ) : ℚ) *
∏ q ∈ rationalPrimeFactorizationSupport x p,
(q : ℚ) ^ padicValRat q (x : ℚ)The p-adic unit part of x is its sign times the finite product of q ^ padicValRat q x over the primes q ≠ p.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalPrimeUnit_factorization
(x : ℚˣ) (p : Nat.Primes) :
(rationalPrimeUnit x p : ℚ) =
(((x : ℚ).num.sign : ℤ) : ℚ) *
∏ q ∈ (rationalPrimeFactorizationSupport x p).erase p.1,
(q : ℚ) ^ padicValRat q (x : ℚ)A nonzero rational number of p-adic valuation zero, regarded as a unit of the p-adic integers.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def padicIntUnitOfRat
(p : Nat.Primes) (y : ℚ)
(hy : y ≠ 0) (hval : padicValRat p.1 y = 0) :
ℤ_[p.1]ˣThe underlying p-adic number of padicIntUnitOfRat is the original rational number.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicIntUnitOfRat_coe
(p : Nat.Primes) (y : ℚ)
(hy : y ≠ 0) (hval : padicValRat p.1 y = 0) :
(((padicIntUnitOfRat p y hy hval : ℤ_[p.1]) : ℚ_[p.1])) =
(y : ℚ_[p.1])The sign of a nonzero rational numerator is a unit at every finite prime.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicValRat_rational_num_sign
(x : ℚˣ) (p : Nat.Primes) :
padicValRat p.1 ((((x : ℚ).num.sign : ℤ) : ℚ)) = 0The actual sign of x, regarded as a unit of the p-adic integers.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalSignPadicUnit
(x : ℚˣ) (p : Nat.Primes) : ℤ_[p.1]ˣThe underlying p-adic number of rationalSignPadicUnit is the sign of the rational numerator.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalSignPadicUnit_coe
(x : ℚˣ) (p : Nat.Primes) :
(((rationalSignPadicUnit x p : ℤ_[p.1]) : ℚ_[p.1])) =
(((((x : ℚ).num.sign : ℤ) : ℚ) : ℚ_[p.1]))The value in ℤ_[p] of rationalSignPadicUnit is the integer sign.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalSignPadicUnit_val
(x : ℚˣ) (p : Nat.Primes) :
(rationalSignPadicUnit x p : ℤ_[p.1]) =
((x : ℚ).num.sign : ℤ)The rational sign unit has square one.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalSignPadicUnit_sq
(x : ℚˣ) (p : Nat.Primes) :
rationalSignPadicUnit x p ^ 2 = 1Reduction of the rational sign unit modulo p ^ k has the expected integer value.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalSignPadicUnit_toZModPow_val
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
((Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p) :
(ZMod (p.1 ^ k))ˣ) : ZMod (p.1 ^ k)) =
((x : ℚ).num.sign : ℤ)Reduction of the rational sign unit still has square one.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalSignPadicUnit_toZModPow_sq
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p) ^ 2 =
1A natural number prime to p, regarded as a unit of ℤ_[p].
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def padicNatUnit
(p : Nat.Primes) (q : ℕ) (h : p.1.Coprime q) :
ℤ_[p.1]ˣSurrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicNatUnit_val
(p : Nat.Primes) (q : ℕ) (h : p.1.Coprime q) :
(padicNatUnit p q h : ℤ_[p.1]) = qReducing the canonical p-adic unit attached to q modulo p ^ k gives the canonical unit represented by q in ZMod (p ^ k).
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicNatUnit_toZModPow
(p : Nat.Primes) (q k : ℕ) (h : p.1.Coprime q) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(padicNatUnit p q h) =
ZMod.unitOfCoprime q (h.symm.pow_right k)The successor of p is a p-adic unit.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicValRat_rationalPrime_succ
(p : Nat.Primes) :
padicValRat p.1 (((p.1 + 1 : ℕ) : ℚ)) = 0A positive natural number greater than one, prime to p, gives a genuine non-torsion unit of ℤ_[p].
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicNatUnit_not_isOfFinOrder_of_one_lt
(p : Nat.Primes) (n : ℕ)
(hcoprime : p.1.Coprime n)
(hn : 1 < n) :
¬ IsOfFinOrder (padicNatUnit p n hcoprime)Every member of the rational factorization support is prime.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem prime_of_mem_rationalPrimeFactorizationSupport
(x : ℚˣ) (p : Nat.Primes) {q : ℕ}
(hq : q ∈ rationalPrimeFactorizationSupport x p) :
q.PrimeThe canonical embedding of the natural-number factorization support into the type of natural primes.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalPrimeFactorizationSupportEmbedding
(x : ℚˣ) (p : Nat.Primes) :
↥(rationalPrimeFactorizationSupport x p) ↪ Nat.Primes where
toFun q :=
⟨q.1,
prime_of_mem_rationalPrimeFactorizationSupport
x p q.2⟩
inj' q r h := by
apply Subtype.ext
exact
congrArg (fun z : Nat.Primes => (z : ℕ)) hThe factorization support as an actual finite set of Nat.Primes.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalPrimeFactorizationPrimeSupport
(x : ℚˣ) (p : Nat.Primes) : Finset Nat.PrimesMembership in the prime-valued support is exactly membership of the underlying natural number in the original support.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem mem_rationalPrimeFactorizationPrimeSupport_iff
(x : ℚˣ) (p : Nat.Primes) (q : Nat.Primes) :
q ∈ rationalPrimeFactorizationPrimeSupport x p ↔
q.1 ∈ rationalPrimeFactorizationSupport x pThe distinguished prime belongs to the prime-valued support.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem mem_rationalPrimeFactorizationPrimeSupport
(x : ℚˣ) (p : Nat.Primes) :
p ∈ rationalPrimeFactorizationPrimeSupport x pErasing p commutes with passing from natural-number support to prime-valued support.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem mem_rationalPrimeFactorizationPrimeSupport_erase_iff
(x : ℚˣ) (p q : Nat.Primes) :
q ∈ (rationalPrimeFactorizationPrimeSupport x p).erase p ↔
q.1 ∈ (rationalPrimeFactorizationSupport x p).erase p.1The canonical prime associated with an element of the erased natural support.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalPrimeOfMemFactorizationSupportErase
(x : ℚˣ) (p : Nat.Primes)
(q : ↥((rationalPrimeFactorizationSupport x p).erase p.1)) :
Nat.PrimesThe erased natural support and the erased prime-valued support have canonically equivalent element types.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalPrimeFactorizationSupportEraseEquiv
(x : ℚˣ) (p : Nat.Primes) :
↥((rationalPrimeFactorizationSupport x p).erase p.1) ≃
↥((rationalPrimeFactorizationPrimeSupport x p).erase p) where
toFun q :=
⟨rationalPrimeOfMemFactorizationSupportErase x p q,
(mem_rationalPrimeFactorizationPrimeSupport_erase_iff
x p _).2 q.2⟩
invFun q :=
⟨q.1.1,
(mem_rationalPrimeFactorizationPrimeSupport_erase_iff
x p q.1).1 q.2⟩
left_inv q := by
apply Subtype.ext
rfl
right_inv q := by
apply Subtype.ext
apply Subtype.ext
rflA prime in the support with p erased is coprime to p.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem coprime_of_mem_rationalPrimeFactorizationSupport_erase
(x : ℚˣ) (p : Nat.Primes) {q : ℕ}
(hq :
q ∈ (rationalPrimeFactorizationSupport x p).erase p.1) :
p.1.Coprime qThe rational prime-unit factorization, lifted from ℚ to an exact identity of units of ℤ_[p].
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicIntUnitOfRat_rationalPrimeUnit_factorization
(x : ℚˣ) (p : Nat.Primes) :
padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p) =
rationalSignPadicUnit x p *
∏ q :
↥((rationalPrimeFactorizationSupport x p).erase p.1),
(padicNatUnit p q.1
(coprime_of_mem_rationalPrimeFactorizationSupport_erase
x p q.2)) ^
padicValRat q.1 (x : ℚ)The rational prime-unit factorization after reduction modulo p ^ k.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicIntUnitOfRat_rationalPrimeUnit_toZModPow
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p)) =
Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p) *
∏ q :
↥((rationalPrimeFactorizationSupport x p).erase p.1),
(ZMod.unitOfCoprime q.1
((coprime_of_mem_rationalPrimeFactorizationSupport_erase
x p q.2).symm.pow_right k)) ^
padicValRat q.1 (x : ℚ)Multiplying the reduced rational prime-unit by the inverse powers of all prime factors away from p recovers the reduced sign.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicIntUnitOfRat_rationalPrimeUnit_mul_inverseFactors_toZModPow
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p)) *
∏ q :
↥((rationalPrimeFactorizationSupport x p).erase p.1),
(ZMod.unitOfCoprime q.1
((coprime_of_mem_rationalPrimeFactorizationSupport_erase
x p q.2).symm.pow_right k)) ^
(-padicValRat q.1 (x : ℚ)) =
Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p)Prime-valued support form of the reduced rational product formula. The direct p-adic unit factor times all inverse away-from-p factors is the reduced rational sign.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem
padicIntUnitOfRat_rationalPrimeUnit_mul_primeSupportInverseFactors_toZModPow
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p)) *
∏ q :
↥((rationalPrimeFactorizationPrimeSupport x p).erase p),
(ZMod.unitOfCoprime q.1.1
((coprime_of_mem_rationalPrimeFactorizationSupport_erase
x p
((mem_rationalPrimeFactorizationPrimeSupport_erase_iff
x p q.1).1 q.2)).symm.pow_right k)) ^
(-padicValRat q.1.1 (x : ℚ)) =
Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p)Multiplication by the reduced sign cancels the sign in the reduced prime-unit factorization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalSignPadicUnit_mul_primeUnit_toZModPow
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p) *
Units.map (PadicInt.toZModPow k).toMonoidHom
(padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p)) =
∏ q :
↥((rationalPrimeFactorizationSupport x p).erase p.1),
(ZMod.unitOfCoprime q.1
((coprime_of_mem_rationalPrimeFactorizationSupport_erase
x p q.2).symm.pow_right k)) ^
padicValRat q.1 (x : ℚ)Inverse/cancellation form of the reduced prime-unit factorization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem padicIntUnitOfRat_rationalPrimeUnit_toZModPow_inv_mul
(x : ℚˣ) (p : Nat.Primes) (k : ℕ) :
(Units.map (PadicInt.toZModPow k).toMonoidHom
(padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p)))⁻¹ *
(Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalSignPadicUnit x p) *
∏ q :
↥((rationalPrimeFactorizationSupport x p).erase p.1),
(ZMod.unitOfCoprime q.1
((coprime_of_mem_rationalPrimeFactorizationSupport_erase
x p q.2).symm.pow_right k)) ^
padicValRat q.1 (x : ℚ)) =
1