Concrete Binary Tower Algebra

Algebra maps and embeddings for the concrete bitvector binary tower.

def ConcreteBinaryTower.canonicalAlgMap (k : ℕ) : ConcreteBTField k →+* ConcreteBTField (k + 1)

@[simp]

theorem ConcreteBinaryTower.generator_is_not_lifted_to_succ (k : ℕ) (x : ConcreteBTField k) : (canonicalAlgMap k) x ≠ Z (k + 1)

Z(k+1) is the adjoined root of poly k to ConcreteBTField (k+1), so it is not lifted to ConcreteBTField (k+1) by canonicalAlgMap

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField_add_eq (k n m : ℕ) : ConcreteBTField (k + n + m) = ConcreteBTField (k + (n + m))

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_eq_of_dest_eq (k m n : ℕ) (h_eq : m = n) : (ConcreteBTField k →+* ConcreteBTField m) = (ConcreteBTField k →+* ConcreteBTField n)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_eq_of_source_eq (k n m : ℕ) (h_eq : k = n) : (ConcreteBTField k →+* ConcreteBTField m) = (ConcreteBTField n →+* ConcreteBTField m)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_cast_dest_apply (k m n : ℕ) (h_eq : m = n) (f : ConcreteBTField k →+* ConcreteBTField m) (x : ConcreteBTField k) : (cast ⋯ f) x = cast ⋯ (f x)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_cast_source_apply (k n m : ℕ) (h_eq : k = n) (f : ConcreteBTField k →+* ConcreteBTField m) (x : ConcreteBTField n) : (cast ⋯ f) x = f (cast ⋯ x)

@[irreducible]

def ConcreteBinaryTower.concreteTowerAlgebraMap (l r : ℕ) (h_le : l ≤ r) : ConcreteBTField l →+* ConcreteBTField r

Auxiliary definition for concreteTowerAlgebraMap using structural recursion. This is easier to reason about in proofs than the Nat.rec version.

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_id (k : ℕ) : concreteTowerAlgebraMap k k ⋯ = RingHom.id (ConcreteBTField k)

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_succ_1 (k : ℕ) : concreteTowerAlgebraMap k (k + 1) ⋯ = canonicalAlgMap k

Right associativity of the Tower Map

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) : concreteTowerAlgebraMap l (r + 1) ⋯ = (concreteTowerAlgebraMap r (r + 1) ⋯).comp (concreteTowerAlgebraMap l r h_le)

Left associativity of the Tower Map

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_succ_last (r l : ℕ) (h_le : l ≤ r) : concreteTowerAlgebraMap l (r + 1) ⋯ = (concreteTowerAlgebraMap (l + 1) (r + 1) ⋯).comp (concreteTowerAlgebraMap l (l + 1) ⋯)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_comp_cast {α β γ δ : ℕ} (f : ConcreteBTField α →+* ConcreteBTField β) (g : ConcreteBTField β →+* ConcreteBTField γ) (h : γ = δ) : (cast ⋯ g).comp f = cast ⋯ (g.comp f)

Cast of composition of ConcreteBTField ring homomorphism is composition of casted ConcreteBTField ring homomorphism. Note that this assumes the SAME underlying instances (e.g. NonAssocSemiring) for both the input and output ring homs.

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_assoc (r mid l : ℕ) (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) : concreteTowerAlgebraMap l r ⋯ = (concreteTowerAlgebraMap mid r h_mid_le_r).comp (concreteTowerAlgebraMap l mid h_l_le_mid)

@[implicit_reducible]

instance ConcreteBinaryTower.instAlgebraTowerConcreteBTF : AlgebraTower ConcreteBTField

Formalization of Cross - Level Algebra : For any k ≤ τ, ConcreteBTField τ is an algebra over ConcreteBTField k.

@[reducible, inline]

abbrev ConcreteBinaryTower.ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : Algebra (ConcreteBTField l) (ConcreteBTField r)

def ConcreteBinaryTower.join_via_add_smul (k : ℕ) (h_pos : k > 0) (hi_btf lo_btf : ConcreteBTField (k - 1)) : ConcreteBTField k

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

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

theorem ConcreteBinaryTower.algebraMap_succ_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : (algebraMap (ConcreteBTField (k - 1)) (ConcreteBTField k)) x = join h_pos 0 x

theorem ConcreteBinaryTower.algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : ConcreteBTField i) : (algebraMap (ConcreteBTField i) (ConcreteBTField j)) x = join ⋯ 0 ((algebraMap (ConcreteBTField i) (ConcreteBTField (j - 1))) x)

theorem ConcreteBinaryTower.split_smul_Z_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : split h_pos (x • Z k) = (x, 0)

theorem ConcreteBinaryTower.smul_Z_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : x • Z k = join h_pos x 0

@[simp]

theorem ConcreteBinaryTower.join_eq_join_via_add_smul {k : ℕ} (h_pos : k > 0) (hi_btf lo_btf : ConcreteBTField (k - 1)) : join h_pos hi_btf lo_btf = join_via_add_smul k h_pos hi_btf lo_btf

theorem ConcreteBinaryTower.split_join_via_add_smul_eq_iff_split {k : ℕ} (h_pos : k > 0) (hi_btf lo_btf : ConcreteBTField (k - 1)) : split h_pos (join_via_add_smul k h_pos hi_btf lo_btf) = (hi_btf, lo_btf)

theorem ConcreteBinaryTower.ConcreteBTFieldAlgebra_def (l r : ℕ) (h_le : l ≤ r) : ConcreteBTFieldAlgebra h_le = (concreteTowerAlgebraMap l r h_le).toAlgebra

theorem ConcreteBinaryTower.algebraMap_ConcreteBTFieldAlgebra_def (l r : ℕ) (h_le : l ≤ r) : algebraMap (ConcreteBTField l) (ConcreteBTField r) = concreteTowerAlgebraMap l r h_le

theorem ConcreteBinaryTower.coe_one_succ (l : ℕ) : (algebraMap (ConcreteBTField l) (ConcreteBTField (l + 1))) 1 = 1

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

@[simp]

theorem ConcreteBinaryTower.ConcreteBTFieldAlgebra_id {l r : ℕ} (h_eq : l = r) : ConcreteBTFieldAlgebra ⋯ = h_eq ▸ Algebra.id (ConcreteBTField l)

theorem ConcreteBinaryTower.ConcreteBTFieldAlgebra_apply_assoc (l mid r : ℕ) (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) (x : ConcreteBTField l) : (algebraMap (ConcreteBTField l) (ConcreteBTField r)) x = (algebraMap (ConcreteBTField mid) (ConcreteBTField r)) ((algebraMap (ConcreteBTField l) (ConcreteBTField mid)) x)

@[reducible, inline]

abbrev ConcreteBinaryTower.binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (ConcreteBTField l) (ConcreteBTField r)

This also provides the corresponding Module instance.

@[implicit_reducible]

instance ConcreteBinaryTower.algebra_adjacent_tower (l : ℕ) : Algebra (ConcreteBTField l) (ConcreteBTField (l + 1))

theorem ConcreteBinaryTower.algebraMap_adjacent_tower_def (l : ℕ) : algebraMap (ConcreteBTField l) (ConcreteBTField (l + 1)) = canonicalAlgMap l

theorem ConcreteBinaryTower.aeval_definingPoly_at_Z_succ (k : ℕ) : (Polynomial.aeval (Z (k + 1))) (definingPoly (Z k)) = 0