structure AnisotropicFormContext : Type 1

An anisotropic symmetric bilinear form context: a symmetric bilinear form $\langle \cdot, \cdot \rangle$ over $k$ that is anisotropic (no nonzero isotropic vectors), together with the ambient DVR data, Hensel-style solvability of quadratic equations, and closure properties of the integral self-pairings. Used to construct the maximal lattice on which the form is integral.

• C : DVRContext
• form : (Fin self.C.n → self.C.k) → (Fin self.C.n → self.C.k) → self.C.k
• form_symm (v w : Fin self.C.n → self.C.k) : self.form v w = self.form w v
• form_add_left (v₁ v₂ w : Fin self.C.n → self.C.k) : self.form (v₁ + v₂) w = self.form v₁ w + self.form v₂ w
• form_smul_left (c : self.C.k) (v w : Fin self.C.n → self.C.k) : self.form (c • v) w = c * self.form v w
• anisotropic (v : Fin self.C.n → self.C.k) : self.form v v = 0 → v = 0
• two_is_unit : self.C.isUnitInO (self.C.embed (1 + 1))
• hensel (b c : self.C.k) : self.C.isUnitInO b → self.C.isInMaxIdeal c → ∃ (α : self.C.k), α * α + b * α + c = 0
• isInO_zero : self.C.isInO 0
• isInO_add {x y : self.C.k} : self.C.isInO x → self.C.isInO y → self.C.isInO (x + y)
• isInO_mul {x y : self.C.k} : self.C.isInO x → self.C.isInO y → self.C.isInO (x * y)
• isInO_neg {x : self.C.k} : self.C.isInO x → self.C.isInO (-x)
• isUnitInO_inv {x : self.C.k} : self.C.isUnitInO x → self.C.isInO x⁻¹
• isInO_embed (r : self.C.𝔬) : self.C.isInO (self.C.embed r)
• selfpair_add_closed (v w : Fin self.C.n → self.C.k) : self.C.isInO (self.form v v) → self.C.isInO (self.form w w) → self.C.isInO (self.form (v + w) (v + w))
• spans_data (v : Fin self.C.n → self.C.k) : ∃ (m : ℕ) (cs : Fin m → self.C.k) (vs : Fin m → Fin self.C.n → self.C.k), (∀ (j : Fin m), self.C.isInO (self.form (vs j) (vs j))) ∧ v = ∑ j : Fin m, cs j • vs j

theorem AnisotropicFormContext.embed_two_ne_zero (ctx : AnisotropicFormContext) : ctx.C.embed (1 + 1) ≠ 0

The image of $2 = 1 + 1$ under the embedding $\mathfrak{o} \hookrightarrow k$ is nonzero, since $2$ is a unit.

theorem AnisotropicFormContext.form_zero_left (ctx : AnisotropicFormContext) (w : Fin ctx.C.n → ctx.C.k) : ctx.form 0 w = 0

The form vanishes on the zero vector in the left slot.

theorem AnisotropicFormContext.form_zero_right (ctx : AnisotropicFormContext) (v : Fin ctx.C.n → ctx.C.k) : ctx.form v 0 = 0

The form vanishes on the zero vector in the right slot.

theorem AnisotropicFormContext.form_zero_isInO (ctx : AnisotropicFormContext) : ctx.C.isInO (ctx.form 0 0)

The form value $\langle 0, 0 \rangle = 0$ is integral.

theorem AnisotropicFormContext.isInO_sub (ctx : AnisotropicFormContext) {x y : ctx.C.k} (hx : ctx.C.isInO x) (hy : ctx.C.isInO y) : ctx.C.isInO (x - y)

The difference of integral elements is integral.

theorem AnisotropicFormContext.form_add_right (ctx : AnisotropicFormContext) (v w₁ w₂ : Fin ctx.C.n → ctx.C.k) : ctx.form v (w₁ + w₂) = ctx.form v w₁ + ctx.form v w₂

Bilinearity of the form on the right slot.

theorem AnisotropicFormContext.form_smul_right (ctx : AnisotropicFormContext) (c : ctx.C.k) (v w : Fin ctx.C.n → ctx.C.k) : ctx.form v (c • w) = c * ctx.form v w

The form is $k$-linear in the right slot.

theorem AnisotropicFormContext.smul_selfpair_isInO (ctx : AnisotropicFormContext) (c : ctx.C.k) (v : Fin ctx.C.n → ctx.C.k) (hc : ctx.C.isInO c) (hv : ctx.C.isInO (ctx.form v v)) : ctx.C.isInO (ctx.form (c • v) (c • v))

Scaling preserves integrality of the self-pairing $\langle cv, cv \rangle = c^2 \langle v, v \rangle$.

theorem AnisotropicFormContext.closed_under_o_combination_data (ctx : AnisotropicFormContext) (coeffs : Fin ctx.C.n → ctx.C.k) (vectors : Fin ctx.C.n → Fin ctx.C.n → ctx.C.k) (hcoeffs : ∀ (i : Fin ctx.C.n), ctx.C.isInO (coeffs i)) (hvecs : ∀ (i : Fin ctx.C.n), ctx.C.isInO (ctx.form (vectors i) (vectors i))) : ctx.C.isInO (ctx.form (∑ i : Fin ctx.C.n, coeffs i • vectors i) (∑ i : Fin ctx.C.n, coeffs i • vectors i))

Integral $\mathfrak{o}$-linear combinations of vectors with integral self-pairings have integral self-pairing.

def AnisotropicFormContext.maxLat (ctx : AnisotropicFormContext) : ctx.C.OLattice

The maximal lattice of an anisotropic form: the $\mathfrak{o}$-lattice $\{v : \langle v, v \rangle \in \mathfrak{o}\}$ of vectors with integral self-pairing.

theorem AnisotropicFormContext.maxLat_complete (ctx : AnisotropicFormContext) (v : Fin ctx.C.n → ctx.C.k) : ctx.C.isInO (ctx.form v v) → v ∈ ctx.maxLat.carrier

Completeness of maxLat: every vector with integral self-pairing is in it.

theorem AnisotropicFormContext.maxLat_integral (ctx : AnisotropicFormContext) (v : Fin ctx.C.n → ctx.C.k) : v ∈ ctx.maxLat.carrier → ∀ w ∈ ctx.maxLat.carrier, ctx.C.isInO (ctx.form v w)

The form is integral on the maximal lattice: $\langle v, w \rangle \in \mathfrak{o}$ for all $v, w$ with integral self-pairings, by the polarisation identity and the fact that $2$ is a unit.