structure InverseLimit.NatInverseSystem : Type (u_1 + 1)

A countable inverse system: a sequence of types obj n together with transition maps map n : obj (n + 1) → obj n.

• obj : ℕ → Type u_1
• map (n : ℕ) : self.obj (n + 1) → self.obj n

def InverseLimit.NatInverseSystem.InverseLimit (S : NatInverseSystem) : Type u_1

The inverse limit of a NatInverseSystem $S$: coherent sequences $(a_n)$ with $a_n \in S_n$ and $S.\mathrm{map}\,n\,(a_{n+1}) = a_n$.

def InverseLimit.NatInverseSystem.proj (S : NatInverseSystem) (n : ℕ) (a : S.InverseLimit) : S.obj n

Canonical projection $\mathrm{proj}_n : \mathrm{InverseLimit}\,S \to S_n$.

theorem InverseLimit.NatInverseSystem.ext (S : NatInverseSystem) {a b : S.InverseLimit} (h : ∀ (n : ℕ), S.proj n a = S.proj n b) : a = b

Extensionality: two elements of the inverse limit agree iff they agree in every projection.

theorem InverseLimit.NatInverseSystem.ext_iff {S : NatInverseSystem} {a b : S.InverseLimit} : a = b ↔ ∀ (n : ℕ), S.proj n a = S.proj n b

def InverseLimit.NatInverseSystem.lift (S : NatInverseSystem) {X : Type u_1} (g : (n : ℕ) → X → S.obj n) (hg : ∀ (n : ℕ) (x : X), S.map n (g (n + 1) x) = g n x) : X → S.InverseLimit

Universal property (lift): a compatible family g n : X → S.obj n factors through the inverse limit.

theorem InverseLimit.NatInverseSystem.proj_lift (S : NatInverseSystem) {X : Type u_1} (g : (n : ℕ) → X → S.obj n) (hg : ∀ (n : ℕ) (x : X), S.map n (g (n + 1) x) = g n x) (n : ℕ) (x : X) : S.proj n (S.lift g hg x) = g n x

Computational rule for lift: projecting the lifted map recovers the original family.

theorem InverseLimit.NatInverseSystem.lift_unique (S : NatInverseSystem) {X : Type u_1} (g : (n : ℕ) → X → S.obj n) (hg : ∀ (n : ℕ) (x : X), S.map n (g (n + 1) x) = g n x) (φ : X → S.InverseLimit) (hφ : ∀ (n : ℕ) (x : X), S.proj n (φ x) = g n x) : φ = S.lift g hg

Uniqueness of the lift: any map into the inverse limit whose projections agree with g is equal to S.lift g hg.

structure InverseLimit.NatRingInverseSystem : Type (u_1 + 1)

A countable inverse system of commutative rings: a sequence of CommRings with ring homomorphism transition maps.

• obj : ℕ → Type u_1
• instCommRing (n : ℕ) : CommRing (self.obj n)
• map (n : ℕ) : self.obj (n + 1) →+* self.obj n

def InverseLimit.NatRingInverseSystem.toNatInverseSystem (S : NatRingInverseSystem) : NatInverseSystem

Forget the ring structure on a NatRingInverseSystem, viewing it as a NatInverseSystem.

def InverseLimit.NatRingInverseSystem.invLimSubring (S : NatRingInverseSystem) : Subring ((n : ℕ) → S.obj n)

The inverse limit of a NatRingInverseSystem realized as a subring of the product $\prod_n S_n$, consisting of coherent sequences.

@[reducible, inline]

abbrev InverseLimit.NatRingInverseSystem.InverseLimitRing (S : NatRingInverseSystem) : Type u_1

The inverse limit of a NatRingInverseSystem as a commutative ring (alias for the subring invLimSubring).

@[implicit_reducible]

instance InverseLimit.NatRingInverseSystem.instCommRingInverseLimitRing (S : NatRingInverseSystem) : CommRing S.InverseLimitRing

def InverseLimit.NatRingInverseSystem.projRingHom (S : NatRingInverseSystem) (n : ℕ) : S.InverseLimitRing →+* S.obj n

The $n$-th projection ring homomorphism InverseLimitRing →+* S.obj n.

noncomputable def InverseLimit.zmodInverseSystem (p : ℕ) [Fact (Nat.Prime p)] : NatInverseSystem

The NatInverseSystem whose $n$-th object is $\mathbb{Z}/p^{n+1}\mathbb{Z}$ and whose transition maps are reduction modulo $p^{n+1}$ to $p^n$.

noncomputable def InverseLimit.zmodRingInverseSystem (p : ℕ) [Fact (Nat.Prime p)] : NatRingInverseSystem

The NatRingInverseSystem whose $n$-th object is the commutative ring $\mathbb{Z}/p^{n+1}\mathbb{Z}$ with reduction ring homomorphisms.

@[implicit_reducible]

noncomputable instance InverseLimit.instCommRingInverseLimitRingZmodRingInverseSystem (p : ℕ) [Fact (Nat.Prime p)] : CommRing (zmodRingInverseSystem p).InverseLimitRing

structure DiscreteValuation (R : Type u_1) [CommRing R] : Type u_1

Definition 4.18 (discrete valuation): a function $v : R \to \mathbb{Z} \cup \{\infty\}$ satisfying $v(a) = \infty \iff a = 0$, $v(ab) = v(a) + v(b)$, and the ultrametric inequality $\min(v(a), v(b)) \le v(a + b)$.

• val : R → WithTop ℤ
• val : R → WithTop ℤ
• val : R → WithTop ℤ
• val_eq_top_iff (a : R) : self.val a = ⊤ ↔ a = 0
• val_mul (a b : R) : self.val (a * b) = self.val a + self.val b
• val_add (a b : R) : min (self.val a) (self.val b) ≤ self.val (a + b)

@[implicit_reducible]

instance DiscreteValuation.instCoeFunForallWithTopInt {R : Type u_1} [CommRing R] : CoeFun (DiscreteValuation R) fun (x : DiscreteValuation R) => R → WithTop ℤ

@[simp]

theorem DiscreteValuation.coe_mk {R : Type u_1} [CommRing R] (f : R → WithTop ℤ) (h1 : ∀ (a : R), f a = ⊤ ↔ a = 0) (h2 : ∀ (a b : R), f (a * b) = f a + f b) (h3 : ∀ (a b : R), min (f a) (f b) ≤ f (a + b)) : { val := f, val_eq_top_iff := h1, val_mul := h2, val_add := h3 }.val = f

Definitional unfolding: the coercion of the anonymous constructor ⟨f, h1, h2, h3⟩ to a function is f itself.

theorem DiscreteValuation.ext {R : Type u_1} [CommRing R] {v w : DiscreteValuation R} (h : ∀ (x : R), v.val x = w.val x) : v = w

Extensionality for discrete valuations: agreement pointwise on $R$ implies equality.

theorem DiscreteValuation.ext_iff {R : Type u_1} [CommRing R] {v w : DiscreteValuation R} : v = w ↔ ∀ (x : R), v.val x = w.val x

@[simp]

theorem DiscreteValuation.val_zero {R : Type u_1} [CommRing R] (v : DiscreteValuation R) : v.val 0 = ⊤

A discrete valuation sends $0$ to $\infty$.

def PadicIntegers.zmodInvLimSubring (p : ℕ) : Subring ((n : ℕ) → ZMod (p ^ n))

The subring of $\prod_n \mathbb{Z}/p^n\mathbb{Z}$ consisting of compatible sequences with respect to all reduction maps $\mathbb{Z}/p^n\mathbb{Z} \to \mathbb{Z}/p^m\mathbb{Z}$ for $m \le n$. This is the explicit inverse-limit model for $\mathbb{Z}_p$.

def PadicIntegers.invLimProj (p n : ℕ) : ↥(zmodInvLimSubring p) →+* ZMod (p ^ n)

The $n$-th projection ring homomorphism from zmodInvLimSubring to $\mathbb{Z}/p^n\mathbb{Z}$.

theorem PadicIntegers.invLimProj_compat (p m n : ℕ) (h : m ≤ n) : (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (invLimProj p n) = invLimProj p m

Compatibility of the projections: the reduction $\mathbb{Z}/p^n\mathbb{Z} \to \mathbb{Z}/p^m\mathbb{Z}$ composed with invLimProj p n equals invLimProj p m for $m \le n$.

noncomputable def PadicIntegers.padicIntToInvLim (p : ℕ) [hp : Fact (Nat.Prime p)] : ℤ_[p] →+* ↥(zmodInvLimSubring p)

Forward map of the isomorphism $\mathbb{Z}_p \simeq \varprojlim \mathbb{Z}/p^n\mathbb{Z}$: sends $x \in \mathbb{Z}_p$ to the compatible sequence of its reductions modulo $p^n$.

def PadicIntegers.invLimToPadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : ↥(zmodInvLimSubring p) →+* ℤ_[p]

Inverse map of the isomorphism $\mathbb{Z}_p \simeq \varprojlim \mathbb{Z}/p^n\mathbb{Z}$: obtained via the universal property PadicInt.lift from the family of compatible projections.

noncomputable def PadicIntegers.padicIntEquivInvLim (p : ℕ) [hp : Fact (Nat.Prime p)] : ℤ_[p] ≃+* ↥(zmodInvLimSubring p)

Theorem 4.6 (inverse-limit description): the ring isomorphism $\mathbb{Z}_p \simeq \varprojlim_n \mathbb{Z}/p^n\mathbb{Z}$.

@[implicit_reducible]

instance PadicIntegers.instCommRingSubtypeForallZModHPowNatMemSubringZmodInvLimSubring (p : ℕ) : CommRing ↥(zmodInvLimSubring p)

@[reducible]

noncomputable def PadicIntegers.padicInt_commRing (p : ℕ) [hp : Fact (Nat.Prime p)] : CommRing ℤ_[p]

Reducible alias for the commutative ring structure on $\mathbb{Z}_p$.

@[reducible, inline]

abbrev PadicUnits.padicUnits (p : ℕ) [Fact (Nat.Prime p)] : Type

The group of units of $\mathbb{Z}_p$, abbreviated padicUnits p.

@[implicit_reducible]

noncomputable instance PadicUnits.instGroupPadicUnits (p : ℕ) [Fact (Nat.Prime p)] : Group (padicUnits p)

@[implicit_reducible]

noncomputable instance PadicUnits.instCommGroupPadicUnits (p : ℕ) [Fact (Nat.Prime p)] : CommGroup (padicUnits p)

noncomputable def PadicInt.padicDigit {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : ℕ

The $n$-th digit in the $p$-adic expansion of $a \in \mathbb{Z}_p$, defined via the PadicInt.appr natural-number approximation.

theorem PadicInt.padicDigit_lt {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : a.padicDigit n < p

Each $p$-adic digit lies in $\{0, 1, \ldots, p-1\}$.

noncomputable def PadicInt.padicExpansion {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : Fin p

The $p$-adic expansion of $a \in \mathbb{Z}_p$ as a sequence valued in Fin p, packaging padicDigit together with the bound padicDigit_lt.

theorem PadicInt.padicDigit_mul_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : a.padicDigit n * p ^ n = a.appr (n + 1) - a.appr n

Reconstruction relation: the digit times $p^n$ equals the difference of consecutive approximations of $a$.

theorem PadicInt.appr_succ_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : a.appr (n + 1) = a.appr n + a.padicDigit n * p ^ n

Successor relation for approximations: $a_{n+1} = a_n + d_n \cdot p^n$, where $d_n$ is the $n$-th $p$-adic digit.

theorem PadicInt.appr_eq_sum_padicDigit {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : a.appr n = ∑ k ∈ Finset.range n, a.padicDigit k * p ^ k

Closed-form for the approximation: $a_n = \sum_{k<n} d_k\,p^k$.

noncomputable def PadicInt.digitPartialSum {p : ℕ} (b : ℕ → Fin p) (n : ℕ) : ℤ

Given a sequence of digits $b : \mathbb{N} \to \mathrm{Fin}\,p$, the partial sum $\sum_{k<n} b_k\,p^k \in \mathbb{Z}$.

theorem PadicInt.digitPartialSum_nonneg {p : ℕ} (b : ℕ → Fin p) (n : ℕ) : 0 ≤ digitPartialSum b n

The digit partial sum is nonnegative.

theorem PadicInt.digitPartialSum_lt {p : ℕ} (b : ℕ → Fin p) (n : ℕ) : digitPartialSum b n < ↑p ^ n

The partial sum is strictly bounded by $p^n$.

theorem PadicInt.padicExpansion_surjective {p : ℕ} [hp : Fact (Nat.Prime p)] (b : ℕ → Fin p) : ∃ (x : ℤ_[p]), ∀ (n : ℕ), x.padicExpansion n = b n

Surjectivity of padicExpansion: every sequence $(b_n)_{n \in \mathbb{N}}$ with $b_n \in \{0, \ldots, p - 1\}$ arises as the digit sequence of some $x \in \mathbb{Z}_p$.

theorem PadicInt.padicExpansion_injective {p : ℕ} [hp : Fact (Nat.Prime p)] : Function.Injective padicExpansion

Injectivity of padicExpansion: two $p$-adic integers with the same digit sequence are equal.

theorem PadicInt.padicExpansion_bijective {p : ℕ} [hp : Fact (Nat.Prime p)] : Function.Bijective padicExpansion

Theorem 4.6 (bijection between $p$-adic expansions and $\mathbb{Z}_p$): the digit-extraction map padicExpansion : ℤ_[p] → (ℕ → Fin p) is a bijection.

theorem IsDiscreteValuationRing.isPrincipalIdealRing (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsPrincipalIdealRing R

A discrete valuation ring is a principal ideal ring.

theorem IsDiscreteValuationRing.isLocalRing (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsLocalRing R

A discrete valuation ring is a local ring.

theorem PadicInt.isDiscreteValuationRing (p : ℕ) [Fact (Nat.Prime p)] : IsDiscreteValuationRing ℤ_[p]

$\mathbb{Z}_p$ is a discrete valuation ring.

theorem PadicInt.toZModPow_surjective {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : Function.Surjective ⇑(toZModPow m)

The reduction $\mathbb{Z}_p \twoheadrightarrow \mathbb{Z}/p^m\mathbb{Z}$ is surjective.

theorem PadicInt.exact_mul_pow_p_toZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : (Set.range fun (a : ℤ_[p]) => ↑p ^ m * a) = ↑(RingHom.ker (toZModPow m))

Exactness statement: the image of multiplication by $p^m$ on $\mathbb{Z}_p$ coincides with the kernel of the reduction toZModPow m.

noncomputable def PadicInt.quotientSpanPowPEquivZMod {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : ℤ_[p] ⧸ Ideal.span {↑p ^ m} ≃+* ZMod (p ^ m)

Ring isomorphism $\mathbb{Z}_p / (p^m) \simeq \mathbb{Z}/p^m\mathbb{Z}$ obtained from the first isomorphism theorem applied to toZModPow m.

noncomputable def PadicInt.corollary_4_9 (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : ℤ_[p] ⧸ Ideal.span {↑p ^ m} ≃+* ZMod (p ^ m)

Corollary 4.9: the ring isomorphism $\mathbb{Z}_p / (p^m) \simeq \mathbb{Z}/p^m\mathbb{Z}$.

noncomputable def padicValuationDef {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) : WithTop ℕ

The $p$-adic valuation on $\mathbb{Z}_p$ extended to $\mathbb{N} \cup \{\infty\}$: $v(0) = \infty$ and $v(a) = \mathrm{PadicInt.valuation}(a)$ otherwise.

@[simp]

theorem padicValuationDef_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : padicValuationDef 0 = ⊤

$v(0) = \infty$.

@[simp]

theorem padicValuationDef_of_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ_[p]} (ha : a ≠ 0) : padicValuationDef a = ↑a.valuation

For nonzero $a$, the extended valuation agrees with the natural-number-valued PadicInt.valuation.

theorem padicValuationDef_ne_top {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ_[p]} (ha : a ≠ 0) : padicValuationDef a ≠ ⊤

A nonzero $p$-adic integer has finite valuation.

theorem padicValuationDef_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ℤ_[p]} (ha : a ≠ 0) (hb : b ≠ 0) : padicValuationDef (a * b) = padicValuationDef a + padicValuationDef b

Multiplicativity of the valuation: $v(ab) = v(a) + v(b)$ when both $a, b$ are nonzero.

theorem padicValuationDef_add {p : ℕ} [hp : Fact (Nat.Prime p)] (a b : ℤ_[p]) : min (padicValuationDef a) (padicValuationDef b) ≤ padicValuationDef (a + b)

Ultrametric inequality: $\min(v(a), v(b)) \le v(a + b)$.

theorem PadicInt.isDomain (p : ℕ) [Fact (Nat.Prime p)] : IsDomain ℤ_[p]

Corollary 4.13 (part): $\mathbb{Z}_p$ is an integral domain.

theorem unit_valuation_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) : (↑u).valuation = 0

Any unit of $\mathbb{Z}_p$ has valuation $0$.

theorem thm_4_15_units_valuation {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (ha : a ≠ 0) : IsUnit a ↔ a.valuation = 0

Theorem 4.15 (units): a nonzero $a \in \mathbb{Z}_p$ is a unit if and only if its valuation is zero.

theorem thm_4_15_unique_factorization {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (ha : a ≠ 0) : ∃! nu : ℕ × ℤ_[p]ˣ, a = ↑p ^ nu.1 * ↑nu.2

Theorem 4.15 (unique factorization): every nonzero $a \in \mathbb{Z}_p$ admits a unique factorization $a = p^n \cdot u$ with $n \in \mathbb{N}$ and $u \in \mathbb{Z}_p^\times$.

theorem thm_4_16_nonzero_ideal_span_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (I : Ideal ℤ_[p]) (hI : I ≠ ⊥) : ∃ (m : ℕ), I = Ideal.span {↑p ^ m}

Theorem 4.16: every nonzero ideal of $\mathbb{Z}_p$ is of the form $(p^m)$ for some $m \in \mathbb{N}$.

theorem PadicInt.isPrincipalIdealRing (p : ℕ) [Fact (Nat.Prime p)] : IsPrincipalIdealRing ℤ_[p]

Corollary 4.17 (part): $\mathbb{Z}_p$ is a principal ideal ring.

theorem PadicInt.isLocalRing (p : ℕ) [Fact (Nat.Prime p)] : IsLocalRing ℤ_[p]

Corollary 4.17 (part): $\mathbb{Z}_p$ is a local ring.