Abstract Binary Tower Split

Splitting and recombination lemmas for abstract binary tower extensions.

@[simp]

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

theorem BinaryTower.BTField.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 ι (BTField k) (BTField m) = Module.Basis ι (BTField k) (BTField n)

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

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

@[simp]

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

@[simp]

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

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

noncomputable def BinaryTower.powerBasisSucc (k : ℕ) : PowerBasis (BTField k) (BTField (k + 1))

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

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

noncomputable def BinaryTower.join_via_add_smul {k : ℕ} (h_pos : k > 0) (hi_btf lo_btf : BTField (k - 1)) : BTField k

def BinaryTower.«term⋘_,_⋙» : Lean.ParserDescr

theorem BinaryTower.join_via_add_smul_zero {k : ℕ} (h_pos : k > 0) : join_via_add_smul h_pos 0 0 = 0

theorem BinaryTower.join_via_add_smul_one_zero_eq_Z {k : ℕ} (h_pos : k > 0) : join_via_add_smul h_pos 1 0 = Z k

theorem BinaryTower.join_via_add_smul_one {k : ℕ} (h_pos : k > 0) : join_via_add_smul h_pos 0 1 = 1

theorem BinaryTower.sum_join_via_add_smul (k : ℕ) (h_pos : k > 0) (a₁ a₀ b₁ b₀ : BTField (k - 1)) : join_via_add_smul h_pos a₁ a₀ + join_via_add_smul h_pos b₁ b₀ = join_via_add_smul h_pos (a₁ + b₁) (a₀ + b₀)

theorem BinaryTower.mul_join_via_add_smul (k : ℕ) (h_pos : k > 0) (a₁ a₀ b₁ b₀ : BTField (k - 1)) : join_via_add_smul h_pos a₁ a₀ * join_via_add_smul h_pos b₁ b₀ = join_via_add_smul h_pos (a₁ * b₁ * Z (k - 1) + a₁ * b₀ + a₀ * b₁) (a₀ * b₀ + a₁ * b₁)

(a₁ • Z k + a₀) * (b₁ • Z k + b₀) = a₁ * b₁ • (Z k)^2 + (a₁ * b₀ + a₀ * b₁) • Z k + a₀ * b₀ = a₁ * b₁ • (Z (k-1) * Z k + 1) + (a₁ * b₀ + a₀ * b₁) • Z k + a₀ * b₀ = [a₁ * b₁ * Z (k - 1) + a₁ * b₀ + a₀ * b₁] * (Z k) + (a₀ * b₀ + a₁ * b₁)

theorem BinaryTower.unique_linear_decomposition_succ (k : ℕ) (x : BTField (k + 1)) : ∃! p : BTField k × BTField k, x = join_via_add_smul ⋯ p.1 p.2

noncomputable def BinaryTower.split (k : ℕ) (h_k : k > 0) (x : BTField k) : BTField (k - 1) × BTField (k - 1)

Proofs that split is the inverse of join_via_add_smul

theorem BinaryTower.eq_join_via_add_smul_eq_iff_split (k : ℕ) (h_pos : k > 0) (x : BTField k) (hi_btf lo_btf : BTField (k - 1)) : x = join_via_add_smul h_pos hi_btf lo_btf ↔ split k h_pos x = (hi_btf, lo_btf)

theorem BinaryTower.split_join_via_add_smul_eq_iff_split (k : ℕ) (h_pos : k > 0) (hi_btf lo_btf : BTField (k - 1)) : split k h_pos (join_via_add_smul h_pos hi_btf lo_btf) = (hi_btf, lo_btf)

theorem BinaryTower.join_eq_join_iff (k : ℕ) (h_pos : k > 0) (hi₁ hi₀ lo₁ lo₀ : BTField (k - 1)) : join_via_add_smul h_pos hi₁ lo₁ = join_via_add_smul h_pos hi₀ lo₀ ↔ hi₁ = hi₀ ∧ lo₁ = lo₀

theorem BinaryTower.split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1)) : split k h_pos ((algebraMap (BTField (k - 1)) (BTField k)) x) = (0, x)

An element x lifted from the base field BTField (k-1) has (0, x) as its split representation in BTField k.

theorem BinaryTower.algebraMap_succ_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1)) : (algebraMap (BTField (k - 1)) (BTField k)) x = join_via_add_smul h_pos 0 x

theorem BinaryTower.algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : BTField i) : (algebraMap (BTField i) (BTField j)) x = join_via_add_smul ⋯ 0 ((algebraMap (BTField i) (BTField (j - 1))) x)

@[simp]

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