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

Anisotropic quadratic space data: a symmetric bilinear form on $V = k^n$ that is anisotropic ($B(v,v) = 0 \Rightarrow v = 0$), together with the auxiliary hypotheses needed to construct the unique maximal $\mathfrak{o}$-valued lattice: $2$ is a unit in $\mathfrak{o}$, the uniformizer's image is nonzero, $\mathfrak{o}$ is integrally closed for squares ($a^2 \in \mathfrak{o} \Rightarrow a \in \mathfrak{o}$), $\mathfrak{o}$ is Henselian, and a normalisation hypothesis controlling the valuation of cross-ratios $B(x,y)/B(x,x)$.

• form : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k
• form_symm (v w : Fin C.n → C.k) : self.form v w = self.form w v
• form_smul_left (r : C.k) (v w : Fin C.n → C.k) : self.form (r • v) w = r * self.form v w
• form_add_left (u v w : Fin C.n → C.k) : self.form (u + v) w = self.form u w + self.form v w
• anisotropic (v : Fin C.n → C.k) : self.form v v = 0 → v = 0
• two_unit : C.isUnitInO 2
• embed_pi_ne_zero : C.embed C.uniformizer ≠ 0
• dvr_sq_integral (a : C.k) : C.isInO (a * a) → C.isInO a
• inst_henselian : HenselianLocalRing C.𝔬
• hmax : C.maxIdeal = IsLocalRing.maximalIdeal C.𝔬
• dvr_normalize_ratio (a d : C.k) : ¬C.isInO a → C.isInO d → d ≠ 0 → ∃ (n : ℕ), 0 < n ∧ C.isUnitInO (C.embed C.uniformizer ^ n * (a * d⁻¹)) ∧ ∀ (e : C.k), C.isInO e → C.isInMaxIdeal (C.embed C.uniformizer ^ (2 * n) * (e * d⁻¹))

theorem DVRContext.AnisotropicQuadSpace.form_smul_right {C : DVRContext} (B : C.AnisotropicQuadSpace) (r : C.k) (v w : Fin C.n → C.k) : B.form v (r • w) = r * B.form v w

Right linearity of $B$: derived from symmetry and left linearity, $B(v, r w) = r B(v, w)$.

theorem DVRContext.AnisotropicQuadSpace.form_add_right {C : DVRContext} (B : C.AnisotropicQuadSpace) (u v w : Fin C.n → C.k) : B.form u (v + w) = B.form u v + B.form u w

Right additivity of $B$: derived from symmetry and left additivity, $B(u, v + w) = B(u, v) + B(u, w)$.

theorem DVRContext.AnisotropicQuadSpace.form_zero_left {C : DVRContext} (B : C.AnisotropicQuadSpace) (v : Fin C.n → C.k) : B.form 0 v = 0

Vanishing of $B$ at zero on the left: $B(0, v) = 0$.

theorem DVRContext.AnisotropicQuadSpace.form_zero_right {C : DVRContext} (B : C.AnisotropicQuadSpace) (v : Fin C.n → C.k) : B.form v 0 = 0

Vanishing of $B$ at zero on the right: $B(v, 0) = 0$.

theorem DVRContext.AnisotropicQuadSpace.form_add_expand {C : DVRContext} (B : C.AnisotropicQuadSpace) (x y : Fin C.n → C.k) : B.form (x + y) (x + y) = B.form x x + 2 * B.form x y + B.form y y

Polarisation expansion: $B(x + y, x + y) = B(x, x) + 2 B(x, y) + B(y, y)$, the characteristic-zero expansion of the quadratic form along a sum.

theorem DVRContext.AnisotropicQuadSpace.form_smul_self {C : DVRContext} (B : C.AnisotropicQuadSpace) (r : C.k) (x : Fin C.n → C.k) : B.form (r • x) (r • x) = r * r * B.form x x

Scaling identity: $B(r x, r x) = r^2 B(x, x)$ -- the quadratic form is homogeneous of degree $2$.

theorem DVRContext.AnisotropicQuadSpace.two_unit_o {C : DVRContext} (B : C.AnisotropicQuadSpace) : IsUnit 2

$2$ is a unit in $\mathfrak{o}$: transfers the $2$-is-a-unit-in-$k$ hypothesis of an anisotropic quadratic space to a statement at the level of the ring $\mathfrak{o}$, by exploiting injectivity of the embedding $\iota : \mathfrak{o} \hookrightarrow k$.

theorem DVRContext.AnisotropicQuadSpace.hensel_quadratic_root {C : DVRContext} (B : C.AnisotropicQuadSpace) (b c : C.k) (hb : C.isUnitInO b) (hc : C.isInMaxIdeal c) : ∃ (α : C.k), C.isInO α ∧ α * α + 2 * b * α + c = 0

Hensel's lemma applied to monic quadratic equations: given $b \in \mathfrak{o}^\times$ and $c \in \mathfrak{m}$, the polynomial $X^2 + 2 b X + c$ has a root $\alpha \in \mathfrak{o}$. This is the key application of HenselianLocalRing.is_henselian used in constructing the maximal $\mathfrak{o}$-valued lattice.

def DVRContext.AnisotropicQuadSpace.integralCarrier {C : DVRContext} (B : C.AnisotropicQuadSpace) : Set (Fin C.n → C.k)

The maximal $\mathfrak{o}$-integral set: vectors $v \in V$ such that $B(v, v) \in \mathfrak{o}$. This is shown below to be the carrier of the unique maximal $\mathfrak{o}$-valued lattice.

def DVRContext.AnisotropicQuadSpace.IsOValued {C : DVRContext} (B : C.AnisotropicQuadSpace) (Λ : C.OLattice) : Prop

$\mathfrak{o}$-valued lattice: a lattice $\Lambda$ is $\mathfrak{o}$-valued if the form $B$ takes values in $\mathfrak{o}$ on $\Lambda \times \Lambda$.

theorem DVRContext.AnisotropicQuadSpace.form_cross_integral {C : DVRContext} (B : C.AnisotropicQuadSpace) [C.DVRClosure] (x y : Fin C.n → C.k) (hx : C.isInO (B.form x x)) (hy : C.isInO (B.form y y)) : C.isInO (B.form x y)

Cross terms are integral: if $B(x, x), B(y, y) \in \mathfrak{o}$, then $B(x, y) \in \mathfrak{o}$. The proof argues by contradiction: a non-integral cross-pairing combined with integral self-pairings would force a nontrivial isotropic vector via Hensel's lemma, contradicting anisotropy.

theorem DVRContext.AnisotropicQuadSpace.integralCarrier_add_closed {C : DVRContext} (B : C.AnisotropicQuadSpace) [C.DVRClosure] (x y : Fin C.n → C.k) (hx : x ∈ B.integralCarrier) (hy : y ∈ B.integralCarrier) : x + y ∈ B.integralCarrier

$B$-integral set is closed under addition: combining form_add_expand with form_cross_integral, the carrier $\{v : B(v, v) \in \mathfrak{o}\}$ is closed under addition.

theorem DVRContext.AnisotropicQuadSpace.integralCarrier_zero_mem {C : DVRContext} (B : C.AnisotropicQuadSpace) [C.DVRClosure] : 0 ∈ B.integralCarrier

Zero is $B$-integral: $B(0, 0) = 0 \in \mathfrak{o}$.

theorem DVRContext.AnisotropicQuadSpace.integralCarrier_smul_mem {C : DVRContext} (B : C.AnisotropicQuadSpace) [C.DVRClosure] (r : C.𝔬) (v : Fin C.n → C.k) (hv : v ∈ B.integralCarrier) : C.oscal r v ∈ B.integralCarrier

$B$-integral set is closed under $\mathfrak{o}$-scaling: for $r \in \mathfrak{o}$ and $v$ with $B(v, v) \in \mathfrak{o}$, also $B(r v, r v) = r^2 B(v, v) \in \mathfrak{o}$.

theorem DVRContext.AnisotropicQuadSpace.oValued_subset_integralCarrier {C : DVRContext} (B : C.AnisotropicQuadSpace) (Λ : C.OLattice) (hΛ : B.IsOValued Λ) : Λ.carrier ⊆ B.integralCarrier

Every $\mathfrak{o}$-valued lattice lies inside the maximal integral carrier: this is the maximality statement -- if $\Lambda$ takes $\mathfrak{o}$-values then in particular each $v \in \Lambda$ has $B(v, v) \in \mathfrak{o}$.

theorem DVRContext.AnisotropicQuadSpace.unique_maximal_oValued_lattice {C : DVRContext} (B : C.AnisotropicQuadSpace) [C.DVRClosure] : (∀ (x y : Fin C.n → C.k), x ∈ B.integralCarrier → y ∈ B.integralCarrier → x + y ∈ B.integralCarrier) ∧ 0 ∈ B.integralCarrier ∧ (∀ (r : C.𝔬), ∀ v ∈ B.integralCarrier, C.oscal r v ∈ B.integralCarrier) ∧ (∀ (v w : Fin C.n → C.k), v ∈ B.integralCarrier → w ∈ B.integralCarrier → C.isInO (B.form v w)) ∧ ∀ (Λ : C.OLattice), B.IsOValued Λ → Λ.carrier ⊆ B.integralCarrier

Unique maximal $\mathfrak{o}$-valued lattice: for an anisotropic quadratic space, the carrier $\{v : B(v, v) \in \mathfrak{o}\}$ is closed under addition, contains zero, is closed under $\mathfrak{o}$-scaling, has $B$-values in $\mathfrak{o}$, and contains every other $\mathfrak{o}$-valued lattice. This combines the previous closure lemmas with the maximality statement to certify the existence and uniqueness of the maximal $\mathfrak{o}$-valued lattice.