Concrete Binary Tower Basis

Basis constructions for the concrete bitvector binary tower.

@[simp]

theorem ConcreteBinaryTower.Basis_cast_index_eq (i j k n : ℕ) (h_le : k ≤ n) (h_eq : i = j) : Module.Basis (Fin i) (ConcreteBTField k) (ConcreteBTField n) = Module.Basis (Fin j) (ConcreteBTField k) (ConcreteBTField n)

theorem ConcreteBinaryTower.Basis_cast_dest_eq {ι : Type u_1} (k n m : ℕ) (h_k_le_n : k ≤ n) (h_k_le_m : k ≤ m) (h_eq : m = n) : Module.Basis ι (ConcreteBTField k) (ConcreteBTField m) = Module.Basis ι (ConcreteBTField k) (ConcreteBTField n)

theorem ConcreteBinaryTower.PowerBasis_cast_dest_eq (k n m : ℕ) (h_k_le_n : k ≤ n) (h_k_le_m : k ≤ m) (h_eq : m = n) : PowerBasis (ConcreteBTField k) (ConcreteBTField m) = PowerBasis (ConcreteBTField k) (ConcreteBTField n)

The following two theorems are used to cast the basis of ConcreteBTField α to ConcreteBTField β via changing in index type : Fin (i) to Fin (j) when α ≤ β.

@[simp]

theorem ConcreteBinaryTower.Basis_cast_index_apply {α β i j : ℕ} {k : Fin j} (h_le : α ≤ β) (h_eq : i = j) {b : Module.Basis (Fin i) (ConcreteBTField α) (ConcreteBTField β)} : have castBasis := cast ⋯ b; castBasis k = b (Fin.cast ⋯ k)

@[simp]

theorem ConcreteBinaryTower.Basis_cast_dest_apply {ι : Type u_1} (α β γ : ℕ) (h_le1 : α ≤ β) (h_le2 : α ≤ γ) (h_eq : β = γ) {k : ι} (b : Module.Basis ι (ConcreteBTField α) (ConcreteBTField β)) : have castBasis := cast ⋯ b; castBasis k = cast ⋯ (b k)

noncomputable def ConcreteBinaryTower.basisSucc (k : ℕ) : Module.Basis (Fin 2) (ConcreteBTField k) (ConcreteBTField (k + 1))

The power basis for ConcreteBTField (k + 1) over ConcreteBTField k is {1, Z (k + 1)}

noncomputable def ConcreteBinaryTower.powerBasisSucc (k : ℕ) : PowerBasis (ConcreteBTField k) (ConcreteBTField (k + 1))

theorem ConcreteBinaryTower.powerBasisSucc_gen (k : ℕ) : (powerBasisSucc k).gen = Z (k + 1)

@[simp]

theorem ConcreteBinaryTower.minPoly_of_powerBasisSucc_generator (k : ℕ) : minpoly (ConcreteBTField k) (powerBasisSucc k).gen = Polynomial.X ^ 2 + Z k • Polynomial.X + 1

theorem ConcreteBinaryTower.powerBasisSucc_dim (k : ℕ) : (powerBasisSucc k).dim = 2

noncomputable def ConcreteBinaryTower.hli_level_diff_0 (l : ℕ) : Module.Basis (Fin 1) (ConcreteBTField l) (ConcreteBTField l)

@[reducible]

def ConcreteBinaryTower.isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) : IsScalarTower (ConcreteBTField l) (ConcreteBTField r) (ConcreteBTField (r + 1))

Reducible Prop-valued helper for letI scalar-tower instances.

@[irreducible]

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

The multilinear basis for ConcreteBTField τ over ConcreteBTField 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 ConcreteBinaryTower.PowerBasis.dim_of_eq_rec (r1 r : ℕ) (h_r : r = r1 + 1) (b : PowerBasis (ConcreteBTField r1) (ConcreteBTField (r1 + 1))) : (⋯ ▸ b).dim = b.dim

@[simp]

theorem ConcreteBinaryTower.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 (ConcreteBTField (r1 + 1)) (ConcreteBTField r)) (b.basis (Fin.cast ⋯ k)); left k = right

@[simp]

theorem ConcreteBinaryTower.coe_basis_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) (i : Fin pb.dim) : pb.basis i = pb.gen ^ ↑i

theorem ConcreteBinaryTower.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 (ConcreteBTField (k + 1)) (ConcreteBTField r)) (𝕏 k) = (algebraMap (ConcreteBTField (m + 1)) (ConcreteBTField 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 ConcreteBinaryTower.multilinearBasis_apply (r l : ℕ) (h_le : l ≤ r) (j : Fin (2 ^ (r - l))) : (multilinearBasis l r h_le) j = ∏ i : Fin (r - l), (algebraMap (ConcreteBTField (l + ↑i + 1)) (ConcreteBTField r)) (𝕏 (l + ↑i) ^ (↑i).getBit ↑j)