Concrete Binary Tower Field

Field-structure lemmas for successive levels of the concrete binary tower.

Lemmas of field properties at level k that depends on field properties at level (k-1)

theorem ConcreteBinaryTower.concrete_mul_eq {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b : ConcreteBTField k) {a₁ a₀ b₁ b₀ : ConcreteBTField (k - 1)} (h_a : (a₁, a₀) = split h_k a) (h_b : (b₁, b₀) = split h_k b) : concrete_mul a b = join h_k (concrete_mul a₀ b₁ + concrete_mul b₀ a₁ + concrete_mul (concrete_mul a₁ b₁) (Z (k - 1))) (concrete_mul a₀ b₀ + concrete_mul a₁ b₁)

theorem ConcreteBinaryTower.concrete_zero_mul {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul zero a = zero

theorem ConcreteBinaryTower.concrete_mul_zero {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul a zero = zero

theorem ConcreteBinaryTower.concrete_one_mul {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul one a = a

theorem ConcreteBinaryTower.concrete_mul_one {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul a one = a

theorem ConcreteBinaryTower.concrete_pow_base_one {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (n : ℕ) : concrete_pow_nat 1 n = 1

theorem ConcreteBinaryTower.concrete_mul_comm {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b : ConcreteBTField k) : concrete_mul a b = concrete_mul b a

theorem ConcreteBinaryTower.concrete_mul_assoc {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)

theorem ConcreteBinaryTower.concrete_mul_left_distrib {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c

theorem ConcreteBinaryTower.concrete_mul_right_distrib {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c

theorem ConcreteBinaryTower.norm_of_ne_zero_is_ne_zero {k : ℕ} {h_k_gt_0 : k > 0} (prevBTFieldResult : ConcreteBTFStepResult (k - 1)) (a : ConcreteBTField k) (h_a_ne_zero : a ≠ 0) : have a₁ := (split h_k_gt_0 a).1; have a₀ := (split h_k_gt_0 a).2; concrete_mul a₀ (a₀ + concrete_mul a₁ (Z (k - 1))) + concrete_mul a₁ a₁ ≠ 0

theorem ConcreteBinaryTower.concrete_mul_inv_cancel {k : ℕ} (prevBTFieldResult : ConcreteBTFStepResult (k - 1)) (a : ConcreteBTField k) (h : a ≠ 0) : concrete_mul a (concrete_inv a) = one

theorem ConcreteBinaryTower.concrete_inv_one {k : ℕ} : concrete_inv 1 = 1

Inductive tower construction, using lemmas from BTFieldPropsOneLevelLiftingLemmas

theorem ConcreteBinaryTower.Z_square_eq (k : ℕ) (prevBTFieldProps : ConcreteBTFieldProps k) (curBTFieldProps : ConcreteBTFieldProps (k + 1)) : Z (k + 1) ^ 2 = join ⋯ (Z k) 1

def ConcreteBinaryTower.liftBTFieldProps (k : ℕ) (prevBTFResult : ConcreteBTFStepResult k) : ConcreteBTFieldProps (k + 1)

@[reducible]

def ConcreteBinaryTower.liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult k) : Field (ConcreteBTField (k + 1))

def ConcreteBinaryTower.concreteCanonicalEmbedding (k : ℕ) (prevBTFieldProps : ConcreteBTFieldProps k) (curBTFieldProps : ConcreteBTFieldProps (k + 1)) : ConcreteBTField k →+* ConcreteBTField (k + 1)

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

@[implicit_reducible]

instance ConcreteBinaryTower.instAlgebraLiftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult k) : Algebra (ConcreteBTField k) (ConcreteBTField (k + 1))

theorem ConcreteBinaryTower.Z_square_mul_form (k : ℕ) (prev : ConcreteBTFStepResult k) : Z (k + 1) ^ 2 = Z (k + 1) * (algebraMap (ConcreteBTField k) (ConcreteBTField (k + 1))) (Z k) + 1

theorem ConcreteBinaryTower.sum_inv_Z_next_eq (k : ℕ) (prev : ConcreteBTFStepResult k) : Z (k + 1) + (Z (k + 1))⁻¹ = (algebraMap (ConcreteBTField k) (ConcreteBTField (k + 1))) (Z k)

noncomputable def ConcreteBinaryTower.getBTFResult (k : ℕ) : ConcreteBTFStepResult k

@[implicit_reducible]

instance ConcreteBinaryTower.instFieldConcrete {k : ℕ} : Field (ConcreteBTField k)

instance ConcreteBinaryTower.instCharP2 {k : ℕ} : CharP (ConcreteBTField k) 2

@[implicit_reducible]

noncomputable instance ConcreteBinaryTower.instFintype {k : ℕ} : Fintype (ConcreteBTField k)

def ConcreteBinaryTower.𝕏 (k : ℕ) : ConcreteBTField (k + 1)

adjoined root of poly k, generator of successor field BTField (k + 1)