Abstract Binary Tower Algebra

Algebra maps and tower embeddings for the abstract binary tower fields.

noncomputable def BinaryTower.canonicalEmbedding (k : ℕ) : BTField k →+* BTField (k + 1)

The canonical ring homomorphism embedding BTField k into BTField (k+1). This is the AdjoinRoot.of map.

@[simp]

theorem BinaryTower.BTField_add_eq (k n m : ℕ) : BTField (k + n + m) = BTField (k + (n + m))

@[simp]

theorem BinaryTower.BTField.RingHom_eq_of_dest_eq (k m n : ℕ) (h_eq : m = n) : (BTField k →+* BTField m) = (BTField k →+* BTField n)

@[simp]

theorem BinaryTower.BTField.RingHom_eq_of_dest_AdjoinRoot_eq (k m : ℕ) : (BTField k →+* BTField (m + 1)) = (BTField k →+* AdjoinRoot (poly m))

@[simp]

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

@[simp]

theorem BinaryTower.BTField.RingHom_cast_dest_AdjoinRoot_apply (k m : ℕ) (f : BTField k →+* AdjoinRoot (poly m)) (x : BTField k) : (cast ⋯ f) x = cast ⋯ (f x)

@[irreducible]

def BinaryTower.towerAlgebraMap (l r : ℕ) (h_le : l ≤ r) : BTField l →+* BTField r

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

theorem BinaryTower.towerAlgebraMap_id (k : ℕ) : towerAlgebraMap k k ⋯ = RingHom.id (BTField k)

theorem BinaryTower.towerAlgebraMap_succ_1 (k : ℕ) : towerAlgebraMap k (k + 1) ⋯ = canonicalEmbedding k

Right associativity of the Tower Map

theorem BinaryTower.towerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) : towerAlgebraMap l (r + 1) ⋯ = (towerAlgebraMap r (r + 1) ⋯).comp (towerAlgebraMap l r h_le)

Left associativity of the Tower Map

theorem BinaryTower.towerAlgebraMap_succ_last (r l : ℕ) (h_le : l ≤ r) : towerAlgebraMap l (r + 1) ⋯ = (towerAlgebraMap (l + 1) (r + 1) ⋯).comp (towerAlgebraMap l (l + 1) ⋯)

@[simp]

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

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

theorem BinaryTower.towerAlgebraMap_assoc (r mid l : ℕ) (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) : towerAlgebraMap l r ⋯ = (towerAlgebraMap mid r h_mid_le_r).comp (towerAlgebraMap l mid h_l_le_mid)

@[implicit_reducible]

noncomputable instance BinaryTower.instAlgebraTowerNatBTField : AlgebraTower BTField

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

@[reducible]

noncomputable def BinaryTower.binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r)

theorem BinaryTower.binaryTowerAlgebra_def (l r : ℕ) (h_le : l ≤ r) : binaryAlgebraTower h_le = (towerAlgebraMap l r h_le).toAlgebra

theorem BinaryTower.algebraMap_binaryTowerAlgebra_def (l r : ℕ) (h_le : l ≤ r) : algebraMap (BTField l) (BTField r) = towerAlgebraMap l r h_le

theorem BinaryTower.BTField.coe_one_succ (l : ℕ) : (algebraMap (BTField l) (BTField (l + 1))) 1 = 1

@[simp]

theorem BinaryTower.binaryTowerAlgebra_id {l r : ℕ} (h_eq : l = r) : binaryAlgebraTower ⋯ = h_eq ▸ Algebra.id (BTField l)

theorem BinaryTower.binaryTowerAlgebra_apply_assoc (l mid r : ℕ) (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) (x : BTField l) : (algebraMap (BTField l) (BTField r)) x = (algebraMap (BTField mid) (BTField r)) ((algebraMap (BTField l) (BTField mid)) x)

@[reducible]

noncomputable def BinaryTower.binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r)

This also provides the corresponding Module instance.

@[implicit_reducible]

noncomputable instance BinaryTower.algebra_adjacent_tower (l : ℕ) : Algebra (BTField l) (BTField (l + 1))

theorem BinaryTower.algebraMap_adjacent_tower_def (l : ℕ) : algebraMap (BTField l) (BTField (l + 1)) = canonicalEmbedding l

theorem BinaryTower.algebraMap_adjacent_tower_succ_eq_Adjoin_of (k : ℕ) : algebraMap (BTField k) (BTField (k + 1)) = AdjoinRoot.of (poly k)

theorem BinaryTower.algebra_adjacent_tower_def (l : ℕ) : algebra_adjacent_tower l = (canonicalEmbedding l).toAlgebra

theorem BinaryTower.algebra_adjacent_tower_eq_AdjoinRoot_algebra (k : ℕ) : algebra_adjacent_tower k = AdjoinRoot.instAlgebra (poly k)

def BinaryTower.BTField_succ_alg_equiv_adjoinRoot (k : ℕ) : AdjoinRoot (poly k) ≃ₐ[BTField k] BTField (k + 1)