structure DVRContext : Type (max (u_1 + 1) (u_2 + 1))

Discrete valuation context: a bundle of data describing a discrete valuation field. It consists of a field $k$, an integral domain $\mathfrak{o}$ (the ring of integers), an injective ring embedding $\mathfrak{o} \hookrightarrow k$, a chosen uniformizer $\pi \in \mathfrak{o}$ generating the maximal ideal, and a positive integer $n$ specifying the rank of the ambient module $k^n$ used for lattices and the building of $GL_n$.

• k : Type u_1
• 𝔬 : Type u_2
• inst_field : Field self.k
• inst_comm_ring : CommRing self.𝔬
• inst_domain : IsDomain self.𝔬
• embed : self.𝔬 →+* self.k
• embed_injective : Function.Injective ⇑self.embed
• uniformizer : self.𝔬
• n : ℕ
• n_pos : 0 < self.n

def DVRContext.maxIdeal (C : DVRContext) : Ideal C.𝔬

The maximal ideal of $\mathfrak{o}$: the principal ideal $(\pi) \subseteq \mathfrak{o}$ generated by the chosen uniformizer $\pi$. In a DVR this is the unique maximal ideal.

def DVRContext.oscal (C : DVRContext) (r : C.𝔬) (v : Fin C.n → C.k) : Fin C.n → C.k

$\mathfrak{o}$-scalar action on $k^n$: pointwise multiplication by the image $\iota(r) \in k$ of $r \in \mathfrak{o}$. Used to express the $\mathfrak{o}$-module structure of $k^n$ via the embedding $\iota = $embed.

def DVRContext.isInO (C : DVRContext) (x : C.k) : Prop

Predicate "$x \in \mathfrak{o}$": an element $x \in k$ lies in the valuation ring iff it is the image of some $r \in \mathfrak{o}$ under the embedding $\iota$.

def DVRContext.isInMaxIdeal (C : DVRContext) (x : C.k) : Prop

Predicate "$x \in \mathfrak{m}$": an element $x \in k$ lies in the maximal ideal iff it is the image of some $r \in (\pi) \subseteq \mathfrak{o}$.

def DVRContext.isUnitInO (C : DVRContext) (x : C.k) : Prop

Predicate "$x \in \mathfrak{o}^\times$": an element $x \in k$ is a unit of the valuation ring iff it is the image of a unit $r \in \mathfrak{o}^\times$.

theorem DVRContext.isUnitInO_isInO (C : DVRContext) {x : C.k} (h : C.isUnitInO x) : C.isInO x

Units lie in $\mathfrak{o}$: every unit in $\mathfrak{o}$ is in particular an element of $\mathfrak{o}$.

theorem DVRContext.isInMaxIdeal_isInO (C : DVRContext) {x : C.k} (h : C.isInMaxIdeal x) : C.isInO x

The maximal ideal lies in $\mathfrak{o}$: every element of the maximal ideal is in particular an element of $\mathfrak{o}$.

noncomputable def DVRContext.newtonSeq (C : DVRContext) (f : Polynomial C.𝔬) (x₀ : C.𝔬) : ℕ → C.𝔬

Newton iteration sequence: starting from $x_0$, iteratively define $x_{n+1} = x_n - f(x_n) / f'(x_n)$ using Ring.inverse for the division. This is the underlying sequence used in Hensel's lemma to produce a root of $f$.

theorem DVRContext.HenselsLemma (C : DVRContext) [IsLocalRing C.𝔬] [IsAdicComplete (IsLocalRing.maximalIdeal C.𝔬) C.𝔬] (f : Polynomial C.𝔬) (a₀ : C.𝔬) : Polynomial.eval a₀ f ∈ IsLocalRing.maximalIdeal C.𝔬 → Polynomial.eval a₀ (Polynomial.derivative f) ∉ IsLocalRing.maximalIdeal C.𝔬 → ∃ (a : C.𝔬), Polynomial.eval a f = 0 ∧ a - a₀ ∈ IsLocalRing.maximalIdeal C.𝔬 ∧ (∀ (n : ℕ), Polynomial.eval (C.newtonSeq f a₀ n) f ∈ IsLocalRing.maximalIdeal C.𝔬 ^ (n + 1)) ∧ ∀ (n : ℕ), IsUnit (Polynomial.eval (C.newtonSeq f a₀ n) (Polynomial.derivative f))

Hensel's lemma: in an adically complete local ring $\mathfrak{o}$, if $a_0 \in \mathfrak{o}$ satisfies $f(a_0) \in \mathfrak{m}$ and $f'(a_0) \notin \mathfrak{m}$, then there exists a root $a \in \mathfrak{o}$ of $f$ with $a \equiv a_0 \pmod{\mathfrak{m}}$. Moreover the Newton iterates $c_n$ satisfy $f(c_n) \in \mathfrak{m}^{n+1}$ and $f'(c_n)$ is a unit for all $n$.

structure DVRContext.OLattice (C : DVRContext) : Type u_1

An $\mathfrak{o}$-lattice in $V = k^n$: a subset $\Lambda \subseteq k^n$ that is an $\mathfrak{o}$-submodule (contains zero, is closed under addition and under the action of $\mathfrak{o}$), spans $V$ as a $k$-vector space, and is closed under $\mathfrak{o}$-linear combinations of $n$ vectors with $\mathfrak{o}$-coefficients (used as a substitute for finite generation over $\mathfrak{o}$).

• carrier : Set (Fin C.n → C.k)
• zero_mem : 0 ∈ self.carrier
• add_mem {x y : Fin C.n → C.k} : x ∈ self.carrier → y ∈ self.carrier → x + y ∈ self.carrier
• smul_mem (r : C.𝔬) {x : Fin C.n → C.k} : x ∈ self.carrier → C.oscal r x ∈ self.carrier
• spans_V (v : Fin C.n → C.k) : ∃ (m : ℕ) (cs : Fin m → C.k) (vs : Fin m → Fin C.n → C.k), (∀ (j : Fin m), vs j ∈ self.carrier) ∧ v = ∑ j : Fin m, cs j • vs j
• closed_under_o_combination (coeffs : Fin C.n → C.k) (vectors : Fin C.n → Fin C.n → C.k) : (∀ (i : Fin C.n), C.isInO (coeffs i)) → (∀ (i : Fin C.n), vectors i ∈ self.carrier) → ∑ i : Fin C.n, coeffs i • vectors i ∈ self.carrier

def DVRContext.OLattice.scale (C : DVRContext) (Λ : C.OLattice) (α : C.k) : Set (Fin C.n → C.k)

Scaling a lattice by a scalar: $\alpha \cdot \Lambda := \{\alpha \cdot w : w \in \Lambda\}$, used to define the homothety relation between lattices.

def DVRContext.OLattice.IsHomothetic (C : DVRContext) (Λ₁ Λ₂ : C.OLattice) : Prop

Homothety relation on lattices: two lattices $\Lambda_1, \Lambda_2$ are homothetic iff $\Lambda_1 = \alpha \cdot \Lambda_2$ for some nonzero scalar $\alpha \in k^\times$. The quotient by this relation yields the vertices of the Bruhat--Tits building.

def DVRContext.HomothetyClass (C : DVRContext) : Type u_1

Vertex set of the Bruhat--Tits building: the quotient of the set of $\mathfrak{o}$-lattices in $V = k^n$ by the homothety equivalence relation.

structure DVRContext.PrimitiveLattice (C : DVRContext) extends C.OLattice : Type u_1

Primitive lattice with a bilinear form: an $\mathfrak{o}$-lattice $\Lambda$ equipped with a bilinear form form $: V \times V \to k$ such that the form is integral on $\Lambda$ (takes values in $\mathfrak{o}$) and is nondegenerate modulo $\pi$: any element $v \in \Lambda$ that is not divisible by the uniformizer pairs to a unit against some element of $\Lambda$.

• carrier : Set (Fin C.n → C.k)
• zero_mem : 0 ∈ self.carrier
• add_mem {x y : Fin C.n → C.k} : x ∈ self.carrier → y ∈ self.carrier → x + y ∈ self.carrier
• smul_mem (r : C.𝔬) {x : Fin C.n → C.k} : x ∈ self.carrier → C.oscal r x ∈ self.carrier
• spans_V (v : Fin C.n → C.k) : ∃ (m : ℕ) (cs : Fin m → C.k) (vs : Fin m → Fin C.n → C.k), (∀ (j : Fin m), vs j ∈ self.carrier) ∧ v = ∑ j : Fin m, cs j • vs j
• closed_under_o_combination (coeffs : Fin C.n → C.k) (vectors : Fin C.n → Fin C.n → C.k) : (∀ (i : Fin C.n), C.isInO (coeffs i)) → (∀ (i : Fin C.n), vectors i ∈ self.carrier) → ∑ i : Fin C.n, coeffs i • vectors i ∈ self.carrier
• form : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k
• form_linear_left (r : C.k) (v w : Fin C.n → C.k) : self.form (r • v) w = r * self.form v w
• form_linear_right (r : C.k) (v w : Fin C.n → C.k) : self.form v (r • w) = r * self.form v w
• form_integral {v w : Fin C.n → C.k} : v ∈ self.carrier → w ∈ self.carrier → C.isInO (self.form v w)
• form_nondeg {v : Fin C.n → C.k} : v ∈ self.carrier → (¬∃ w ∈ self.carrier, v = C.oscal C.uniformizer w) → ∃ w ∈ self.carrier, C.isUnitInO (self.form v w)

@[reducible, inline]

abbrev DVRContext.GL_n_k (C : DVRContext) : Type u_1

Abbreviation for $GL_n(k)$: the general linear group of invertible $n \times n$ matrices over the field $k$.

def DVRContext.UpperUnipotent (C : DVRContext) : Set C.GL_n_k

Upper unipotent subgroup of $GL_n(k)$: matrices with $1$'s on the diagonal and zeros strictly below the diagonal.

def DVRContext.LowerUnipotent (C : DVRContext) : Set C.GL_n_k

Lower unipotent subgroup of $GL_n(k)$: matrices with $1$'s on the diagonal and zeros strictly above the diagonal.

def DVRContext.DiagonalMatrices (C : DVRContext) : Set C.GL_n_k

Diagonal subgroup of $GL_n(k)$: invertible matrices whose off-diagonal entries vanish.

def DVRContext.IwahoriSubgroupGLn (C : DVRContext) : Set C.GL_n_k

Iwahori subgroup of $GL_n(k)$: invertible matrices whose diagonal entries are units in $\mathfrak{o}$, whose strictly-upper-triangular entries lie in $\mathfrak{o}$, and whose strictly-lower-triangular entries lie in the maximal ideal $\mathfrak{m}$.

def DVRContext.GL_n_o (C : DVRContext) : Set C.GL_n_k

Maximal compact subgroup $GL_n(\mathfrak{o})$: invertible matrices over $\mathfrak{o}$ whose inverse also has entries in $\mathfrak{o}$. Equivalently, $GL_n(\mathfrak{o})$ is the group of $\mathfrak{o}$-linear automorphisms of the standard lattice.

class DVRContext.DVRClosure (C : DVRContext) : Prop

DVR closure axioms: a packaging of the algebraic closure properties of $\mathfrak{o} \subseteq k$ that are used throughout the development: $0, 1 \in \mathfrak{o}$, closure of $\mathfrak{o}$ under negation, addition, and multiplication, integers are in $\mathfrak{o}$, the inverse of a unit in $\mathfrak{o}$ is in $\mathfrak{o}$, and the determinant of any matrix satisfying the Iwahori conditions is a unit in $\mathfrak{o}$.

• isInO_zero : C.isInO 0
• isInO_one : C.isInO 1
• isInO_neg {x : C.k} : C.isInO x → C.isInO (-x)
• isInO_add {x y : C.k} : C.isInO x → C.isInO y → C.isInO (x + y)
• isInO_mul {x y : C.k} : C.isInO x → C.isInO y → C.isInO (x * y)
• isInO_intCast (n : ℤ) : C.isInO ↑n
• isUnitInO_inv {x : C.k} : C.isUnitInO x → C.isInO x⁻¹
• iwahori_det_unit (g : Matrix (Fin C.n) (Fin C.n) C.k) : (∀ (i : Fin C.n), C.isUnitInO (g i i)) → (∀ (i j : Fin C.n), i < j → C.isInO (g i j)) → (∀ (i j : Fin C.n), j < i → C.isInMaxIdeal (g i j)) → C.isUnitInO g.det

theorem DVRContext.isInO_sum (C : DVRContext) [C.DVRClosure] {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ i ∈ s, C.isInO (f i)) : C.isInO (∑ i ∈ s, f i)

Sums of $\mathfrak{o}$-elements lie in $\mathfrak{o}$: a finite sum of elements all in $\mathfrak{o}$ remains in $\mathfrak{o}$.

theorem DVRContext.isInO_prod (C : DVRContext) [C.DVRClosure] {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ i ∈ s, C.isInO (f i)) : C.isInO (∏ i ∈ s, f i)

Products of $\mathfrak{o}$-elements lie in $\mathfrak{o}$: a finite product of elements all in $\mathfrak{o}$ remains in $\mathfrak{o}$.

theorem DVRContext.det_isInO (C : DVRContext) [C.DVRClosure] {m : ℕ} (A : Matrix (Fin m) (Fin m) C.k) (hA : ∀ (i j : Fin m), C.isInO (A i j)) : C.isInO A.det

Determinant of an $\mathfrak{o}$-matrix lies in $\mathfrak{o}$: if all entries of an $m \times m$ matrix $A$ over $k$ lie in $\mathfrak{o}$, then so does $\det A$.

theorem DVRContext.adjugate_isInO (C : DVRContext) [C.DVRClosure] {m : ℕ} (A : Matrix (Fin m) (Fin m) C.k) (hA : ∀ (i j : Fin m), C.isInO (A i j)) (i j : Fin m) : C.isInO (A.adjugate i j)

Adjugate of an $\mathfrak{o}$-matrix has $\mathfrak{o}$-entries: if all entries of $A$ lie in $\mathfrak{o}$, then every entry of the adjugate matrix $\mathrm{adj}(A)$ also lies in $\mathfrak{o}$.

theorem DVRContext.nonsing_inv_isInO (C : DVRContext) [C.DVRClosure] {m : ℕ} (A : Matrix (Fin m) (Fin m) C.k) (hA : ∀ (i j : Fin m), C.isInO (A i j)) (hdet : C.isUnitInO A.det) (i j : Fin m) : C.isInO (A⁻¹ i j)

Inverse of an integral matrix with unit determinant has $\mathfrak{o}$-entries: if $A$ has entries in $\mathfrak{o}$ and $\det A$ is a unit in $\mathfrak{o}$, then $A^{-1}$ also has entries in $\mathfrak{o}$. This is the analogue for integral matrices of the unimodularity condition for $GL_n(\mathfrak{o})$.

class DVRContext.DVRTopology (C : DVRContext) : Type u_1

DVR topology axioms: bundle together an ultrametric normed-field structure on $k$ and the assertions that the valuation predicates isInO, isInMaxIdeal, isUnitInO correspond to the standard normed conditions $\|x\| \le 1$, $\|x\| < 1$, $\|x\| = 1$ respectively. This turns the algebraic DVR data into a topological one.

• instNormedField : NormedField C.k
• instUltrametric : IsUltrametricDist C.k
• isInO_iff_norm_le_one (x : C.k) : C.isInO x ↔ ‖x‖ ≤ 1
• isInMaxIdeal_iff_norm_lt_one (x : C.k) : C.isInMaxIdeal x ↔ ‖x‖ < 1
• isUnitInO_iff_norm_eq_one (x : C.k) : C.isUnitInO x ↔ ‖x‖ = 1

theorem DVRContext.isClopen_valuationRing (C : DVRContext) [ht : C.DVRTopology] : IsClopen {x : C.k | C.isInO x}

The valuation ring $\mathfrak{o}$ is clopen in $k$: under the ultrametric topology of $k$, the set $\{x \in k : \|x\| \le 1\} = \mathfrak{o}$ is both open and closed. This is a key feature distinguishing the ultrametric setting from the archimedean one.

theorem DVRContext.isClopen_maximalIdeal (C : DVRContext) [ht : C.DVRTopology] : IsClopen {x : C.k | C.isInMaxIdeal x}

The maximal ideal $\mathfrak{m}$ is clopen in $k$: under the ultrametric topology of $k$, the set $\{x \in k : \|x\| < 1\} = \mathfrak{m}$ is both open and closed.

theorem DVRContext.isClopen_units (C : DVRContext) [ht : C.DVRTopology] : IsClopen {x : C.k | C.isUnitInO x}

The unit sphere $\mathfrak{o}^\times$ is clopen in $k$: the set $\{x \in k : \|x\| = 1\} = \mathfrak{o}^\times$ is both open and closed, expressed as the difference of two clopen balls.

theorem DVRContext.isClopen_valuationRing_units_maxIdeal (C : DVRContext) [ht : C.DVRTopology] : IsClopen {x : C.k | C.isInO x} ∧ IsClopen {x : C.k | C.isUnitInO x} ∧ IsClopen {x : C.k | C.isInMaxIdeal x}

All three valuation-defined subsets are clopen: $\mathfrak{o}$, $\mathfrak{o}^\times$, and $\mathfrak{m}$ are all simultaneously open and closed in the ultrametric topology of $k$. A convenient packaging of the three preceding theorems.