Abstract Binary Tower Basis

Basis constructions and index-casting lemmas for abstract binary tower extensions.

noncomputable def BinaryTower.hli_level_diff_0 (l : ℕ) : Module.Basis (Fin 1) (BTField l) (BTField l)

@[reducible]

def BinaryTower.BTField.isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) : IsScalarTower (BTField l) (BTField r) (BTField (r + 1))

@[irreducible]

def BinaryTower.multilinearBasis (l r : ℕ) (h_le : l ≤ r) : Module.Basis (Fin (2 ^ (r - l))) (BTField l) (BTField r)

The multilinear basis for BTField τ over BTField k is the set of multilinear monomials in the tower generators Z(k+1), ..., Z(τ). This is done via scalar tower multiplication of power basis across adjacent levels.

@[simp]

theorem BinaryTower.BTField.PowerBasis.dim_of_eq_rec (r1 r : ℕ) (h_r : r = r1 + 1) (b : PowerBasis (BTField r1) (BTField (r1 + 1))) : (⋯ ▸ b).dim = b.dim

@[simp]

theorem BinaryTower.PowerBasis.cast_basis_succ_of_eq_rec_apply (r1 r : ℕ) (h_r : r = r1 + 1) (k : Fin 2) : let b := powerBasisSucc r1; let bCast := ⋯ ▸ b; have h_pb_dim := ⋯; have h_pb'_dim := ⋯; have h_pb_type_eq := ⋯; have left := cast h_pb_type_eq bCast.basis; have right := (algebraMap (BTField (r1 + 1)) (BTField r)) (b.basis (Fin.cast ⋯ k)); left k = right

theorem BinaryTower.algebraMap_𝕏_eq_of_index_eq (r k m : ℕ) (h_k_le : k + 1 ≤ r) (h_m_le : m + 1 ≤ r) (h_eq : k = m) : (algebraMap (BTField (k + 1)) (BTField r)) (𝕏 k) = (algebraMap (BTField (m + 1)) (BTField r)) (𝕏 m)

When two indices are equal, the tower algebra maps send the respective 𝕏 to the same element.

The basis element at index j is the product of the tower generators at the ON bits in binary representation of j.

theorem BinaryTower.multilinearBasis_apply (r l : ℕ) (h_le : l ≤ r) (j : Fin (2 ^ (r - l))) : (multilinearBasis l r h_le) j = ∏ i : Fin (r - l), (algebraMap (BTField (l + ↑i + 1)) (BTField r)) (𝕏 (l + ↑i) ^ (↑i).getBit ↑j)