A field basis containing one supplies the complement used by the multiplication pairing. The resulting product inequality is independent of the geometric construction of the basis or the length function.
theorem
CCDN.fieldBasisMiddle_span
{F : Type u_1}
{K : Type u_2}
{ι : Type u_3}
[Field F]
[Field K]
[Algebra F K]
(b : Module.Basis ι F K)
(p q : ι)
:
The span of the basis vectors b i with i ≠ p and i ≠ q is the intersection of the kernels
of the coordinate functionals b.coord q and b.coord p.
noncomputable def
CCDN.fieldBasisMiddle
{F : Type u_1}
{K : Type u_2}
{ι : Type u_3}
[Field F]
[Field K]
[Algebra F K]
(b : Module.Basis ι F K)
(p q : ι)
:
The original basis vectors other than the unit and the distinguished last vector form a basis of the two coordinate kernels.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CCDN.field_basis_multiplication_minimum_product
{F : Type u_1}
{K : Type u_2}
{ι : Type u_3}
[Field F]
[Field K]
[Algebra F K]
[Fintype ι]
(b : Module.Basis ι F K)
(p q : ι)
(hpq : p ≠ q)
(hp : b p = 1)
(N : K → ℝ)
(hN : ∀ (x : K), 0 ≤ N x)
(hmul : ∀ (x y : K), N (x * y) ≤ N x * N y)
(hunit : 1 ≤ N (b p))
(hminimum : ∀ (i j : { i : ι // i ≠ p ∧ i ≠ q }), (b.coord q) (b ↑i * b ↑j) ≠ 0 → N (b q) ≤ N (b ↑i * b ↑j))
:
A nonnegative submultiplicative length and a minimum condition on products detected by the last coordinate give the field-basis product bound. In lattice applications the minimum condition follows because a detected product lies outside the preceding coordinate hyperplane.