theorem perm_exists_gt_of_ne_one {m : ℕ} (σ : Equiv.Perm (Fin m)) (hσ : σ ≠ 1) : ∃ (i : Fin m), i < σ i

A non-identity permutation moves some index upward: for any permutation $σ \ne 1$ on $\text{Fin}\,m$, there is some $i$ with $i < σ(i)$. Used to detect off-diagonal terms in the Iwahori-determinant computation. Proof: if $σ(i) \le i$ for all $i$, then strict inequality somewhere combined with $\sum σ(j) = \sum j$ gives a contradiction.

theorem prod_lt_one_of_le_one {m : ℕ} (f : Fin m → ℝ) (hnn : ∀ (i : Fin m), 0 ≤ f i) (hle : ∀ (i : Fin m), f i ≤ 1) {i₀ : Fin m} (hlt : f i₀ < 1) : ∏ i : Fin m, f i < 1

Product strictly less than $1$ when one factor is strictly less than $1$ and others are $\le 1$: pulled out as a separate fact to bound off-diagonal Iwahori products.

theorem ultrametric_norm_sum_lt (p : ℕ) [Fact (Nat.Prime p)] {ι : Type u_1} {s : Finset ι} {f : ι → ℚ_[p]} {C : ℝ} (hC : 0 < C) (hbound : ∀ i ∈ s, ‖f i‖ < C) : ‖∑ i ∈ s, f i‖ < C

Ultrametric strict triangle inequality for a finite sum: in $\mathbb{Q}_p$ (or any ultrametric field), if every term $f(i)$ has norm $< C$, then so does the sum $\sum_i f(i)$. Proof by induction on the finset using $\|x + y\| \le \max(\|x\|, \|y\|)$.

theorem iwahori_det_norm_eq_one (p : ℕ) [Fact (Nat.Prime p)] {m : ℕ} (g : Matrix (Fin m) (Fin m) ℚ_[p]) (hdiag : ∀ (i : Fin m), ‖g i i‖ = 1) (habove : ∀ (i j : Fin m), i < j → ‖g i j‖ ≤ 1) (hbelow : ∀ (i j : Fin m), j < i → ‖g i j‖ < 1) : ‖g.det‖ = 1

Iwahori determinant has $p$-adic norm $1$: a matrix $g$ over $\mathbb{Q}_p$ that is in Iwahori form (diagonal entries unit norm, above-diagonal $\le 1$, strictly below-diagonal $< 1$) has $\|\det g\| = 1$. The proof expands the determinant as a sum over permutations: the identity contributes a product of unit-norm entries giving norm $1$, while every non-identity permutation forces at least one strictly-below-diagonal factor, making its contribution have norm $< 1$. Ultrametricity then yields $\|\det g\| = 1$.

noncomputable def padicDVRContext (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : DVRContext

The $p$-adic DVR context: instantiates the DVRContext framework with $k = \mathbb{Q}_p$, $\mathfrak{o} = \mathbb{Z}_p$, the natural inclusion as embed, and the uniformizer $p$. The parameter $n$ records the relevant dimension (e.g. of an Iwahori subgroup of $GL_n$).

theorem padic_isInO_iff {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (x : ℚ_[p]) : (padicDVRContext p n hn).isInO x ↔ ‖x‖ ≤ 1

Membership in the $p$-adic valuation subring via norm: $x \in \mathbb{Z}_p$ (as image of embed) iff $\|x\|_p \le 1$.

theorem padic_isInMaxIdeal_iff {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (x : ℚ_[p]) : (padicDVRContext p n hn).isInMaxIdeal x ↔ ‖x‖ < 1

Membership in the $p$-adic maximal ideal via norm: $x \in p\mathbb{Z}_p$ iff $\|x\|_p < 1$. Uses PadicInt.norm_lt_one_iff_dvd to translate between divisibility by $p$ and norm being strictly less than $1$.

theorem padic_isUnitInO_iff {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (x : ℚ_[p]) : (padicDVRContext p n hn).isUnitInO x ↔ ‖x‖ = 1

Units of $\mathbb{Z}_p$ via norm: $x \in \mathbb{Z}_p^\times$ iff $\|x\|_p = 1$.

theorem padic_iwahori_det_unit {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (g : Matrix (Fin n) (Fin n) ℚ_[p]) (hdiag : ∀ (i : Fin n), (padicDVRContext p n hn).isUnitInO (g i i)) (habove : ∀ (i j : Fin n), i < j → (padicDVRContext p n hn).isInO (g i j)) (hbelow : ∀ (i j : Fin n), j < i → (padicDVRContext p n hn).isInMaxIdeal (g i j)) : (padicDVRContext p n hn).isUnitInO g.det

Iwahori matrices over $\mathbb{Q}_p$ have unit determinant: phrased in the abstract DVRContext language as a wrapper around iwahori_det_norm_eq_one.

instance padicDVRClosure {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : (padicDVRContext p n hn).DVRClosure

DVRClosure instance for the $p$-adic context: assembles all closure properties of $\mathbb{Z}_p$ inside $\mathbb{Q}_p$ — closed under $0$, $1$, negation, addition, multiplication, integer casts, and inverses of units; plus Iwahori-determinant unit.

@[implicit_reducible]

noncomputable instance padicDVRTopology {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : (padicDVRContext p n hn).DVRTopology

DVRTopology instance for the $p$-adic context: equips the $p$-adic DVR context with its norm topology (a NormedField) and the ultrametric inequality, registering the norm-characterisations of isInO, isInMaxIdeal, and isUnitInO.