def InverseLimit (S : ℕ → Type u) (f : (n : ℕ) → S (n + 1) → S n) : Type u

The inverse limit of a sequence of types $S_0, S_1, \ldots$ connected by transition maps $f_n : S_{n+1} \to S_n$: a coherent sequence $(s_n)_{n \in \mathbb{N}}$ with $s_n \in S_n$ and $f_n(s_{n+1}) = s_n$ for every $n$.

def InverseLimit.imgCh {S : ℕ → Type u} (fn : (n : ℕ) → S (n + 1) → S n) (n k : ℕ) : Set (S n)

The $k$-fold image chain imgCh fn n k: the subset of $S_n$ obtained by iterating the transition maps $k$ times starting from $S_{n+k}$. Forms an antitone family in $k$ that captures which elements of $S_n$ lift back through the inverse system.

theorem InverseLimit.imgCh_succ_subset {S : ℕ → Type u} (fn : (n : ℕ) → S (n + 1) → S n) (n k : ℕ) : imgCh fn n (k + 1) ⊆ imgCh fn n k

The image chains are nested: imgCh fn n (k+1) ⊆ imgCh fn n k.

theorem InverseLimit.imgCh_antitone {S : ℕ → Type u} (fn : (n : ℕ) → S (n + 1) → S n) (n : ℕ) : Antitone (imgCh fn n)

The image chains imgCh fn n k form an antitone family in $k$.

theorem InverseLimit.imgCh_nonempty {S : ℕ → Type u} (fn : (n : ℕ) → S (n + 1) → S n) [∀ (n : ℕ), Nonempty (S n)] (n k : ℕ) : (imgCh fn n k).Nonempty

If every $S_n$ is nonempty, every image chain imgCh fn n k is nonempty.

theorem InverseLimit.nat_antitone_stabilizes {g : ℕ → ℕ} (hg : Antitone g) : ∃ (N : ℕ), ∀ (k : ℕ), N ≤ k → g k = g N

Any antitone function $g : \mathbb{N} \to \mathbb{N}$ eventually stabilizes: there exists $N$ such that $g(k) = g(N)$ for all $k \ge N$.

theorem InverseLimit.iInter_nonempty_of_antitone {α : Type u} [Fintype α] {T : ℕ → Set α} (hanti : Antitone T) (hne : ∀ (k : ℕ), (T k).Nonempty) : (⋂ (k : ℕ), T k).Nonempty

Finite König-style lemma: an antitone family of nonempty subsets of a finite type has nonempty intersection.

theorem InverseLimit.surjective_on_eventual_image {S : ℕ → Type u} (fn : (n : ℕ) → S (n + 1) → S n) [(n : ℕ) → Fintype (S n)] [∀ (n : ℕ), Nonempty (S n)] (n : ℕ) (x : S n) (hx : x ∈ ⋂ (k : ℕ), imgCh fn n k) : ∃ y ∈ ⋂ (k : ℕ), imgCh fn (n + 1) k, fn n y = x

Lifting step in the König argument: any element of $S_n$ in every image chain at level $n$ has a preimage in $S_{n+1}$ that itself lies in every image chain at level $n+1$.

theorem InverseLimit.nonempty (S : ℕ → Type u) (fn : (n : ℕ) → S (n + 1) → S n) [(n : ℕ) → Fintype (S n)] [∀ (n : ℕ), Nonempty (S n)] : Nonempty (InverseLimit S fn)

Lemma 8.3 (König's lemma): an inverse system $(S_n, f_n)$ of nonempty finite types has nonempty inverse limit. The compatible sequence is built recursively by choosing preimages that remain in the stable image chain at each level.

def PolyRootSet {p : ℕ} [hp : Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) (n : ℕ) : Type

The finite set of roots of $f \in \mathbb{Z}_p[X]$ in the quotient ring $\mathbb{Z}/p^n\mathbb{Z}$, i.e. roots of the reduction of $f$ modulo $p^n$.

@[implicit_reducible]

noncomputable instance polyRootSetFintype {p : ℕ} [hp : Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) (n : ℕ) : Fintype (PolyRootSet f n)

PolyRootSet f n is a finite type, being a subtype of the finite ring $\mathbb{Z}/p^n\mathbb{Z}$.

def polyRootReduction {p : ℕ} [hp : Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) (n : ℕ) : PolyRootSet f (n + 1) → PolyRootSet f n

Transition map from roots of $f \bmod p^{n+1}$ to roots of $f \bmod p^n$, given by reducing the representative modulo $p^n$. Makes (PolyRootSet f, polyRootReduction f) into an inverse system.

theorem polyRootReduction_val {p : ℕ} [hp : Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) (n : ℕ) (x : PolyRootSet f (n + 1)) : ↑(polyRootReduction f n x) = (ZMod.castHom ⋯ (ZMod (p ^ n))) ↑x

The underlying value of polyRootReduction f n x is the cast of x.val from $\mathbb{Z}/p^{n+1}\mathbb{Z}$ to $\mathbb{Z}/p^n\mathbb{Z}$.

theorem padic_poly_root_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) : (∃ (a : ℤ_[p]), Polynomial.eval a f = 0) ↔ ∀ (n : ℕ), ∃ (r : ZMod (p ^ n)), Polynomial.eval r (Polynomial.map (PadicInt.toZModPow n) f) = 0

Theorem 8.4: a polynomial $f \in \mathbb{Z}_p[X]$ has a root in $\mathbb{Z}_p$ if and only if it has a root modulo $p^n$ for every $n \in \mathbb{N}$. The forward direction is reduction; the reverse uses König's lemma on PolyRootSet f together with the inverse-limit description of $\mathbb{Z}_p$.